Commit 54f830cf authored by Martin Clochard's avatar Martin Clochard

examples/register_allocation: proved

parent 9cd2cacb
......@@ -57,6 +57,7 @@ module Spec
| Cons v st -> { s with reg = update s.reg r v; st = st }
end
end
meta rewrite_def function exec
type code = list instr
......@@ -76,6 +77,79 @@ module Spec
| Cons i1 l1 -> exec_append l1 c2 (exec i1 s)
end
function expr_post (e:expr) (r:register) : state -> state -> bool =
\s s'. s'.mem = s.mem /\ s'.reg r = eval s.mem e /\ s'.st = s.st /\
forall r'. r' < r -> s'.reg r' = s.reg r'
meta rewrite_def function expr_post
end
module DWP
use import list.List
use import list.Append
use import Spec
meta compute_max_steps 0x10000
predicate (-->) (x y:'a) = "rewrite" x = y
meta rewrite_def predicate (-->)
type post = state -> state -> bool
type hcode = {
hcode : code;
ghost post : post;
}
predicate hcode_ok (hc:hcode) = forall s. hc.post s (exec_list hc.hcode s)
type trans = (state -> bool) -> state -> bool
type wcode = {
ghost trans : trans;
wcode : code;
}
predicate wcode_ok (wc:wcode) = forall q s.
wc.trans q s -> q (exec_list wc.wcode s)
function to_wp (pst:post) : trans = \q s1. forall s2. pst s1 s2 -> q s2
meta rewrite_def function to_wp
function rcompose : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = \f g x. g (f x)
meta rewrite_def function rcompose
function exec_closure (i:instr) : state -> state = \s. exec i s
function id : 'a -> 'a = \x.x
let ($_) (hc:hcode) : wcode
requires { hcode_ok hc }
ensures { wcode_ok result }
ensures { result.trans --> to_wp hc.post }
= { wcode = hc.hcode; trans = to_wp hc.post }
let wrap (wc:wcode) (ghost pst:post) : hcode
requires { wcode_ok wc }
requires { forall x. wc.trans (pst x) x }
ensures { hcode_ok result }
ensures { result.post --> pst }
= { hcode = wc.wcode; post = pst }
let (--) (w1 w2:wcode) : wcode
requires { wcode_ok w1 /\ wcode_ok w2 }
ensures { wcode_ok result }
ensures { result.trans --> rcompose w2.trans w1.trans }
= { wcode = w1.wcode ++ w2.wcode; trans = rcompose w2.trans w1.trans }
let cons (i:instr) (w:wcode) : wcode
requires { wcode_ok w }
ensures { wcode_ok result }
ensures { result.trans --> rcompose w.trans (rcompose (exec i)) }
= { wcode = Cons i w.wcode;
trans = rcompose w.trans (rcompose (exec_closure i)) }
let nil () : wcode
ensures { wcode_ok result }
ensures { result.trans --> \q.q }
= { wcode = Nil; trans = id }
end
module InfinityOfRegisters
......@@ -85,25 +159,32 @@ module InfinityOfRegisters
use import list.List
use import list.Append
use import Spec
use import DWP
(** [compile e r] returns a list of instructions that stores the value
of [e] in register [r], without modifying any register [r' < r]. *)
let rec compile (e: expr) (r: register) : code
let rec compile (e: expr) (r: register) : hcode
variant { e }
ensures { forall s. let s' = exec_list result s in
ensures { hcode_ok result }
ensures { result.post --> expr_post e r }
= wrap (
match e with
| Evar x -> cons (Iload x r) (nil ())
| Eneg e -> $ compile e r -- cons (Ineg r) (nil ())
| Eadd e1 e2 ->
$ compile e1 r -- $ compile e2 (r + 1) -- cons (Iadd (r+1) r) (nil ())
end) (expr_post e r)
(* To recover usual specification. *)
let ghost recover (e:expr) (r:register) (h:hcode) : unit
requires { hcode_ok h /\ h.post --> expr_post e r }
ensures { forall s. let s' = exec_list h.hcode s in
s'.mem = s.mem /\
s'.reg r = eval s.mem e /\
s'.st = s.st /\
forall r'. r' < r -> s'.reg r' = s.reg r' }
=
match e with
| Evar x ->
Cons (Iload x r) Nil
| Eneg e ->
compile e r ++ Cons (Ineg r) Nil
| Eadd e1 e2 ->
compile e1 r ++ compile e2 (r + 1) ++ Cons (Iadd (r + 1) r) Nil
end
= ()
end
......@@ -114,6 +195,7 @@ module FiniteNumberOfRegisters
use import list.List
use import list.Append
use import Spec
use import DWP
(** we have k registers, namely 0,1,...,k-1 *)
constant k: int
......@@ -124,32 +206,24 @@ module FiniteNumberOfRegisters
(** [compile e r] returns a list of instructions that stores the value
of [e] in register [r], without modifying any register [r' < r]. *)
(** PROOF TO BE COMPLETED
let rec compile (e: expr) (r: register) : code
let rec compile (e: expr) (r: register) : hcode
requires { 0 <= r < k }
variant { e }
ensures { forall s. let s' = exec_list result s in
s'.mem = s.mem /\
s'.st = s.st /\
s'.reg r = eval s.mem e /\
forall r'. r' < r -> s'.reg r' = s.reg r' }
=
match e with
| Evar x ->
Cons (Iload x r) Nil
| Eneg e ->
compile e r ++ Cons (Ineg r) Nil
| Eadd e1 e2 ->
if r < k-1 then
compile e1 r ++ compile e2 (r + 1) ++ Cons (Iadd (r + 1) r) Nil
else
Cons (Ipush (k - 2)) (
compile e1 (k - 2) ++ compile e2 (k - 1) ++
Cons (Iadd (k - 2) (k - 1)) (
Cons (Ipop (k - 2)) Nil))
end
**)
ensures { hcode_ok result }
ensures { result.post --> expr_post e r }
= wrap (
match e with
| Evar x -> cons (Iload x r) (nil ())
| Eneg e -> $ compile e r -- cons (Ineg r) (nil ())
| Eadd e1 e2 ->
if r < k-1 then
$ compile e1 r -- $ compile e2 (r + 1) --
cons (Iadd (r + 1) r) (nil ())
else
cons (Ipush (k - 2)) (
$ compile e1 (k - 2) -- $ compile e2 (k - 1) --
cons (Iadd (k - 2) (k - 1)) (
cons (Ipop (k - 2)) (nil ())))
end) (expr_post e r)
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment