Extend the LiftImperativeExpression pass.
It should also handle programs like:
procedure foo() {
var x := 1;
var y := {
assert x > 0;
3
};
assert (x := 2) == 2
}
Meaning: asserts and assumes need to be lifted as well. And the children of asserts and assumes should be lifted just like the children of other nodes.
For any node that is lifted, its prepend statement should come after the prepend statements added by its children, so you need to do:
let prePrepends ← takePrepends -- save outer prepends (from x := 3)
let seqArgs ← args.reverse.mapM transformExpr
let argPrepends ← takePrepends -- just the arg-generated prepends
...
modify fun s => { s with prependedStmts := s.prependedStmts ++ argPrepends ++ liftedThing ++ prePrepends }
Extend the LiftImperativeExpression pass.
It should also handle programs like:
Meaning: asserts and assumes need to be lifted as well. And the children of asserts and assumes should be lifted just like the children of other nodes.
For any node that is lifted, its prepend statement should come after the prepend statements added by its children, so you need to do:
let prePrepends ← takePrepends -- save outer prepends (from x := 3)
let seqArgs ← args.reverse.mapM transformExpr
let argPrepends ← takePrepends -- just the arg-generated prepends
...
modify fun s => { s with prependedStmts := s.prependedStmts ++ argPrepends ++ liftedThing ++ prePrepends }