User Tools

Site Tools


This page is a draft

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.

val cf_com : com -> env -> com = <fun>

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).

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
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))
constant_folding.txt · Last modified: 2015/10/08 15:20 (external edit)