Commit cb490e22 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new module Refint for integer references

new program arm.mlw: ARM verification experiments in progress
parent 8fce4d64
(* experiments related to ARM program verification *)
module M
use import module stdlib.Refint
use import module stdlib.Array
parameter a : array int
logic inv (a : t int int) =
a[0] = 0 and length a = 11 and forall k:int. 1 <= k <= 10 -> 0 < a[k]
parameter loop1 : ref int
parameter loop2 : ref int
let insertion_sort () =
{ inv a and
(* ghost *) loop1 = 0 and loop2 = 0 }
let i = ref 2 in
while !i <= 10 do
invariant { 2 <= i <= 11 and inv a and
(* ghost *) loop1 = i - 2 and 2 * loop2 <= (i-2) * (i-1) }
variant { 10 - i }
(* ghost *) incr loop1;
let j = ref !i in
while a[!j] < a[!j - 1] do
invariant { 1 <= j <= i and inv a and
(* ghost *) 2 * loop2 <= (i-2) * (i-1) + 2*(i-j) }
variant { j }
(* ghost *) incr loop2;
let temp = a[!j] in
a[!j <- a[!j - 1]];
a[!j - 1 <- temp];
decr j
done;
incr i
done
{ loop1 = 9 and loop2 <= 45 }
end
module ARM
use export int.Int
use export array.Array
use export module stdlib.Ref
(* memory *)
parameter mem : ref (t int int)
parameter mem_ldr : a:int -> {} int reads mem { result = mem[a] }
parameter mem_str : a:int -> v:int ->
{} int writes mem { mem = (old mem)[a <- v] }
(* data segment *)
(*
parameter data : ref (t int int)
parameter data_ldr : a:int -> {} int reads data { result = data[a] }
parameter data_str :
a:int -> v:int -> {} int writes data { data = (old data)[a <- v] }
*)
(* registers *)
parameter r0 : ref int
parameter r1 : ref int
parameter r2 : ref int
parameter r3 : ref int
(* ... *)
parameter fp : ref int
parameter pc : ref int (* pc *)
parameter ldr :
r:ref int -> a:int -> {} unit reads mem writes r { r = mem[a] }
parameter str :
r:ref int -> a:int -> {} unit reads r writes mem { mem = (old mem)[a <- r] }
(* condition flags *)
parameter le : ref bool
parameter cmp : r:ref int -> v:int ->
{}
unit reads r writes le
{ le=True <-> r <= v }
end
module InsertionSortExample
use import module ARM
(* i = fp-16
j = fp-20
temp = fp-24 *)
parameter l4 : ref int
parameter l7 : ref int
logic a : int
(* stack and data segment do not overlap *)
logic separation (fp : int) = a+10 < fp-24
logic inv (mem : t int int) =
mem[a] = 0 and forall k:int. 1 <= k <= 10 -> 0 < mem[a + k]
logic inv_l2 (mem : t int int) (fp : int) (l4 : int) =
2 <= mem[fp - 16] <= 11 and l4 = mem[fp-16] - 2 and inv mem
let path_init_l2 () =
{ separation fp and inv mem }
(* ghost *) l4 := 0; l7 := 0;
r3 := 2;
str r3 (!fp - 16)
{ inv_l2 mem fp l4 }
let path_l2_exit () =
{ separation fp and inv_l2 mem fp l4 }
ldr r3 (!fp - 16);
cmp r3 10;
assume { le = False }
{ l4 = 9 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/arm.gui"
End:
*)
......@@ -13,6 +13,17 @@ module Ref
end
module Refint
use export int.Int
use export module Ref
parameter incr : r:ref int -> {} unit writes r { r = old r + 1 }
parameter decr : r:ref int -> {} unit writes r { r = old r - 1 }
end
(* Arrays *)
module Array
......
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