search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 60 forks source link

Avoid divide-by-zero in the PLE Interpreter #686

Closed facundominguez closed 6 months ago

facundominguez commented 6 months ago

There was an attempt in #560 to avoid producing expressions in tests that would cause divide-by-zero when simplifying them. This problem seems to have resurfaced here with a counter-example like:

POr
  [ POr
    [ ESym (SL "dymkjhhxgd")
    , ECon (L "emurwzzckkgx" (FTC (TC "Stcdlfq" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False}))))
    ]
  , EBin Div (ECon (I 0)) (ECon (R 0.0))
  ]

I cannot reproduce the failure, but it is apparent that the code that generates expressions would need to recognize the division by zero when one operand is integer and the other is real.

I do want to ask, however, why is that the simplifier must simplify all divisions of constants, instead of leaving divisions by zero unmodified. Perhaps a better solution is to modify the simplifier to desist from constant folding in this case (?).

ranjitjhala commented 6 months ago

I agree, we should just leave the div-by-zero alone in this case I think!