Xazax-hun / domains-oxide

Toy language to help experiment with numerical domains for abstract interpretation
Apache License 2.0
2 stars 0 forks source link

Add fixed-point iteration that works on the edges instead of the nodes #4

Open Xazax-hun opened 1 year ago

Xazax-hun commented 1 year ago

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.