examples/register_allocation.mlw

   1
   2 (** A tiny register allocator for tree expressions.
   3
   4     Authors: Martin Clochard (École Normale Supérieure)
   5              Jean-Christophe Filliâtre (CNRS)
   6  *)
   7
   8 module Spec
   9
  10   use int.Int
  11
  12   type addr
  13
  14   type expr =
  15   | Evar addr
  16   | Eneg expr
  17   | Eadd expr expr
  18
  19   type memory = addr -> int
  20
  21   function eval (m: memory) (e: expr) : int =
  22     match e with
  23     | Evar x     -> m x
  24     | Eneg e     -> - (eval m e)
  25     | Eadd e1 e2 -> eval m e1 + eval m e2
  26     end
  27
  28   type register = int
  29
  30   type instr =
  31     | Iload addr register
  32     | Ineg  register
  33     | Iadd  register register
  34     | Ipush register
  35     | Ipop  register
  36
  37   type registers = register -> int
  38
  39   function update (reg: registers) (r: register) (v: int) : registers =
  40     fun r' -> if r' = r then v else reg r'
  41
  42   use list.List
  43
  44   type stack = list int
  45
  46   type state = {
  47     mem: memory;
  48     reg: registers;
  49     st : stack;
  50   }
  51
  52   function exec (i: instr) (s: state) : state =
  53     match i with
  54     | Iload x r   -> { s with reg = update s.reg r (s.mem x) }
  55     | Ineg  r     -> { s with reg = update s.reg r (- s.reg r) }
  56     | Iadd  r1 r2 -> { s with reg = update s.reg r2 (s.reg r1 + s.reg r2) }
  57     | Ipush r     -> { s with st = Cons (s.reg r) s.st }
  58     | Ipop  r     -> match s.st with
  59                      | Nil       -> s (* fails *)
  60                      | Cons v st -> { s with reg = update s.reg r v; st = st }
  61                      end
  62     end
  63   meta rewrite_def function exec
  64
  65   type code = list instr
  66
  67   function exec_list (c: code) (s: state) : state =
  68     match c with
  69     | Nil      -> s
  70     | Cons i l -> exec_list l (exec i s)
  71     end
  72
  73   use list.Append
  74
  75   let rec lemma exec_append (c1 c2: code) (s: state) : unit
  76     ensures { exec_list (c1 ++ c2) s = exec_list c2 (exec_list c1 s) }
  77     variant { c1 }
  78   = match c1 with
  79     | Nil        -> ()
  80     | Cons i1 l1 -> exec_append l1 c2 (exec i1 s)
  81     end
  82
  83   (** specification of the forthcoming compilation:
  84       - value of expression e lies in register r in final state
  85       - all registers smaller than are preserved
  86       - memory and stack are preserved *)
  87   function expr_post (e: expr) (r: register) : state -> state -> bool =
  88     fun s s' -> s'.mem = s.mem /\ s'.reg r = eval s.mem e /\ s'.st = s.st /\
  89       forall r'. r' < r -> s'.reg r' = s.reg r'
  90   meta rewrite_def function expr_post
  91
  92 end
  93
  94 (** Double WP technique
  95
  96     If you read French, see https://hal.inria.fr/hal-01094488
  97
  98     See also this other Why3 proof, from where this technique originates:
  99     http://toccata.lri.fr/gallery/double_wp.en.html
 100 *)
 101
 102 module DWP
 103
 104   use list.List
 105   use list.Append
 106   use Spec
 107
 108   meta compute_max_steps 0x10000
 109
 110   predicate (-->) (x y: 'a) = [@rewrite] x = y
 111   meta rewrite_def predicate (-->)
 112
 113   type post = state -> state -> bool
 114   type hcode = {
 115     hcode : code;
 116     ghost post : post;
 117   }
 118   predicate hcode_ok (hc: hcode) = forall s. hc.post s (exec_list hc.hcode s)
 119
 120   type trans = (state -> bool) -> state -> bool
 121   type wcode = {
 122     ghost trans : trans;
 123     wcode : code;
 124   }
 125   predicate wcode_ok (wc: wcode) = forall q s.
 126     wc.trans q s -> q (exec_list wc.wcode s)
 127
 128   function to_wp (pst: post) : trans = fun q s1 -> forall s2. pst s1 s2 -> q s2
 129   meta rewrite_def function to_wp
 130
 131   function rcompose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = fun f g x -> g (f x)
 132   meta rewrite_def function rcompose
 133
 134   function exec_closure (i: instr) : state -> state = fun s -> exec i s
 135   function id : 'a -> 'a = fun x -> x
 136
 137   let ($_) (hc: hcode) : wcode
 138     requires { hcode_ok hc }
 139     ensures { wcode_ok result }
 140     ensures { result.trans --> to_wp hc.post }
 141   = { wcode = hc.hcode; trans = to_wp hc.post }
 142
 143   let wrap (wc: wcode) (ghost pst: post) : hcode
 144     requires { wcode_ok wc }
 145     requires { forall x. wc.trans (pst x) x }
 146     ensures { hcode_ok result }
 147     ensures { result.post --> pst }
 148   = { hcode = wc.wcode; post = pst }
 149
 150   let (--) (w1 w2: wcode) : wcode
 151     requires { wcode_ok w1 /\ wcode_ok w2 }
 152     ensures { wcode_ok result }
 153     ensures { result.trans --> rcompose w2.trans w1.trans }
 154   = { wcode = w1.wcode ++ w2.wcode; trans = rcompose w2.trans w1.trans }
 155
 156   let cons (i: instr) (w: wcode) : wcode
 157     requires { wcode_ok w }
 158     ensures { wcode_ok result }
 159     ensures { result.trans --> rcompose w.trans (rcompose (exec i)) }
 160   = { wcode = Cons i w.wcode;
 161       trans = rcompose w.trans (rcompose (exec_closure i)) }
 162
 163   let nil () : wcode
 164     ensures { wcode_ok result }
 165     ensures { result.trans --> fun q -> q }
 166   = { wcode = Nil; trans = id }
 167
 168 end
 169
 170 module InfinityOfRegisters
 171
 172   use int.Int
 173   use list.List
 174   use list.Append
 175   use Spec
 176   use DWP
 177
 178   (** `compile e r` returns a list of instructions that stores the value
 179       of `e` in register `r`, without modifying any register `r' < r`. *)
 180
 181   let rec compile (e: expr) (r: register) : hcode
 182     variant { e }
 183     ensures { hcode_ok result }
 184     ensures { result.post --> expr_post e r }
 185   = wrap (
 186       match e with
 187       | Evar x -> cons (Iload x r) (nil ())
 188       | Eneg e -> $ compile e r -- cons (Ineg r) (nil ())
 189       | Eadd e1 e2 ->
 190           $ compile e1 r -- $ compile e2 (r + 1) -- cons (Iadd (r+1) r) (nil ())
 191       end) (expr_post e r)
 192
 193   (* To recover usual specification. *)
 194   let ghost recover (e: expr) (r: register) (h: hcode) : unit
 195     requires { hcode_ok h /\ h.post --> expr_post e r }
 196     ensures  { forall s. let s' = exec_list h.hcode s in
 197                s'.mem = s.mem /\
 198                s'.reg r = eval s.mem e /\
 199                s'.st = s.st /\
 200                forall r'. r' < r -> s'.reg r' = s.reg r' }
 201   = ()
 202
 203 end
 204
 205 module FiniteNumberOfRegisters
 206
 207   use int.Int
 208   use list.List
 209   use list.Append
 210   use Spec
 211   use DWP
 212
 213   (** we have k registers, namely 0,1,...,k-1,
 214       and there are at least two of them, otherwise we can't add *)
 215   val constant k: int
 216     ensures { 2 <= result }
 217
 218   (** `compile e r` returns a list of instructions that stores the value
 219       of `e` in register `r`, without modifying any register `r' < r`. *)
 220
 221   let rec compile (e: expr) (r: register) : hcode
 222     requires { 0 <= r < k }
 223     variant  { e }
 224     ensures  { hcode_ok result }
 225     ensures  { result.post --> expr_post e r }
 226   = wrap (
 227       match e with
 228       | Evar x -> cons (Iload x r) (nil ())
 229       | Eneg e -> $ compile e r -- cons (Ineg r) (nil ())
 230       | Eadd e1 e2 ->
 231           if r < k-1 then
 232             $ compile e1 r -- $ compile e2 (r + 1) --
 233             cons (Iadd (r + 1) r) (nil ())
 234           else
 235             cons (Ipush (k - 2)) (
 236             $ compile e1 (k - 2) -- $ compile e2 (k - 1) --
 237             cons (Iadd (k - 2) (k - 1)) (
 238             cons (Ipop (k - 2)) (nil ())))
 239       end) (expr_post e r)
 240
 241 end
 242
 243 module OptimalNumberOfRegisters
 244
 245   use int.Int
 246   use int.MinMax
 247   use list.List
 248   use list.Append
 249   use Spec
 250   use DWP
 251
 252   (** we have `k` registers, namely `0,1,...,k-1`,
 253       and there are at least two of them, otherwise we can't add *)
 254   val constant k: int
 255     ensures { 2 <= result }
 256
 257   (** the minimal number of registers needed to evaluate e *)
 258   let rec function n (e: expr) : int
 259   variant { e }
 260   = match e with
 261     | Evar _     -> 1
 262     | Eneg e     -> n e
 263     | Eadd e1 e2 -> let n1 = n e1 in let n2 = n e2 in
 264                     if n1 = n2 then 1 + n1 else max n1 n2
 265     end
 266
 267   (** Note: This is of course inefficient to recompute function `n` many
 268       times. A realistic implementation would compute `n e` once for
 269       each sub-expression `e`, either with a first pass of tree decoration,
 270       or with function `compile` returning the value of `n e` as well,
 271       in a bottom-up way *)
 272
 273   function measure (e: expr) : int =
 274     match e with
 275     | Evar _     -> 0
 276     | Eneg e     -> 1 + measure e
 277     | Eadd e1 e2 -> 1 + if n e1 >= n e2 then measure e1 + measure e2
 278                         else 1 + measure e1 + measure e2
 279     end
 280
 281   lemma measure_nonneg: forall e. measure e >= 0
 282
 283   (** `compile e r` returns a list of instructions that stores the value
 284       of `e` in register `r`, without modifying any register `r' < r`. *)
 285
 286   let rec compile (e: expr) (r: register) : hcode
 287     requires { 0 <= r < k }
 288     variant  { measure e }
 289     ensures  { hcode_ok result }
 290     ensures  { result.post --> expr_post e r }
 291   = wrap (
 292       match e with
 293       | Evar x -> cons (Iload x r) (nil ())
 294       | Eneg e -> $ compile e r -- cons (Ineg r) (nil ())
 295       | Eadd e1 e2 ->
 296           if n e1 >= n e2 then (* we must compile e1 first *)
 297             if r < k-1 then
 298               $ compile e1 r -- $ compile e2 (r + 1) --
 299               cons (Iadd (r + 1) r) (nil ())
 300             else
 301               cons (Ipush (k - 2)) (
 302               $ compile e1 (k - 2) -- $ compile e2 (k - 1) --
 303               cons (Iadd (k - 2) (k - 1)) (
 304               cons (Ipop (k - 2)) (nil ())))
 305           else
 306             $ compile (Eadd e2 e1) r (* compile e2 first *)
 307       end) (expr_post e r)
 308
 309 end