programs: no more optimization for singleton record types

parent fe31fcaf
......@@ -135,7 +135,8 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
encoding_decorate encoding_bridge \
encoding_explicit encoding_guard encoding_sort \
encoding_instantiate simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon
introduction abstraction close_epsilon lift_epsilon \
eval_match
LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa cvc3
......
......@@ -3,7 +3,7 @@ module M
use import int.Int
use import module ref.Ref
parameter incr : x:ref int -> { } unit writes x { x = old x + 1 }
parameter incr : x:ref int -> { } unit writes x { !x = old !x + 1 }
parameter x : ref int
......@@ -17,14 +17,14 @@ let test_and_1 () =
{ result = 1 }
let test_and_2 () =
{ x <> 0 }
{ !x <> 0 }
if id_not_0 !x >= 1 && !x <= 1 then !x else 0+1
{ result = 1 }
let test_or_1 () =
{ }
if (incr x; !x > 0) || !x < 0 then 1 else 2
{ result = 1 -> x <> 0 }
{ result = 1 -> !x <> 0 }
let test_or_2 () =
{ }
......@@ -34,17 +34,17 @@ let test_or_2 () =
let test_not_1 () =
{ }
if not (!x = 0) then x := 0
{ x = 0 }
{ !x = 0 }
let test_not_2 () =
{ x <= 0 }
while not (!x = 0) do invariant { x <= 0 } incr x done
{ x = 0 }
{ !x <= 0 }
while not (!x = 0) do invariant { !x <= 0 } incr x done
{ !x = 0 }
let test_all_1 () =
{ }
(!x >= 0 && not (!x = 0) || !x >= 1)
{ result=True <-> x>=1 }
{ result=True <-> !x>=1 }
(* from Cesar Munoz's CD3D *)
......@@ -58,7 +58,7 @@ parameter sq : x:int -> {} int { result = x*x }
let test_cd3d () =
{ true }
if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d then 1 else 2
{ result=1 -> vx=0 and vy=0 }
{ result=1 -> !vx=0 and !vy=0 }
end
......
......@@ -11,7 +11,7 @@ let f (n : int) : int =
try
while (!i > 0) do
invariant { true }
variant { i }
variant { !i }
if (!i <= 10) then raise Break;
i := !i - 1
done
......@@ -22,3 +22,9 @@ let f (n : int) : int =
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/exceptions"
End:
*)
......@@ -48,17 +48,17 @@ use import module ref.Ref
parameter x : ref int
let p7 () =
{} begin x := 1; raise E; x := 2 end { false } | E -> { x = 1 }
{} begin x := 1; raise E; x := 2 end { false } | E -> { !x = 1 }
let p8 () =
{}
begin x := 1; raise (F !x); x := 2 end
{ false } | F -> { x = 1 and result = 1 }
{ false } | F -> { !x = 1 and result = 1 }
let p9 () =
{}
(raise (F begin x := 1; !x end) : unit)
{ false } | F -> { x = 1 and result = 1 }
{ false } | F -> { !x = 1 and result = 1 }
(* try / with *)
......@@ -82,7 +82,7 @@ let p13 () =
with E -> x := 2
| F _ -> x := 3
end
{ x = 2 }
{ !x = 2 }
let p13a () =
{}
......@@ -92,7 +92,7 @@ let p13a () =
with E ->
x := 0
end
{ x <> 1 }
{ !x <> 1 }
exception E1
exception E2
......@@ -106,17 +106,17 @@ let p14 () =
if !x = 3 then raise E3;
raise E : unit
end
{ false } | E1 -> { x = 1 } | E2 -> { x = 2 } | E3 -> { x = 3 }
| E -> { x <> 1 and x <> 2 and x <> 3 }
{ false } | E1 -> { !x = 1 } | E2 -> { !x = 2 } | E3 -> { !x = 3 }
| E -> { !x <> 1 and !x <> 2 and !x <> 3 }
let p15 () =
{}
if !x = 0 then raise E else (x := 0; raise (F !x)) : unit
{ false } | E -> { x=0 } | F -> { result=0 }
{ false } | E -> { !x=0 } | F -> { result=0 }
let p16 () = {} if !x = 0 then (x:=1; raise E) { x<>0 } | E -> { x=1 }
let p16 () = {} if !x = 0 then (x:=1; raise E) { !x<>0 } | E -> { !x=1 }
let p17 () = {} (x := 0; (raise E; x := 1)) { false } | E -> { x=0 }
let p17 () = {} (x := 0; (raise E; x := 1)) { false } | E -> { !x=0 }
end
......
......@@ -7,10 +7,10 @@ use import module ref.Ref
let test1 () =
let x = ref 0 in
for i = 1 to 10 do
invariant { x = i-1 }
invariant { !x = i-1 }
x := !x + 1
done;
assert { x = 10 }
assert { !x = 10 }
(* we don't even enter *)
let test2 () =
......@@ -18,7 +18,7 @@ let test2 () =
for i = 2 to 1 do
x := 1
done;
assert { x = 0 }
assert { !x = 0 }
exception E
......@@ -50,17 +50,17 @@ let test4 x =
let test1d () =
let x = ref 11 in
for i = 10 downto 1 do
invariant { x = i+1 }
invariant { !x = i+1 }
x := !x - 1
done;
assert { x = 1 }
assert { !x = 1 }
let test2d () =
let x = ref 0 in
for i = 1 downto 2 do
x := 1
done;
assert { x = 0 }
assert { !x = 0 }
let test3d () =
{ }
......
......@@ -8,29 +8,29 @@ use import module ref.Ref
parameter i : ref int
let loop1 (u:unit) =
{ i <= 10 }
{ !i <= 10 }
while !i < 10 do
invariant { i <= 10 } variant { 10 - i }
invariant { !i <= 10 } variant { 10 - !i }
i := !i + 1
done
{ i = 10 }
{ !i = 10 }
(** 2. The same loop, followed by a function call. *)
parameter x: ref int
let negate (u:unit) = {} x := - !x { x = - (old x) }
let negate (u:unit) = {} x := - !x { !x = - (old !x) }
let loop2 (u:unit) =
{ x <= 10 }
{ !x <= 10 }
begin
while !x < 10 do invariant { x <= 10 } variant { 10 - x }
while !x < 10 do invariant { !x <= 10 } variant { 10 - !x }
x := !x + 1
done;
assert { x = 10 };
assert { !x = 10 };
if !x > 0 then (negate ());
assert { x = -10 }
assert { !x = -10 }
end
{}
......
......@@ -7,20 +7,20 @@ module M
parameter r : ref int
parameter f1 : y:int ->
{} unit writes r { q1 r (old r) y }
{} unit writes r { q1 !r (old !r) y }
let g1 () = {} f1 !r { q1 r (old r) (old r) }
let g1 () = {} f1 !r { q1 !r (old !r) (old !r) }
logic foo int : int
logic q int int int
parameter f : t:ref int -> x:int ->
{} unit writes t { q t (old t) x }
{} unit writes t { q !t (old !t) x }
let g (t:ref int) =
{}
f t (foo !t)
{ q t (old t) (foo (old t)) }
{ q !t (old !t) (foo (old !t)) }
end
......
......@@ -11,13 +11,13 @@ parameter x : ref int
(* basic stuff: assignment, sequence and local variables *)
let p1 () = { q (x+1) } begin x := !x + 1 end { q x }
let p1 () = { q (!x+1) } begin x := !x + 1 end { q !x }
let p2 () = { q 7 } begin x := 3 + 4 end { q x }
let p2 () = { q 7 } begin x := 3 + 4 end { q !x }
let p3 () = {} begin x := !x + 1; x := !x + 2 end { x = (old x) + 3 }
let p3 () = {} begin x := !x + 1; x := !x + 2 end { !x = (old !x) + 3 }
let p4 () = {} begin x := 7; x := 2 * !x end { x = 14 }
let p4 () = {} begin x := 7; x := 2 * !x end { !x = 14 }
let p5 () = {} 3 + 4 { result = 7 }
......@@ -28,14 +28,14 @@ let p7 () = {} 3 + (let a = 4 in a + a) { result = 11 }
(* side effects in function arguments *)
let p8 () =
{ q (x+1) } 3 + begin x := !x + 1; !x end { q x and result = (old x) + 4 }
{ q (!x+1) } 3 + begin x := !x + 1; !x end { q !x and result = (old !x) + 4 }
(* evaluation order (argument first) *)
let p9 () =
{} begin x := 1; 1 end + begin x := 2; 1 end { result = 2 and x = 2 }
{} begin x := 1; 1 end + begin x := 2; 1 end { result = 2 and !x = 2 }
let p9a () = {} begin x := 1; 1 end + 1 { result = 2 and x = 1 }
let p9a () = {} begin x := 1; 1 end + 1 { result = 2 and !x = 1 }
(* function with a post-condition *)
......@@ -49,19 +49,19 @@ let p11a () = {} let a = (fsucc 1) in a + a { result = 4 }
(* function with a post-condition and side-effects *)
parameter incrx : unit -> { } unit writes x { x = (old x) + 1 }
parameter incrx : unit -> { } unit writes x { !x = (old !x) + 1 }
let p12 () = { x = 0 } incrx () { x = 1 }
let p12 () = { !x = 0 } incrx () { !x = 1 }
let p13 () = {} begin incrx (); incrx () end { x = (old x) + 2 }
let p13 () = {} begin incrx (); incrx () end { !x = (old !x) + 2 }
let p13a () = {} incrx (incrx ()) { x = (old x) + 2 }
let p13a () = {} incrx (incrx ()) { !x = (old !x) + 2 }
(* function with side-effects, result and post-condition *)
parameter incrx2 : unit -> { } int writes x { x = old x + 1 and result = x }
parameter incrx2 : unit -> { } int writes x { !x = old !x + 1 and result = !x }
let p14 () = { x = 0 } incrx2 () { result = 1 }
let p14 () = { !x = 0 } incrx2 () { result = 1 }
end
......
......@@ -14,33 +14,33 @@ let rec f1 (x:int) : int variant { x } =
parameter x : ref int
let rec f2 (u:unit) : unit variant { x } =
{ x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { x = 0 }
let rec f2 (u:unit) : unit variant { !x } =
{ !x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { !x = 0 }
(** 3. With effects and a pure argument *)
let rec f3 (a:int) : unit variant { a } =
{ a >= 0 }
if a > 0 then begin x := !x + 1; (f3 (a-1)) end
{ x = old x + a }
{ !x = old !x + a }
(** 4. With effects and a reference as argument *)
let rec f4 (a:ref int) : unit variant { a } =
{ a >= 0 }
let rec f4 (a:ref int) : unit variant { !a } =
{ !a >= 0 }
if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
{ x = old x + old a }
{ !x = old !x + old !a }
(** 5. The acid test:
partial application of a recursive function with effects *)
let rec f5 (a b:ref int) variant { a } =
{ a >= 0 }
let rec f5 (a b:ref int) variant { !a } =
{ !a >= 0 }
if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
{ result = old a + old b }
{ result = old !a + old !b }
let test_f5 () =
{ x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old x }
{ !x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
end
......
......@@ -10,7 +10,7 @@ parameter b1 : ref int
parameter b2 : ref int
let f () =
{} b := 1 - !b; !b { result = b and b = 1 - old b }
{} b := 1 - !b; !b { result = !b and !b = 1 - old !b }
let k () =
{}
......@@ -19,7 +19,7 @@ let k () =
b1 := (1 - (f ())) + (f ());
b2 := (f ()) * (1 - (f ()))
end
{ b1 = 0 and b2 = 1 }
{ !b1 = 0 and !b2 = 1 }
end
......
......@@ -11,7 +11,7 @@ module M
v:int ->
{}
bool writes x
{ x = v and if result=True then x = 0 else x <> 0 }
{ !x = v and if result=True then !x = 0 else !x <> 0 }
let p () = {} if set_and_test_zero 0 then 1 else 2 { result = 1 }
......@@ -19,31 +19,31 @@ module M
v:int ->
{}
bool writes x
{ x = v and if result=True then x <> 0 else x = 0 }
{ !x = v and if result=True then !x <> 0 else !x = 0 }
let p2 (y:ref int) =
{ y >= 0 }
{ !y >= 0 }
while set_and_test_nzero !y do
invariant { y >= 0 } variant { y }
invariant { !y >= 0 } variant { !y }
y := !y - 1
done
{ y = 0 }
{ !y = 0 }
let p3 (y:ref int) =
{ y >= 0 }
{ !y >= 0 }
while let b = set_and_test_nzero !y in b do
invariant { y >= 0 } variant { y }
invariant { !y >= 0 } variant { !y }
y := !y - 1
done
{ y = 0 }
{ !y = 0 }
let p4 (y:ref int) =
{ y >= 1 }
{ !y >= 1 }
while begin y := !y - 1; (set_and_test_nzero !y) end do
invariant { y >= 1 } variant { y }
invariant { !y >= 1 } variant { !y }
()
done
{ y = 0 }
{ !y = 0 }
end
......
......@@ -5,7 +5,7 @@ use import module ref.Ref
parameter x : ref int
parameter f : unit -> { } unit writes x { x = 1 - old x }
parameter f : unit -> { } unit writes x { !x = 1 - old !x }
let p () =
begin
......@@ -13,7 +13,7 @@ let p () =
let t = () in ();
(f ());
(f ());
assert { x = at x Init };
assert { !x = at !x Init };
()
end
......
......@@ -152,11 +152,11 @@ theory map.Map
syntax type map "(Array %1 %2)"
meta "encoding : lskept" logic get
meta "encoding : lskept" logic set
meta "encoding : lskept" logic create_const
meta "encoding : lskept" logic const
syntax logic get "(select %1 %2)"
syntax logic set "(store %1 %2 %3)"
syntax logic create_const "(const[%t0] %1)"
syntax logic const "(const[%t0] %1)"
end
......
......@@ -23,11 +23,11 @@ module Algo63
a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ m < n }
unit writes a i j
{ m <= j and j < i and i <= n and permut_sub (old a) a m n and
{ m <= !j and !j < !i and !i <= n and permut_sub (old a) a m n and
exists x:int.
(forall r:int. m <= r <= j -> a[r] <= x) and
(forall r:int. j < r < i -> a[r] = x) and
(forall r:int. i <= r <= n -> a[r] >= x) }
(forall r:int. m <= r <= !j -> a[r] <= x) and
(forall r:int. !j < r < !i -> a[r] = x) and
(forall r:int. !i <= r <= n -> a[r] >= x) }
end
......
......@@ -30,11 +30,11 @@ module Algo64
a:array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ 0 <= m < n < length a }
unit writes a i j
{ m <= j < i <= n and permut_sub (old a) a m n and
{ m <= !j < !i <= n and permut_sub (old a) a m n and
exists x:int.
(forall r:int. m <= r <= j -> a[r] <= x) and
(forall r:int. j < r < i -> a[r] = x) and
(forall r:int. i <= r <= n -> a[r] >= x) }
(forall r:int. m <= r <= !j -> a[r] <= x) and
(forall r:int. !j < r < !i -> a[r] = x) and
(forall r:int. !i <= r <= n -> a[r] >= x) }
(* Algorithm 64 *)
......
......@@ -25,11 +25,11 @@ module Algo65
a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ 0 <= m < n < length a }
unit writes a i j
{ m <= j < i <= n and permut_sub (old a) a m n and
{ m <= !j < !i <= n and permut_sub (old a) a m n and
exists x:int.
(forall r:int. m <= r <= j -> a[r] <= x) and
(forall r:int. j < r < i -> a[r] = x) and
(forall r:int. i <= r <= n -> a[r] >= x) }
(forall r:int. m <= r <= !j -> a[r] <= x) and
(forall r:int. !j < r < !i -> a[r] = x) and
(forall r:int. !i <= r <= n -> a[r] >= x) }
(* Algorithm 65 (fixed version) *)
......
......@@ -16,18 +16,18 @@ module M
let insertion_sort () =
{ inv a and
(* ghost *) loop1 = 0 and loop2 = 0 }
(* 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 }
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 }
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];
......@@ -36,7 +36,7 @@ module M
done;
incr i
done
{ loop1 = 9 and loop2 <= 45 }
{ !loop1 = 9 and !loop2 <= 45 }
end
......@@ -48,9 +48,9 @@ module ARM
(* memory *)
parameter mem : ref (map int int)
parameter mem_ldr : a:int -> {} int reads mem.contents { result = mem[a] }
parameter mem_ldr : a:int -> {} int reads mem.contents { result = !mem[a] }
parameter mem_str : a:int -> v:int ->
{} int writes mem.contents { mem = (old mem)[a <- v] }
{} int writes mem.contents { !mem = (old !mem)[a <- v] }
(* data segment *)
(*
......@@ -70,9 +70,9 @@ module ARM
parameter pc : ref int (* pc *)
parameter ldr :
r:ref int -> a:int -> {} unit reads mem.contents writes r.contents { r = mem[a] }
r:ref int -> a:int -> {} unit reads mem.contents writes r.contents { !r = !mem[a] }
parameter str :
r:ref int -> a:int -> {} unit reads r.contents writes mem.contents { mem = (old mem)[a <- r] }
r:ref int -> a:int -> {} unit reads r.contents writes mem.contents { !mem = (old !mem)[a <- !r] }
(* condition flags *)
parameter le : ref bool
......@@ -80,7 +80,7 @@ module ARM
parameter cmp : r:ref int -> v:int ->
{}
unit reads r.contents writes le.contents
{ le=True <-> r <= v }
{ !le=True <-> !r <= v }
end
......@@ -121,18 +121,18 @@ module InsertionSortExample
2 <= mem[fp - 16] <= 11 and l4 = mem[fp-16] - 2 and inv mem
let path_init_l2 () =
{ separation fp and inv mem }
{ separation !fp and inv !mem }
(* ghost *) l4 := 0; l7 := 0;
r3 := 2;
str r3 (!fp - 16)
{ inv_l2 mem fp l4 }
{ inv_l2 !mem !fp !l4 }
let path_l2_exit () =
{ separation fp and inv_l2 mem fp l4 }
{ separation !fp and inv_l2 !mem !fp !l4 }
ldr r3 (!fp - 16);
cmp r3 10;
assume { le = False }
{ l4 = 9 }
assume { !le = False }
{ !l4 = 9 }
end
......
......@@ -21,11 +21,11 @@ module M
let u = ref (length a - 1) in
while !l <= !u do
invariant {
0 <= l and u < length a and
forall i : int. 0 <= i < length a -> a[i] = v -> l <= i <= u }
variant { u - l }
0 <= !l and !u < length a and
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = !l + div (!u - !l) 2 in
assert { l <= m <= u };
assert { !l <= m <= !u };
if a[m] < v then
l := m + 1
else if a[m] > v then
......
......@@ -33,14 +33,14 @@ module M1
let binary_search (t : pointer) (n : int) (v : int) =
{ forall k1 k2:int.
0 <= k1 <= k2 <= n-1 -> get mem t k1 <= get mem t k2 }
0 <= k1 <= k2 <= n-1 -> get !mem t k1 <= get !mem t k2 }
try
let l = ref 0 in
let u = ref (n-1) in
while !l <= !u do
invariant { 0 <= l and u <= n-1 and
forall k:int. 0 <= k < n -> get mem t k = v -> l <= k <= u }
variant { u-l }
invariant { 0 <= !l and !u <= n-1 and
forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u }
variant { !u - !l }
let m = div (!l + !u) 2 in
if get !mem t m < v then l := m + 1
else if get !mem t m > v then u := m - 1
......@@ -50,8 +50,8 @@ module M1
with Return r ->
r
end
{ (result >= 0 and get mem t result = v) or
(result = -1 and forall k:int. 0<=k<n -> get mem t k <> v) }
{ (result >= 0 and get !mem t result = v) or
(result = -1 and forall k:int. 0<=k<n -> get !mem t k <> v) }
end
......@@ -78,23 +78,23 @@ module M2
logic block_size memory pointer : int
parameter get_ :p : pointer -> ofs : int ->
{ 0 <= ofs < block_size mem p }
{ 0 <= ofs < block_size !mem p }
int reads mem