We want to define a static analysis of IMP programs that simplifies them by precomputing the constants used in assignments and boolean guards.
The function cf_com
transforms a command by replacing the constant expressions therein with the precomputed ones.
An expression can be precomputed if it does not contain variables.
val cf_com : com -> env -> com = <fun>
UninitializedLoc
is thrown, meaning that the expression cannot be precomputed (at least, using the naïve method described above).
The function optimize_com
uses the result of cf_com
to transform a program as follows:
b
of a conditional If(b,c1,c2)
is true, it replaces the If
with c1
b
of a conditional If(b,c1,c2)
is false, it replaces the If
with c2
b
of a loop While(b,c)
is false, it replaces the While
with a Skip
val optimize_com : com -> com = <fun>
The function used to optimize a program is defined as follows:
# let optimize_prog (Program (d,c)) = let (r,s) = sem_dec d (emptyenv(),emptystore()) in Program (d,optimize_com (cf_com c r)) ;; val optimize_prog : prog -> prog = <fun>
Here are some examples.
let foo k h = Program( Dseq(Const (Ide "k", N k),Dseq(Const (Ide "h", N h),Var (Ide "i"))), Cseq(Assign (Ide "i", Add(Val (Ide "k"), Val (Ide "h"))), If(Leq (Val (Ide "k"), Val (Ide "h")), While(Leq (Val (Ide "k"), N 10), Assign (Ide "i", Mul (Val (Ide "h"),Val (Ide "k")))), Assign (Ide "i", Add (Val (Ide "i"),N 1))))) ;;
# optimize_prog (foo 3 5);; - : prog = Program (Dseq (Const (Ide "k", N 3), Dseq (Const (Ide "h", N 5), Var (Ide "i"))), Cseq (Assign (Ide "i", N 8), While (True, Assign (Ide "i", N 15))))
# optimize_prog (foo 5 3);; - : prog = Program (Dseq (Const (Ide "k", N 5), Dseq (Const (Ide "h", N 3), Var (Ide "i"))), Cseq (Assign (Ide "i", N 8), Assign (Ide "i", Add (Val (Ide "i"), N 1))))
# optimize_prog (foo 11 12);; - : prog = Program (Dseq (Const (Ide "k", N 11), Dseq (Const (Ide "h", N 12), Var (Ide "i"))), Cseq (Assign (Ide "i", N 23), Skip))