Commit 4f34500c authored by Martin Clochard's avatar Martin Clochard

(WIP) mini-compiler

parent 3c5f8cc4
......@@ -163,7 +163,7 @@ module Compile_com
let ghost inv = loop_invariant cmd in
let ghost var = loop_variant body test in
let ghost post = loop_post cmd ofs in
let hl_while = hoare inv wp_while (loop_preservation inv post var) in
let hl_while = hoare inv wp_while (loop_progress inv post var) in
$ inil () ~ $ make_loop_hl hl_while inv post var
end in
hoare (com_pre cmd) res (com_post cmd res.wcode.length)
......
......@@ -81,6 +81,6 @@ theory Imp
lemma ceval_deterministic : forall c mi mf1 mf2.
ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
end
......@@ -26,18 +26,13 @@ module Compiler_logic
type post 'a = 'a -> pos -> rel
(* Hoare triples with explicit pre & post *)
type hl 'a =
{ code: code;
ghost pre : pre 'a;
ghost post: post 'a }
type hl 'a = { code: code; ghost pre : pre 'a; ghost post: post 'a }
(* Predicate transformer type. *)
type wp_trans 'a = 'a -> pos -> pred -> pred
(* Code with weakest precondition wp_correctness. *)
type wp 'a =
{ wcode : code;
ghost wp : wp_trans 'a }
(* Code with backward predicate transformer. *)
type wp 'a = { wcode : code; ghost wp : wp_trans 'a }
(* Machine transition independence for a piece of code with respect
to the rest of the code. *)
......@@ -49,7 +44,7 @@ module Compiler_logic
forall x:'a,p ms. cs.pre x p ms ->
exists ms'. cs.post x p ms ms' /\ contextual_irrelevance cs.code p ms ms'
(* Invariant for code with WP wp_correctness. *)
(* Invariant for code with predicate transformer wp_correctness. *)
predicate wp_correctness (code:wp 'a) =
forall x:'a,p post ms. (code.wp x p post) ms ->
exists ms'. post ms' /\ contextual_irrelevance code.wcode p ms ms'
......@@ -58,14 +53,12 @@ module Compiler_logic
(* WP combinator for sequence. *)
(*** Technical: Why3 refuse the logic call in program,
so we cannot define it in function of (wp 'a) arguments only. *)
function seq_wp (l1:int) (w1:wp_trans 'a)
(w2:wp_trans ('a,machine_state)) : wp_trans 'a =
function seq_wp
(l1:int) (w1:wp_trans 'a) (w2:wp_trans ('a,machine_state)) : wp_trans 'a =
\x p q ms. w1 x p (w2 (x,ms) (p+l1) q) ms
lemma seq_wp_lemma :
forall l1,w1: wp_trans 'a,w2 x p q ms.
lemma seq_wp_lemma : forall l1,w1: wp_trans 'a,w2 x p q ms.
seq_wp l1 w1 w2 x p q ms = w1 x p (w2 (x,ms) (p+l1) q) ms
meta rewrite prop seq_wp_lemma
(* Code combinator for sequence, with wp. *)
......@@ -110,7 +103,7 @@ module Compiler_logic
meta rewrite prop towp_wp_lemma
(* Unwrap code with hoare triple into code with wp.
Analogous to function call/abstract block. *)
Analogous to procedure call/abstract block. *)
let ($_) (c:hl 'a) : wp 'a
requires { hl_correctness c }
ensures { result.wcode.length = c.code.length }
......@@ -127,15 +120,15 @@ module Compiler_logic
ensures { result.code.length = c.wcode.length /\ hl_correctness result}
= { code = c.wcode ; pre = pre; post = post }
function trivial_pre : pre 'a = \x p ms. let (VMS p' _ _) = ms in p = p'
function trivial_pre : pre 'a = \x p ms. let VMS p' _ _ = ms in p = p'
meta rewrite_def function trivial_pre
inductive acc ('a -> 'a -> bool) 'a =
| Acc : forall r, x:'a. (forall y. r y x -> acc r y) -> acc r x
function loop_preservation (inv post:pre 'a) (var:post 'a) : post 'a =
function loop_progress (inv post:pre 'a) (var:post 'a) : post 'a =
\x p ms ms'. (inv x p ms' /\ var x p ms' ms) \/ post x p ms'
meta rewrite_def function loop_preservation
meta rewrite_def function loop_progress
function forget_old (post:pre 'a) : post 'a =
\x p ms . post x p
......@@ -146,7 +139,7 @@ module Compiler_logic
requires { hl_correctness c }
requires { forall x p ms. inv x p ms -> acc (var x p) ms }
requires { c.pre = inv }
requires { c.post = loop_preservation inv post var }
requires { c.post = loop_progress inv post var }
ensures { result.pre = inv /\ result.post = forget_old post }
ensures { result.code.length = c.code.length /\ hl_correctness result }
= let res = { code = c.code ; pre = inv ; post = forget_old post } in
......
......@@ -7,7 +7,7 @@
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<file name="../logic.mlw">
<theory name="Compiler_logic" sum="5406b74834a442338dc0e119b6bd4296">
<theory name="Compiler_logic" sum="ae38e28d7adb31fc270172c0537012eb">
<goal name="seq_wp_lemma">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......
......@@ -12,7 +12,7 @@ module VM_instr_spec
function ifun_post (f:machine_state -> machine_state) : post 'a =
\x p ms ms'. ms' = f ms
meta rewrite_def function ifun_post
let ifunf (ghost pre:pre 'a) (code_f:code)
(ghost f:machine_state -> machine_state) : hl 'a
requires { forall c p. codeseq_at c p code_f ->
......@@ -44,7 +44,7 @@ module VM_instr_spec
function ivar_post (x:id) : post 'a =
\a p ms ms'. forall s m. ms = VMS p s m -> ms' = VMS (p+1) (push m[x] s) m
meta rewrite_def function ivar_post
function ivar_fun (x:id) : machine_state -> machine_state =
\ms. let (VMS p s m) = ms in VMS (p+1) (push m[x] s) m
meta rewrite_def function ivar_fun
......@@ -105,7 +105,7 @@ module VM_instr_spec
ensures { result.code.length = 1 /\ hl_correctness result}
= create_binop imul mul
(* Inil spec *)
(* Inil spec *)
function inil_post : post 'a =
\x p ms ms'. ms = ms'
meta rewrite_def function inil_post
......@@ -154,7 +154,7 @@ module VM_instr_spec
= let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in
hoare ibinop_pre c (icjump_post cond ofs)
(* binary Boolean operators specification (Ibeq, Ibne, Ible, Ibgt) *)
(* binary Boolean operators specification (Ibeq, Ibne, Ible, Ibgt) *)
constant beq : cond = \x y. x = y
meta rewrite_def function beq
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../specs.mlw" expanded="true">
<theory name="VM_instr_spec" sum="248e9ea0b1524771f1c03296a0834509" expanded="true">
<theory name="VM_instr_spec" sum="7a644b37a9d4e75706a1354367239885" expanded="true">
<goal name="WP_parameter ifunf" expl="VC for ifunf">
<transf name="split_goal_wp">
<goal name="WP_parameter ifunf.1" expl="1. assertion">
......@@ -84,7 +84,7 @@
<goal name="WP_parameter create_binop.1.1" expl="1.">
<transf name="compute_specified">
<goal name="WP_parameter create_binop.1.1.1" expl="1.">
<proof prover="1"><result status="valid" time="1.80"/></proof>
<proof prover="1"><result status="valid" time="1.42"/></proof>
</goal>
</transf>
</goal>
......@@ -217,7 +217,7 @@
<goal name="WP_parameter isetvarf.1.1" expl="1.">
<transf name="compute_specified">
<goal name="WP_parameter isetvarf.1.1.1" expl="1.">
<proof prover="1"><result status="valid" time="3.30"/></proof>
<proof prover="1"><result status="valid" time="2.47"/></proof>
</goal>
</transf>
</goal>
......
theory State
clone export map.Map
clone export map.Map
type id = Id int
type state = map id int
......
......@@ -43,19 +43,20 @@ theory Vm "Virtual Machine for IMP language"
type machine_state = VMS pos stack state (* virtual machine configuration *)
type ofs = int
(* The instruction set of the machine. *)
type instr =
| Iconst int (* push n on stack *)
| Ivar id (* push the value of variable *)
| Isetvar id (* pop an integer, assign it to variable *)
| Ibranch pos (* skip ofs instructions *)
| Ibranch ofs (* skip ofs instructions *)
| Iadd (* pop two values, push their sum *)
| Isub (* pop two values, push their difference *)
| Imul (* pop two values, push their product *)
| Ibeq pos (* pop n2, pop n1, skip ofs forward if n1 = n2 *)
| Ibne pos (* pop n2, pop n1, skip ofs forward if n1 <> n2 *)
| Ible pos (* pop n2, pop n1, skip ofs forward if n1 <= n2 *)
| Ibgt pos (* pop n2, pop n1, skip ofs forward if n1 > n2 *)
| Ibeq ofs (* pop n2, pop n1, skip ofs forward if n1 = n2 *)
| Ibne ofs (* pop n2, pop n1, skip ofs forward if n1 <> n2 *)
| Ible ofs (* pop n2, pop n1, skip ofs forward if n1 <= n2 *)
| Ibgt ofs (* pop n2, pop n1, skip ofs forward if n1 > n2 *)
| Ihalt (* end of program *)
type code = list instr
......@@ -80,59 +81,59 @@ theory Vm "Virtual Machine for IMP language"
constant iadd : code = Cons Iadd Nil
constant isub : code = Cons Isub Nil
constant imul : code = Cons Imul Nil
function ibeq (ofs:int) : code = Cons (Ibeq ofs) Nil
function ible (ofs:int) : code = Cons (Ible ofs) Nil
function ibne (ofs:int) : code = Cons (Ibne ofs) Nil
function ibgt (ofs:int) : code = Cons (Ibgt ofs) Nil
function ibranch (ofs:int) : code = Cons (Ibranch ofs) Nil
function ibeq (ofs:ofs) : code = Cons (Ibeq ofs) Nil
function ible (ofs:ofs) : code = Cons (Ible ofs) Nil
function ibne (ofs:ofs) : code = Cons (Ibne ofs) Nil
function ibgt (ofs:ofs) : code = Cons (Ibgt ofs) Nil
function ibranch (ofs:ofs) : code = Cons (Ibranch ofs) Nil
constant ihalt : code = (Cons Ihalt Nil)
(* The semantics of the virtual machine is given in small-step style,
as a transition relation between machine states: triples (program
counter, evaluation stack, variable state). The transition relation is
parameterized by the code c. There is one transition rule for each
kind of instruction, except Ihalt, which has no transition. *)
(* The semantics of the virtual machine is given in small-step style,
as a transition relation between machine states: triples (program
counter, evaluation stack, variable state). The transition relation is
parameterized by the code c. There is one transition rule for each
kind of instruction, except Ihalt, which has no transition. *)
inductive transition code machine_state machine_state =
| trans_const : forall c p n. codeseq_at c p (iconst n) ->
forall s m. transition c (VMS p s m) (VMS (p + 1) (push n s) m)
inductive transition code machine_state machine_state =
| trans_const : forall c p n. codeseq_at c p (iconst n) ->
forall s m. transition c (VMS p s m) (VMS (p + 1) (push n s) m)
| trans_var : forall c p x. codeseq_at c p (ivar x) ->
forall s m. transition c (VMS p s m) (VMS (p + 1) (push m[x] s) m)
| trans_var : forall c p x. codeseq_at c p (ivar x) ->
forall s m. transition c (VMS p s m) (VMS (p + 1) (push m[x] s) m)
| trans_set_var: forall c p x. codeseq_at c p (isetvar x) ->
forall n s m. transition c (VMS p (push n s) m) (VMS (p + 1) s m[x<-n])
| trans_set_var: forall c p x. codeseq_at c p (isetvar x) ->
forall n s m. transition c (VMS p (push n s) m) (VMS (p + 1) s m[x<-n])
| trans_add : forall c p. codeseq_at c p iadd ->
forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
(VMS (p + 1) (push (n1 + n2) s) m)
| trans_add : forall c p. codeseq_at c p iadd ->
forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
(VMS (p + 1) (push (n1 + n2) s) m)
| trans_sub : forall c p. codeseq_at c p isub ->
forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
(VMS (p + 1) (push (n1 - n2) s) m)
| trans_sub : forall c p. codeseq_at c p isub ->
forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
(VMS (p + 1) (push (n1 - n2) s) m)
| trans_mul : forall c p. codeseq_at c p imul ->
forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
(VMS (p + 1) (push (n1 * n2) s) m)
| trans_mul : forall c p. codeseq_at c p imul ->
forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
(VMS (p + 1) (push (n1 * n2) s) m)
| trans_beq: forall c p1 ofs. codeseq_at c p1 (ibeq ofs) ->
forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
(VMS (if n1 = n2 then p1 + 1 + ofs else p1 + 1) s m)
| trans_beq: forall c p1 ofs. codeseq_at c p1 (ibeq ofs) ->
forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
(VMS (if n1 = n2 then p1 + 1 + ofs else p1 + 1) s m)
| trans_bne: forall c p1 ofs. codeseq_at c p1 (ibne ofs) ->
forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
(VMS (if n1 = n2 then p1 + 1 else p1 + 1 + ofs) s m)
| trans_bne: forall c p1 ofs. codeseq_at c p1 (ibne ofs) ->
forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
(VMS (if n1 = n2 then p1 + 1 else p1 + 1 + ofs) s m)
| trans_ble: forall c p1 ofs. codeseq_at c p1 (ible ofs) ->
forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
(VMS (if n1 <= n2 then p1 + 1 + ofs else p1 + 1) s m)
| trans_ble: forall c p1 ofs. codeseq_at c p1 (ible ofs) ->
forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
(VMS (if n1 <= n2 then p1 + 1 + ofs else p1 + 1) s m)
| trans_bgt: forall c p1 ofs. codeseq_at c p1 (ibgt ofs) ->
forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
(VMS (if n1 <= n2 then p1 + 1 else p1 + 1 + ofs) s m)
| trans_bgt: forall c p1 ofs. codeseq_at c p1 (ibgt ofs) ->
forall s m n1 n2. transition c (VMS p1 (push n2 (push n1 s)) m)
(VMS (if n1 <= n2 then p1 + 1 else p1 + 1 + ofs) s m)
| trans_branch: forall c p ofs. codeseq_at c p (ibranch ofs) ->
forall s m. transition c (VMS p s m) (VMS (p + 1 + ofs) s m)
| trans_branch: forall c p ofs. codeseq_at c p (ibranch ofs) ->
forall s m. transition c (VMS p s m) (VMS (p + 1 + ofs) s m)
(* As usual with small-step semantics, we form sequences of machine
transitions to define the behavior of a code. We always start with pc
......
......@@ -20,7 +20,7 @@
</transf>
</goal>
</theory>
<theory name="Vm" sum="a613e6c8c28ff260907256dd866405f6">
<theory name="Vm" sum="8a39716eae7f444c42b1f9cce9c81614">
<goal name="codeseq_at_app_right">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
......
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