Commit 523006f3 authored by Martin Clochard's avatar Martin Clochard

(WIP) mini-compiler: more intuitive meaning of (%)

parent 8bf3ef19
......@@ -76,7 +76,7 @@ module Compile_bexpr
| Bfalse -> $ if cond then inil () else ibranchf ofs
| Bnot b1 -> $ compile_bexpr b1 (not cond) ofs
| Band b1 b2 ->
let c2 = $ compile_bexpr b2 cond ofs % exn_bool b1 false in
let c2 = $ compile_bexpr b2 cond ofs % exn_bool b1 true in
let ofs = if cond then length c2.wcode else ofs + length c2.wcode in
$ compile_bexpr b1 false ofs ~ c2
| Beq a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~
......@@ -152,14 +152,14 @@ module Compile_com
| Cif cond cmd1 cmd2 -> let code_false = compile_com cmd2 in
let code_true = $ compile_com cmd1 ~ $ ibranchf code_false.code.length in
$ compile_bexpr cond false code_true.wcode.length ~
(code_true % exn_bool cond false) ~
($ code_false % exn_bool_old cond true)
(code_true % exn_bool cond true) ~
($ code_false % exn_bool_old cond false)
| Cwhile test body -> let code_body = compile_com body in
let body_length = length code_body.code + 1 in
let code_test = compile_bexpr test false body_length in
let ofs = length code_test.code + body_length in
let wp_while = $ code_test ~
($ code_body ~ $ ibranchf (- ofs)) % exn_bool test false in
($ code_body ~ $ ibranchf (- ofs)) % exn_bool test true in
let ghost inv = loop_invariant cmd in
let ghost var = loop_variant body test in
let ghost post = loop_post cmd ofs in
......
......@@ -82,22 +82,22 @@ module Compiler_logic
contextual_irrelevance res.wcode p ms ms' -> false) && false };
res
function fork_wp (w:wp_trans 'a) (exn:pre 'a) : wp_trans 'a =
\x p q ms. (exn x p ms -> q ms) /\ (not exn x p ms -> w x p q ms)
function fork_wp (w:wp_trans 'a) (cond:pre 'a) : wp_trans 'a =
\x p q ms. (not cond x p ms -> q ms) /\ (cond x p ms -> w x p q ms)
lemma fork_wp_lemma: forall w:wp_trans 'a,exn x p q ms.
fork_wp w exn x p q ms =
((exn x p ms -> q ms) /\ (not exn x p ms -> w x p q ms))
lemma fork_wp_lemma: forall w:wp_trans 'a,cond x p q ms.
fork_wp w cond x p q ms =
((not cond x p ms -> q ms) /\ (cond x p ms -> w x p q ms))
meta rewrite prop fork_wp_lemma
(* Code combinator for sequence, with wp. *)
let (%) (s:wp 'a) (ghost exn:pre 'a) : wp 'a
let (%) (s:wp 'a) (ghost cond:pre 'a) : wp 'a
requires { wp_correctness s }
ensures { result.wp = fork_wp s.wp exn }
ensures { result.wp = fork_wp s.wp cond }
ensures { result.wcode.length = s.wcode.length /\ wp_correctness result }
= { wcode = s.wcode; wp = fork_wp s.wp exn }
= { wcode = s.wcode; wp = fork_wp s.wp cond }
(* WP transformer for hoare triples. *)
function towp_wp (pr:pre 'a) (ps:post 'a) : wp_trans 'a =
......
......@@ -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="6d58101ef25a960c2128d32f7613d9ec">
<theory name="Compiler_logic" sum="5406b74834a442338dc0e119b6bd4296">
<goal name="seq_wp_lemma">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......
......@@ -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="c5b85372fd5c958f2659e46d7bf09fa3" expanded="true">
<theory name="VM_instr_spec" sum="248e9ea0b1524771f1c03296a0834509" 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">
......@@ -50,7 +50,6 @@
<goal name="WP_parameter ivarf" expl="VC for ivarf">
<transf name="split_goal_wp">
<goal name="WP_parameter ivarf.1" expl="1. precondition">
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<transf name="simplify_trivial_quantification">
<goal name="WP_parameter ivarf.1.1" expl="1.">
<transf name="compute_specified">
......@@ -85,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.40"/></proof>
<proof prover="1"><result status="valid" time="1.80"/></proof>
</goal>
</transf>
</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