Commit b9175266 authored by Martin Clochard's avatar Martin Clochard

New example: double-wp

parent 4f34500c
(*Imp to ImpVm compiler *)
(*Imp to Vm compiler *)
(**************************************************************************)
(* Compiler for arithmetic expressions *)
module Compile_aexpr
meta compute_max_steps 0x10000
......@@ -16,9 +18,10 @@ module Compile_aexpr
use import logic.Compiler_logic
use import specs.VM_instr_spec
(* Compilation scheme: the generated code for arithmetic expressions
put the result of the expression on the stack. *)
function aexpr_post (a:aexpr) (len:pos) : post 'a =
\x p ms ms'. let VMS _ s m = ms in ms' = VMS (p+len) (push (aeval m a) s) m
meta rewrite_def function aexpr_post
let rec compile_aexpr (a:aexpr) : hl 'a
......@@ -34,6 +37,8 @@ module Compile_aexpr
end in
hoare trivial_pre c (aexpr_post a c.wcode.length)
(* Check that the above specification indeed implies the
natural one. *)
let compile_aexpr_natural (a:aexpr) : code
ensures { forall c p s m. codeseq_at c p result ->
transition_star c (VMS p s m)
......@@ -43,6 +48,7 @@ module Compile_aexpr
end
(* Compiler for boolean expressions. *)
module Compile_bexpr
use import int.Int
......@@ -56,7 +62,9 @@ module Compile_bexpr
use import specs.VM_instr_spec
use import Compile_aexpr
function bexpr_post (b:bexpr) (cond: bool) (out_t:pos) (out_f:pos) : post 'a =
(* Compilation scheme: the generated code perform a jump
iff the boolean expression evaluate to cond. *)
function bexpr_post (b:bexpr) (cond: bool) (out_t:ofs) (out_f:ofs) : post 'a =
\x p ms ms'. let VMS _ s m = ms in if beval m b = cond
then ms' = VMS (p + out_t) s m
else ms' = VMS (p + out_f) s m
......@@ -66,7 +74,7 @@ module Compile_bexpr
\x p ms. let VMS _ _ m = ms in beval m b1 = cond
meta rewrite_def function exec_cond
let rec compile_bexpr (b : bexpr) (cond: bool) (ofs: pos) : hl 'a
let rec compile_bexpr (b:bexpr) (cond:bool) (ofs:ofs) : hl 'a
ensures { result.pre = trivial_pre /\ hl_correctness result }
ensures { result.post =
bexpr_post b cond (result.code.length + ofs) result.code.length }
......@@ -87,7 +95,8 @@ module Compile_bexpr
let ghost post = bexpr_post b cond (c.wcode.length + ofs) c.wcode.length in
hoare trivial_pre c post
let compile_bexpr_natural (b: bexpr) (cond: bool) (ofs: pos) : code
(* Check that the above specification implies the natural one. *)
let compile_bexpr_natural (b:bexpr) (cond:bool) (ofs:ofs) : code
ensures { forall c p s m. codeseq_at c p result ->
transition_star c (VMS p s m)
(VMS (p + length result + if beval m b = cond then ofs else 0) s m) }
......@@ -113,6 +122,10 @@ module Compile_com
use import Compile_aexpr
use import Compile_bexpr
(* Compilation scheme: the generated code for a command
simulates the command on the memory part of the machine state. *)
(* As we specify only terminating behavior, we have to require
that the source program terminates in the initial conditions. *)
function com_pre (cmd:com) : pre 'a =
\x p ms. let VMS p' _ m = ms in p = p' /\ exists m'. ceval m cmd m'
meta rewrite_def function com_pre
......@@ -126,6 +139,8 @@ module Compile_com
\x p ms. let VMS _ _ m = snd x in beval m b1 = cond
meta rewrite_def function exec_cond_old
(* Invariant for loop compilation: any intermediate state
would evaluate to the same final state as the initial state. *)
function loop_invariant (c:com) : pre ('a,machine_state) =
\x p msi. let VMS _ s0 m0 = snd x in let VMS pi si mi = msi in
pi = p /\ s0 = si /\ exists mf. ceval m0 c mf /\ ceval mi c mf
......@@ -168,6 +183,7 @@ module Compile_com
end in
hoare (com_pre cmd) res (com_post cmd res.wcode.length)
(* Get back to natural specification for the compiler. *)
let compile_com_natural (com: com) : code
ensures { forall c p s m m'. ceval m com m' -> codeseq_at c p result ->
transition_star c (VMS p s m) (VMS (p + length result) s m') }
......@@ -177,6 +193,7 @@ module Compile_com
ms' = VMS (p + length res.code) s m') };
res.code
(* Insert the final halting instruction. *)
let compile_program (prog : com) : code
ensures { forall mi mf: state.
ceval mi prog mf -> vm_terminates result mi mf }
......@@ -201,36 +218,3 @@ module Compile_com
end
(*
Local Variables:
compile-command: "why3 ide -L . compiler.mlw"
End:
*)
(* *)
(*
(res.wp p post) ms ->
(exists ms' : machine_state. (post ms')
/\ contextual_irrelevance res.wcode p ms ms')
*)
(*
(res.wp p post) ms
exists ms'
-----------------------------------------------
(post ms') /\ contextual_irrelevance res.wcode p ms ms')
*)
(*condition suffisante ? *)
(* trouver un ms' qui vérifie :
((s2.wp (p + s1.wcode.length) post) ms') /\ contextual_irrelevance res.wcode p ms ms' *)
(*
(res.wp p post) ms
exists ms'
-----------------------------------------------
(post ms') /\ contextual_irrelevance res.wcode p ms ms') *)
......@@ -76,6 +76,7 @@ theory Imp
ceval mi (Cwhile cond body) mf
(* Determinstic semantics *)
lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
forall mf2. ("inversion" ceval mi c mf2) -> mf1 = mf2
......
(* Program logic (hoare logic + weakest preconditions) over
Virtual Machine language. *)
module Compiler_logic
use import int.Int
......@@ -21,21 +24,24 @@ module Compiler_logic
(* Binary predicates over machine states *)
type rel = machine_state -> pred
(* pre/post-conditions types, as parameterized unary/binary predicates. *)
(* pre/post-conditions types, as parameterized unary/binary predicates.
'a represents auxiliary variables
pos is an auxiliary variable representing the absolute position at which
the code is loaded. *)
type pre 'a = 'a -> pos -> pred
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 }
(* Predicate transformer type. *)
(* Predicate transformer type. Same auxiliary variables as for
Hoare triples. *)
type wp_trans 'a = 'a -> pos -> pred -> pred
(* 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. *)
(* Machine transition valid whatever the global code is. *)
predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) =
forall c_glob. codeseq_at c_glob p c -> transition_star c_glob ms1 ms2
......@@ -44,13 +50,15 @@ 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 predicate transformer wp_correctness. *)
(* Similar definition for backward predicate transformers *)
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'
(* WP combinator for sequence. *)
(* WP combinator for sequence. Similar to the standard WP calculus
for sequence. The initial machine state is memorized in auxiliary
variables for potential use in the second code specification. *)
(*** Technical: Why3 refuse the logic call in program,
so we cannot define it in function of (wp 'a) arguments only. *)
function seq_wp
......@@ -84,7 +92,8 @@ module Compiler_logic
meta rewrite prop fork_wp_lemma
(* Code combinator for sequence, with wp. *)
(* Code combinator for conditional execution.
Similar to WP calculus for (if cond then s). *)
let (%) (s:wp 'a) (ghost cond:pre 'a) : wp 'a
requires { wp_correctness s }
......@@ -123,9 +132,14 @@ module Compiler_logic
function trivial_pre : pre 'a = \x p ms. let VMS p' _ _ = ms in p = p'
meta rewrite_def function trivial_pre
(* Accessibility predicate. *)
inductive acc ('a -> 'a -> bool) 'a =
| Acc : forall r, x:'a. (forall y. r y x -> acc r y) -> acc r x
(* An iteration of the loop should make progress
towards the postcondition: either achieve the postcondition,
or preserve the invariant and "decrease" according to
a well-founded relation. *)
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_progress
......@@ -134,7 +148,11 @@ module Compiler_logic
\x p ms . post x p
meta rewrite_def function forget_old
(* Variant of hoare triplet introduction rule for looping code. *)
(* Variant of hoare triplet introduction rule for looping code.
- inv is the loop invariant
- post is the loop postcondition
- var is a well-founded relation over states satisfying the
invariant. *)
let make_loop_hl (c:hl 'a) (ghost inv post:pre 'a) (ghost var:post 'a) : hl 'a
requires { hl_correctness c }
requires { forall x p ms. inv x p ms -> acc (var x p) ms }
......@@ -149,9 +167,3 @@ module Compiler_logic
end
(*
Local Variables:
compile-command: "why3 ide -L . logic.mlw"
End:
*)
......@@ -13,6 +13,8 @@ module VM_instr_spec
\x p ms ms'. ms' = f ms
meta rewrite_def function ifun_post
(* General specification builder for determinstic machine
instructions. *)
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 ->
......@@ -54,7 +56,8 @@ module VM_instr_spec
ensures { result.code.length = 1 /\ hl_correctness result }
= hoare trivial_pre ($ ifunf trivial_pre x.ivar x.ivar_fun) x.ivar_post
(* Binary arithmetic operators specification (Iadd, Isub, Imul) *)
(* Binary arithmetic operators specification (Iadd, Isub, Imul)
via a generic builder. *)
type binop = int -> int -> int
constant ibinop_pre : pre 'a =
......@@ -116,40 +119,41 @@ module VM_instr_spec
= { pre = trivial_pre; code = Nil; post = inil_post }
(* Ibranch specification *)
function ibranch_post (ofs: pos) : post 'a =
function ibranch_post (ofs: ofs) : post 'a =
\x p ms ms'. forall s m. ms = VMS p s m -> ms' = VMS (p + 1 + ofs) s m
meta rewrite_def function ibranch_post
function ibranch_fun (ofs:pos) : machine_state -> machine_state =
function ibranch_fun (ofs:ofs) : machine_state -> machine_state =
\ms. let (VMS p s m) = ms in VMS (p+1+ofs) s m
meta rewrite_def function ibranch_fun
let ibranchf (ofs:pos) : hl 'a
let ibranchf (ofs:ofs) : hl 'a
ensures { result.pre = trivial_pre /\ result.post = ibranch_post ofs }
ensures { result.code.length = 1 /\ hl_correctness result }
= let cf = $ ifunf trivial_pre (ibranch ofs) (ibranch_fun ofs) in
hoare trivial_pre cf (ibranch_post ofs)
(* Conditional jump specification via a generic builder. *)
type cond = int -> int -> bool
function icjump_post (cond:cond) (ofs:int) : post 'a =
function icjump_post (cond:cond) (ofs:ofs) : post 'a =
\x p ms ms'. forall n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m ->
(cond n1 n2 -> ms' = VMS (p + ofs + 1) s m) /\
(not cond n1 n2 -> ms' = VMS (p+1) s m)
meta rewrite_def function icjump_post
function icjump_fun (cond:cond) (ofs:int) : machine_state -> machine_state =
function icjump_fun (cond:cond) (ofs:ofs) : machine_state -> machine_state =
\ms. match ms with
| VMS p (Cons n2 (Cons n1 s)) m ->
if cond n1 n2 then VMS (p+ofs+1) s m else VMS (p+1) s m
| _ -> ms
end
let create_cjump (code_cd:code) (ghost cond:cond) (ghost ofs:pos) : hl 'a
let create_cjump (code_cd:code) (ghost cond:cond) (ghost ofs:ofs) : hl 'a
requires { forall c p1 n1 n2. codeseq_at c p1 code_cd ->
let p2 = (if cond n1 n2 then p1 + 1 + ofs else p1 + 1) in
forall s m. transition c (VMS p1 (push n2 (push n1 s)) m) (VMS p2 s m) }
ensures { result.pre = ibinop_pre /\ result.post = icjump_post cond ofs }
ensures { result.pre = ibinop_pre /\ result.post = icjump_post cond ofs }
ensures { result.code.length = code_cd.length /\ hl_correctness result }
= let c = $ ifunf ibinop_pre code_cd (icjump_fun cond ofs) in
hoare ibinop_pre c (icjump_post cond ofs)
......@@ -167,26 +171,27 @@ module VM_instr_spec
constant bgt : cond = \x y. x > y
meta rewrite_def function bgt
let ibeqf (ofs : pos) : hl 'a
let ibeqf (ofs:ofs) : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = icjump_post beq ofs }
ensures { result.code.length = 1 /\ hl_correctness result }
= create_cjump (ibeq ofs) beq ofs
let ibnef (ofs : pos) : hl 'a
let ibnef (ofs:ofs) : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = icjump_post bne ofs }
ensures { result.code.length = 1 /\ hl_correctness result }
= create_cjump (ibne ofs) bne ofs
let iblef (ofs : pos) : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = icjump_post ble ofs }
ensures { result.code.length = 1 /\ hl_correctness result }
let iblef (ofs:ofs) : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = icjump_post ble ofs }
ensures { result.code.length = 1 /\ hl_correctness result }
= create_cjump (ible ofs) ble ofs
let ibgtf (ofs : pos) : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = icjump_post bgt ofs }
ensures { result.code.length = 1 /\ hl_correctness result }
let ibgtf (ofs:ofs) : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = icjump_post bgt ofs }
ensures { result.code.length = 1 /\ hl_correctness result }
= create_cjump (ibgt ofs) bgt ofs
(* Isetvar specification *)
constant isetvar_pre : pre 'a =
\x p ms . exists n s m. ms = VMS p (push n s) m
meta rewrite_def function isetvar_pre
......@@ -210,8 +215,3 @@ module VM_instr_spec
end
(*
Local Variables:
compile-command: "why3 ide -L . specs.mlw"
End:
*)
(* Utility module: reflexive transitive closure of a parameterized
relation. *)
module ReflTransClosure
type parameter
......@@ -149,9 +151,3 @@ theory Vm "Virtual Machine for IMP language"
end
(*
Local Variables:
compile-command: "why3ide -L . vm.mlw"
End:
*)
......@@ -92,6 +92,7 @@ run_dir foveoos11-cm
run_dir hoare_logic
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir avl "-L avl"
run_dir double_wp "-L double_wp"
echo ""
echo "Summary : $success/$total"
......
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