mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
230 lines
7.9 KiB
Plaintext
230 lines
7.9 KiB
Plaintext
|
|
module VM_instr_spec
|
|
|
|
meta compute_max_steps 0x10000
|
|
|
|
use int.Int
|
|
use list.List
|
|
use list.Length
|
|
use vm.Vm
|
|
use state.State
|
|
use logic.Compiler_logic
|
|
|
|
function ifun_post (f:machine_state -> machine_state) : post 'a =
|
|
fun _ _ 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 ->
|
|
forall x ms. pre x p ms -> transition c ms (f ms) }
|
|
ensures { result.pre --> pre }
|
|
ensures { result.post --> ifun_post f }
|
|
ensures { result.code --> code_f }
|
|
= { pre = pre; code = code_f; post = ifun_post f }
|
|
|
|
(* Iconst spec *)
|
|
function iconst_post (n:int) : post 'a =
|
|
fun _ p ms ms' -> forall s m. ms = VMS p s m -> ms' = VMS (p+1) (push n s) m
|
|
meta rewrite_def function iconst_post
|
|
|
|
function iconst_fun (n:int) : machine_state -> machine_state =
|
|
fun ms -> let (VMS p s m) = ms in VMS (p+1) (push n s) m
|
|
meta rewrite_def function iconst_fun
|
|
|
|
let iconstf (n: int) : hl 'a
|
|
ensures { result.pre --> trivial_pre }
|
|
ensures { result.post --> iconst_post n }
|
|
ensures { result.code.length --> 1 }
|
|
= hoare trivial_pre ($ ifunf trivial_pre n.iconst n.iconst_fun) n.iconst_post
|
|
|
|
(* Ivar spec *)
|
|
function ivar_post (x:id) : post 'a =
|
|
fun _ 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 =
|
|
fun ms -> let (VMS p s m) = ms in VMS (p+1) (push m[x] s) m
|
|
meta rewrite_def function ivar_fun
|
|
|
|
let ivarf (x: id) : hl 'a
|
|
ensures { result.pre --> trivial_pre }
|
|
ensures { result.post --> ivar_post x }
|
|
ensures { result.code.length --> 1 }
|
|
= hoare trivial_pre ($ ifunf trivial_pre x.ivar x.ivar_fun) x.ivar_post
|
|
|
|
(* Binary arithmetic operators specification (Iadd, Isub, Imul)
|
|
via a generic builder. *)
|
|
type binop = int -> int -> int
|
|
|
|
constant ibinop_pre : pre 'a =
|
|
fun _ p ms -> exists n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m
|
|
meta rewrite_def function ibinop_pre
|
|
|
|
function ibinop_post (op : binop) : post 'a =
|
|
fun _ p ms ms' -> forall n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m ->
|
|
ms' = VMS (p+1) (push (op n1 n2) s) m
|
|
meta rewrite_def function ibinop_post
|
|
|
|
function ibinop_fun (op:binop) : machine_state -> machine_state =
|
|
fun ms -> match ms with
|
|
| VMS p (Cons n2 (Cons n1 s)) m -> VMS (p+1) (push (op n1 n2) s) m
|
|
| _ -> ms
|
|
end
|
|
meta rewrite_def function ibinop_fun
|
|
|
|
let create_binop (code_b:code) (ghost op:binop) : hl 'a
|
|
requires { forall c p. codeseq_at c p code_b ->
|
|
forall n1 n2 s m. transition c (VMS p (push n2 (push n1 s)) m)
|
|
(VMS (p+1) (push (op n1 n2) s) m) }
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> ibinop_post op }
|
|
ensures { result.code.length --> code_b.length }
|
|
= hoare ibinop_pre ($ ifunf ibinop_pre code_b op.ibinop_fun) op.ibinop_post
|
|
|
|
constant plus : binop = fun x y -> x + y
|
|
meta rewrite_def function plus
|
|
|
|
constant sub : binop = fun x y -> x - y
|
|
meta rewrite_def function sub
|
|
|
|
constant mul : binop = fun x y -> x * y
|
|
meta rewrite_def function mul
|
|
|
|
let iaddf () : hl 'a
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> ibinop_post plus }
|
|
ensures { result.code.length --> 1 }
|
|
= create_binop iadd plus
|
|
|
|
let isubf () : hl 'a
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> ibinop_post sub }
|
|
ensures { result.code.length --> 1 }
|
|
= create_binop isub sub
|
|
|
|
let imulf () : hl 'a
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> ibinop_post mul }
|
|
ensures { result.code.length --> 1 }
|
|
= create_binop imul mul
|
|
|
|
(* Inil spec *)
|
|
function inil_post : post 'a =
|
|
fun _ _ ms ms' -> ms = ms'
|
|
meta rewrite_def function inil_post
|
|
|
|
let inil () : hl 'a
|
|
ensures { result.pre --> trivial_pre }
|
|
ensures { result.post --> inil_post }
|
|
ensures { result.code.length --> 0 }
|
|
= { pre = trivial_pre; code = Nil; post = inil_post }
|
|
|
|
(* Ibranch specification *)
|
|
function ibranch_post (ofs: ofs) : post 'a =
|
|
fun _ 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:ofs) : machine_state -> machine_state =
|
|
fun ms -> let (VMS p s m) = ms in VMS (p+1+ofs) s m
|
|
meta rewrite_def function ibranch_fun
|
|
|
|
let ibranchf (ofs:ofs) : hl 'a
|
|
ensures { result.pre --> trivial_pre }
|
|
ensures { result.post --> ibranch_post ofs }
|
|
ensures { result.code.length --> 1 }
|
|
= 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:ofs) : post 'a =
|
|
fun _ 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:ofs) : machine_state -> machine_state =
|
|
fun 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
|
|
meta rewrite_def function icjump_fun
|
|
|
|
let create_cjump (code_cd:code) (ghost cond:cond) (ghost ofs:ofs) : hl 'a
|
|
requires { forall c p1 n1 n2 s m. codeseq_at c p1 code_cd ->
|
|
let p2 = (if cond n1 n2 then p1 + ofs + 1 else p1 + 1) in
|
|
transition c (VMS p1 (push n2 (push n1 s)) m) (VMS p2 s m) }
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> icjump_post cond ofs }
|
|
ensures { result.code.length --> code_cd.length }
|
|
= 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) *)
|
|
constant beq : cond = fun x y -> x = y
|
|
meta rewrite_def function beq
|
|
|
|
constant bne : cond = fun x y -> x <> y
|
|
meta rewrite_def function bne
|
|
|
|
constant ble : cond = fun x y -> x <= y
|
|
meta rewrite_def function ble
|
|
|
|
constant bgt : cond = fun x y -> x > y
|
|
meta rewrite_def function bgt
|
|
|
|
let ibeqf (ofs:ofs) : hl 'a
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> icjump_post beq ofs }
|
|
ensures { result.code.length --> 1 }
|
|
= create_cjump (ibeq ofs) beq ofs
|
|
|
|
let ibnef (ofs:ofs) : hl 'a
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> icjump_post bne ofs }
|
|
ensures { result.code.length --> 1 }
|
|
= create_cjump (ibne ofs) bne ofs
|
|
|
|
let iblef (ofs:ofs) : hl 'a
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> icjump_post ble ofs }
|
|
ensures { result.code.length --> 1 }
|
|
= create_cjump (ible ofs) ble ofs
|
|
|
|
let ibgtf (ofs:ofs) : hl 'a
|
|
ensures { result.pre --> ibinop_pre }
|
|
ensures { result.post --> icjump_post bgt ofs }
|
|
ensures { result.code.length --> 1 }
|
|
= create_cjump (ibgt ofs) bgt ofs
|
|
|
|
(* Isetvar specification *)
|
|
constant isetvar_pre : pre 'a =
|
|
fun _ p ms -> exists n s m. ms = VMS p (push n s) m
|
|
meta rewrite_def function isetvar_pre
|
|
|
|
function isetvar_post (x:id) : post 'a =
|
|
fun _ p ms ms' -> forall s n m.
|
|
ms = VMS p (push n s) m -> ms' = VMS (p+1) s m[x <- n]
|
|
meta rewrite_def function isetvar_post
|
|
|
|
function isetvar_fun (x:id) : machine_state -> machine_state =
|
|
fun ms -> match ms with
|
|
| VMS p (Cons n s) m -> VMS (p+1) s m[x <- n]
|
|
| _ -> ms
|
|
end
|
|
meta rewrite_def function isetvar_fun
|
|
|
|
let isetvarf (x: id) : hl 'a
|
|
ensures { result.pre --> isetvar_pre }
|
|
ensures { result.post --> isetvar_post x }
|
|
ensures { result.code.length --> 1 }
|
|
= let c = $ ifunf isetvar_pre (isetvar x) (isetvar_fun x) in
|
|
hoare isetvar_pre c (isetvar_post x)
|
|
|
|
end
|