xazax-hun / domains Goto Github PK

Add assertions about the current state in the tr language. This could provide an opportunity for static analysis to emit warnings when if an assertion might or will fail.

If loops/alternatives could have condition expressions based on the state, it would be possible to demonstrate how narrowing works, and we could eliminate paths based on the analysis state. Moreover, it would be possible to experiment with path sensitive analysis and symbolic execution.

• The driver should be able to print more detailed diagnostics about the individual options.
• We should automate some of the boilerplate adding a new option or use a library.
• We should have bash autocompletion for options.
• We should have abbreviations for the command line flags.

Currently, we can compute and visualize results. It might be nice to be able to generate the equations that are being solved, it might be insightful in some cases.

Imagine the following scenario in constant propagation:

B1   B2
  \   /
   B3

State:

  B1:  u: 1, v: 2 
  B2:  v: 1 u: 2

With the flat constant propagation lattice, after merging the state for B1 and B2 we would get u: Top, v: Top. But in case B3 is u + v, we could execute the transfer function both for the state in B1 and in B2, and merge after the transfer functions are executed.

Overall, we will execute the transfer functions more often, but will end up having better precision.

Use lit test or a similar framework to also test the driver as it starts to accumulate non-trivial amount of code.