[CN] Pure term (partial) evaluation

[ZippeyKeys12]

Evaluates terms (IndexTerms.t). Can be used for term simplification.
It is needed to evaluate terms when generating test cases in OCaml-land.

Potential issues

• It's supposed to get stuck on errors, but it still might throw exceptions due to the functions used (ex: List.combine)
  • Some of these checks could be omitted, assuming the term is well-typed.

Other

• No sets, pointer ops, casts and a few other operations

[dc-mak]

It would be useful if you could explain why as well as what. I'm off on holiday for until 12th, so I'll let Christopher handle this.

[cp526]

If we want to be able to use eval to simplify quantified constraints or assertions, then it can't crash on free variables.

[ZippeyKeys12]

It doesn't crash, it returns Error, which partial_eval accounts for (and is what would be used for simplification).

[cp526]

I'm not sure this does the right thing, at least for bitvector sizes larger than 64?

[cp526]

Aside from the inline comments, three general points:

• Is it correct that terms with free variables, such as x == x or x + 0 will never be evaluated, even when they could be simplified? This is just to understand how this relates to the current term simplifier: as discussed previously, we probably eventually want to converge on just one.

• Is the (AIUI possibly diverging) lazy evaluation ever used?

• I'm a bit uneasy about the bitvector operations. AIUI, aside from some hand-coded unary operations, the strategy for binary operations is to simply compute in Z and then use the normalisation function to bring the result into the range of the bitvector type. But do we know whether that gives us the right semantics (i.e. the one given by the mapping to SMT)? For instance, the implementation of division seems to ignore the sign of the bitvector type, and there's probably various subtleties to get right in general.

  How fast does the partial evaluator have to be? We could send bitvectors off to the SMT solver for evaluation (perhaps not as slow as solving), via the same solver.ml pipeline, to make sure the semantics is good.

[ZippeyKeys12]

• Is it correct that terms with free variables, such as x == x or x + 0 will never be evaluated, even when they could be simplified? This is just to understand how this relates to the current term simplifier: as discussed previously, we probably eventually want to converge on just one.

Yes, it won't be evaluated. The goal here is just to do evaluation, which should be fairly simple/clear. For a term simplifier, you'd just call eval in it, similar to what partial_eval does.

• Is the (AIUI possibly diverging) lazy evaluation ever used?

The lazy evaluation is the one I plan to use, and shouldn't diverge. Partial evaluation could, which is why we special-case it to fully evaluate arguments before application. It should also simplify more than the strict version.

• I'm a bit uneasy about the bitvector operations. AIUI, aside from some hand-coded unary operations, the strategy for binary operations is to simply compute in Z and then use the normalisation function to bring the result into the range of the bitvector type. But do we know whether that gives us the right semantics (i.e. the one given by the mapping to SMT)? For instance, the implementation of division seems to ignore the sign of the bitvector type, and there's probably various subtleties to get right in general.

I removed the QCheck/OUnit tests I used to check them, to simplify the PR, but I can add them back and see if I missed any operations.

How fast does the partial evaluator have to be? We could send bitvectors off to the SMT solver for evaluation (perhaps not as slow as solving), via the same solver.ml pipeline, to make sure the semantics is good.

This is what the QCheck/OUnit tests were doing, and then seeing if eval and the SMT solver agreed. This also partly why the strict evaluation exists, to be easier to think about and to test the lazy evaluation against it.

[cp526]

• Is it correct that terms with free variables, such as x == x or x + 0 will never be evaluated, even when they could be simplified? This is just to understand how this relates to the current term simplifier: as discussed previously, we probably eventually want to converge on just one.

Yes, it won't be evaluated. The goal here is just to do evaluation, which should be fairly simple/clear. For a term simplifier, you'd just call eval in it, similar to what partial_eval does.

• Is the (AIUI possibly diverging) lazy evaluation ever used?

The lazy evaluation is the one I plan to use, and shouldn't diverge. Partial evaluation could, which is why we special-case it to fully evaluate arguments before application. It should also simplify more than the strict version.

• I'm a bit uneasy about the bitvector operations. AIUI, aside from some hand-coded unary operations, the strategy for binary operations is to simply compute in Z and then use the normalisation function to bring the result into the range of the bitvector type. But do we know whether that gives us the right semantics (i.e. the one given by the mapping to SMT)? For instance, the implementation of division seems to ignore the sign of the bitvector type, and there's probably various subtleties to get right in general.

I removed the QCheck/OUnit tests I used to check them, to simplify the PR, but I can add them back and see if I missed any operations.

Tests are good, but really the question is what the correctness argument is wrt the SMT mapping.

For instance, in the SMT mapping CN Div turns into either an SMT bv_sdiv or bv_udiv, depending on the sign of the CN bitvector type. I don't see anything corresponding to that here. Does the partial evaluator's Z.div + normalisation behave like bv_sdiv and bv_udiv, respectively?

How fast does the partial evaluator have to be? We could send bitvectors off to the SMT solver for evaluation (perhaps not as slow as solving), via the same solver.ml pipeline, to make sure the semantics is good.

This is what the QCheck/OUnit tests were doing, and then seeing if eval and the SMT solver agreed. This also partly why the strict evaluation exists, to be easier to think about and to test the lazy evaluation against it.

... Given the question about the relationship between the SMT semantics and the partial evaluator's implementation, would the evaluator be fast enough if we replaced its bitvector logic with a call into the SMT solver's evaluator (i.e. whenever a unary or binary operation is applied to a bitvector constant, simply asking the SMT solver to evaluate it for us)?