User Tools

Site Tools


constant_folding

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

constant_folding [2015/10/08 15:20] (current)
Line 1: Line 1:
 +<note warning>​This page is a draft</​note>​
 +
 +===== Constant folding =====
 +
 +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.
 +
 +<code ocaml>
 +val cf_com : com -> env -> com = <fun>
 +</​code>​
 +
 +<note tip>
 +**Hint.** To precompute an expression, try to evaluate it with the empty store. If you get a result, then it is just the precomputed constant. Otherwise, an exception ''​UninitializedLoc''​ is thrown, meaning that the expression cannot be precomputed (at least, using the naïve method described above).
 +</​note>​
 +
 +The function ''​optimize_com''​ uses the result of ''​cf_com''​ to transform a program as follows:
 +  * if the guard ''​b''​ of a conditional ''​If(b,​c1,​c2)''​ is true, it replaces the ''​If''​ with ''​c1''​
 +  * if the guard ''​b''​ of a conditional ''​If(b,​c1,​c2)''​ is false, it replaces the ''​If''​ with ''​c2''​
 +  * if the guard ''​b''​ of a loop ''​While(b,​c)''​ is false, it replaces the ''​While''​ with a ''​Skip''​
 +
 +<code ocaml>
 +val optimize_com : com -> com = <fun>
 +</​code>​
 +
 +The function used to optimize a program is defined as follows:
 +<code ocaml> ​
 +# 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>
 +</​code>​
 +
 +Here are some examples.
 +
 +<code ocaml>
 +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)))))
 +;;
 +</​code>​
 +
 +<code ocaml>
 +# 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))))
 +</​code>​
 +
 +<code ocaml>
 +# 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))))
 +</​code>​
 +
 +<code ocaml>
 +# 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))
 +</​code>​
  
constant_folding.txt · Last modified: 2015/10/08 15:20 (external edit)