Translation validator

[ailrst]

This draft pull request adds a translation validated simplifier pipeline enabled by the --simplify-tv flag. This has mostly rewritten from the last iteration but probably still needs work.

See: ir/transforms/validate/SimplifyPipeline.scala for the supported transforms.

This incarnation directly generates QF_BV SMT queries for validataion, as testing showed this is substantially more performant. Similarly we use CVC5 over Z3 as this works better on these queries.

The smt interface is provided by javasmt, and we now support basic model extraction, in the case of validation failure you get input like:

[242] [INFO]   checksat tvsmt/Parameters-uppercase_4268944.smt2
[242] [ERROR]   sat tvsmt/Parameters uppercase_4268944 [[email protected]:1156]
[242] [ERROR]   Part of invariant failed: boolimplies(eq($source__SYNTH_PC_AT4:bv64, 0x2:bv64), booland(booland(booland(booland(booland(booland(booland(booland(booland(booland(booland(booland(booland(booland(bool
and(booland(booland(booland(booland(booland(eq(source__R0_out_AT1:bv64, $target__R0_AT21:bv64), eq(source__R10_out_AT1:bv64, $target__R10_AT1:bv64)), eq(source__R11_out_AT1:bv64, $target__R11_AT1:bv64)), eq(sourc
e__R12_out_AT1:bv64, $target__R12_AT1:bv64)), eq(source__R13_out_AT1:bv64, $target__R13_AT1:bv64)), eq(source__R14_out_AT1:bv64, $target__R14_AT1:bv64)), eq(source__R15_out_AT1:bv64, $target__R15_AT1:bv64)), eq(s
ource__R18_out_AT1:bv64, $target__R18_AT1:bv64)), eq(source__R1_out_AT1:bv64, $target__R1_AT9:bv64)), eq(source__R29_out_AT1:bv64, $target__R29_AT7:bv64)), eq(source__R2_out_AT1:bv64, $target__R2_AT6:bv64)), eq(s
ource__R31_out_AT1:bv64, $target__R31_AT6:bv64)), eq(source__R3_out_AT1:bv64, $target__R3_AT5:bv64)), eq(source__R4_out_AT1:bv64, $target__R4_AT1:bv64)), eq(source__R5_out_AT1:bv64, $target__R5_AT1:bv64)), eq(sou
rce__R6_out_AT1:bv64, $target__R6_AT1:bv64)), eq(source__R7_out_AT1:bv64, $target__R7_AT1:bv64)), eq(source__R8_out_AT1:bv64, $target__R8_AT1:bv64)), eq(source__R9_out_AT1:bv64, $target__R9_AT1:bv64)), eq(source_
__PC_out_AT1:bv64, $target___PC:bv64)), eq($source__TRACE_MEM_mem_64_8_AT25:bool, $target__TRACE_MEM_mem_64_8_AT25:bool))) [[email protected]:849]
[242]  Specifically:
[242]   eq(source__R10_out_AT1:bv64, $target__R10_AT1:bv64) is false
[242] [INFO]   Trace source:
[242] source__uppercase_4268944_SYNTH_ENTRY
[242] source__cut_join_to_Loop1_2
[242] source__uppercase_28
[242] source__uppercase_26
...

In addition to the above, this implementation is improved over the previous iteration by supporting basic interprocedural reasoning (a basic interprocedural analysis lifts call side effects to procedure-local effects): this is sufficient to validate the Parameter inference transform.

To Do

• Fix bugs in invariant generation; injection of analysis facts for motion transforms
• write docmentation explaining how this feature works and what it provides
• make smt file dumping and immediate transform call configurable
• add system test using the TV
• compile with -Wunused and clean up dead code and comments
• extract smt query from JavaSMT to avoid duplicating query build it doesn't really provide much to support this
• --simplify-tv passes on cntlm-noduk
• transform which introduces assertion; support specifying an introduced assertion to ignore
• fix solver timeout; seems to ignore request shutdown (if its even firing), cvc5 should be able to take a timeout flag through furtherOptions cvc5.tlimit. its down the stack
• extract metrics, print big error if any transform has failed, at the end of the run
• fix tv ssa performance
• specification validation: assert(sat(invariant)), assert(sat(not(invariant))
• litmus test that unsat core contains most of source target program
• ensure it works with --tv-assert

Known Design Issues

• The SSA transform is extremely slow because it tracks all defined variables and unions the map on every join
  • this is mitigated a bit by culling using live variables
• The SideEffectStatement is a somewhat tortured abstraction (extends NOP statement): really the DAG CFA needs to be its own graph IR with edges of only assignment and monadic side effect statements, but I don't want to write a new graph implementation and iterator
• The way invariants are generated and injected into the product program (live variables/globals in source renamed with transform drescription function, then the SSA renaming at a cut point, especially as it interacts with ackermannisation) is quite convoluted and fragile, not sure theres a good solution for this though.
• We haven't implemented the case analysis functionality of the previous implementation -- seems to not be super neccessary due to more effective smt representation basic form of this has been implemented
• still no support for interprocedural flow facts / extra predicates in ackermann axioms