Commit d8311c4d authored by Andrei Paskevich's avatar Andrei Paskevich

move tests out of the standard library files

they now live in examples/tests/

also, simplify bench/bench script
parent 5d77d51f
......@@ -78,67 +78,39 @@ list_stuff () {
}
echo "=== Checking drivers ==="
drivers drivers
echo ""
#echo "=== Parsing good files ==="
#goods bench/typing/bad --parse-only
#goods bench/typing/good --parse-only
#goods examples/logic --parse-only
#goods examples/bitvectors "--parse-only -I examples/bitvectors"
#echo ""
echo "=== Type-checking bad files ==="
goods bench/typing/bad --parse-only
bads bench/typing/bad --type-only
echo "=== Checking theories ==="
goods theories
echo ""
echo "=== Type-checking theories ==="
goods theories --type-only
echo "=== Checking modules ==="
goods modules
echo ""
echo "=== Type-checking good files ==="
goods bench/typing/good --type-only
goods examples/logic --type-only
goods examples/bitvectors "--type-only -I examples/bitvectors"
echo ""
#echo "=== Parsing programs ==="
#goods bench/programs/bad-typing --parse-only
#goods bench/programs/good --parse-only
#goods examples --parse-only
#goods examples/in_progress --parse-only
#goods examples/foveoos11-cm --parse-only
#goods examples/hoare_logic --parse-only
#goods examples/vacid_0_binary_heaps "--parse-only -I examples/vacid_0_binary_heaps"
#echo ""
echo "=== Type-checking bad programs ==="
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
goods bench/programs/bad-typing --parse-only
bads bench/typing/bad --type-only
bads bench/programs/bad-typing --type-only
echo ""
echo "=== Type-checking modules ==="
goods modules --type-only
echo ""
#echo "=== Type-checking good programs ==="
#goods bench/programs/good --type-only
#goods examples --type-only
#goods examples/in_progress --type-only
#goods examples/foveoos11-cm --type-only
#goods examples/hoare_logic --type-only
#goods examples/vacid_0_binary_heaps "--type-only -I examples/vacid_0_binary_heaps"
#echo ""
echo "=== VC generation on good programs ==="
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/in_progress
goods examples/foveoos11-cm
goods examples/hoare_logic
goods examples/vacid_0_binary_heaps "-I examples/vacid_0_binary_heaps"
goods examples/bitvectors "-I examples/bitvectors"
goods examples/in_progress
echo ""
echo "=== Checking drivers ==="
drivers drivers
echo ""
echo "=== Checking valid goals ==="
......
......@@ -47,7 +47,8 @@ run_dir () {
echo '</ul>' >> $HTML
}
echo "=== Tests Provers ==="
echo "=== Tests ==="
run_dir tests
run_dir tests-provers
echo ""
......
......@@ -11,8 +11,9 @@ use import int.Int
exception E
let rec f (x:int) : int =
if x = 42 then raise E else
let rec f (x:int) : int
raises { E }
= if x = 42 then raise E else
try
let n = f (x-1) in
n
......
......@@ -13,8 +13,7 @@ use import int.Int
exception MyExc
let rec f (x:int) : int = raises { MyExc } raise MyExc
with g (x:int) : int = raises { MyExc } f x
let rec f (x:int) : int raises { MyExc } = raise MyExc
with g (x:int) : int raises { MyExc } = f x
end
......@@ -13,8 +13,7 @@ module T
exception MyExc
let rec f (a:t) : t = raise MyExc
let rec f (a:t) : t raises { MyExc } = raise MyExc
with g (a:t) : t = try (f a) with MyExc -> a end
end
......@@ -14,8 +14,7 @@ module T
exception MyExc
let rec f (x:t) : t = raise MyExc
with g (x:t) : t ensures { true } = f x
let rec f (x:t) : t raises { MyExc } = raise MyExc
with g (x:t) : t raises { MyExc } ensures { true } = f x
end
......@@ -53,8 +53,8 @@ run_dir () {
done
}
echo "=== Tests Provers ==="
echo "=== Tests ==="
run_dir tests
run_dir tests-provers
echo ""
......
module TestArray
use import int.Int
use import array.Array
let test_append () =
let a1 = make 17 2 in
assert { a1[3] = 2 };
a1[3] <- 4;
assert { a1[3] = 4 };
let a2 = make 25 3 in
assert { a2[0] = 3 }; (* needed to prove a[17]=3 below *)
let a = append a1 a2 in
assert { length a = 42 };
assert { a[3] = 4 };
assert { a[17] = 3 };
()
let test_fill () =
let a = make 17 True in
fill a 10 4 False;
assert { a[9] = True };
assert { a[10] = False };
assert { a[14] = True }
let test_blit () =
let a1 = make 17 True in
let a2 = make 25 False in
blit a1 10 a2 17 7;
assert { a1[10] = True };
assert { a2[16] = False };
assert { a2[17] = True };
assert { a2[23] = True };
assert { a2[24] = False }
end
theory TestBv32
use import map.BV32
lemma Test1:
let b = bw_and bvzero bvone in nth b 1 = False
lemma Test2:
let b = lsr bvone 16 in nth b 15 = True
lemma Test3:
let b = lsr bvone 16 in nth b 16 = False
lemma Test4:
let b = asr bvone 16 in nth b 15 = True
lemma Test5:
let b = asr bvone 16 in nth b 16 = True
lemma Test6:
let b = asr (lsr bvone 1) 16 in nth b 16 = False
end
module TestHashtbl
use import int.Int
use import list.List
use import hashtbl.Hashtbl
function k1: key
function k2: key
function k3: key
axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3
let test1 () =
let h = create 17 in
add h k1 True;
assert { h[k1] = Cons True Nil };
assert { h[k2] = Nil };
let v1 = find h k1 in
assert { v1 = True };
add h k1 False;
assert { h[k1] = Cons False (Cons True Nil) };
replace h k1 True;
assert { h[k1] = Cons True (Cons True Nil) }
end
module TestMatrix
use import int.Int
use import matrix.Syntax
let test1 () =
let m1 = make 3 3 2 in
assert { m1[(0,0)] = 2 };
m1[(0,0)] <- 4;
assert { m1[(0,0)] = 4 };
assert { m1[(0,1)] = 2 };
assert { m1[(1,0)] = 2 };
()
end
module Test
use import list.List
use import pqueue.Pqueue as P
function v1 : elt
function v2 : elt
axiom values: rel v2 v1 /\ v1 <> v2
let test0 () =
let s = P.create () : P.t in
assert { s.elts = Nil };
let b = P.is_empty s in
assert { b = True };
let n = P.length s in
assert { n = 0 }
let test1 () =
raises { P.Empty }
let s = P.create () in
P.push v1 s;
let x = P.peek s in assert { x = v1 };
P.push v2 s;
let x = P.peek s in assert { x = v2 };
()
end
module TestNoDup
use import set.Fset
use import pqueue.PqueueNoDup as P
function v1 : elt
function v2 : elt
axiom values: rel v2 v1 /\ v1 <> v2
let test0 () =
let s = P.create () : P.t in
assert { s.elts = empty };
let b = P.is_empty s in
assert { b = True };
let n = P.length s in
assert { n = 0 }
let test1 () =
raises { P.Empty }
let s = P.create () in
P.push v1 s;
let x = P.peek s in assert { x = v1 };
P.push v2 s;
let x = P.peek s in assert { x = v2 };
()
end
module Test
use import int.Int
use import list.List
use import queue.Queue
let test0 () =
let s = Queue.create () : Queue.t 'a in
assert { s.elts = Nil };
let b = Queue.is_empty s in
assert { b = True };
let n = Queue.length s in
assert { n = 0 }
let test1 ()
raises { Queue.Empty }
= let s = Queue.create () in
Queue.push 1 s;
let x = Queue.peek s in assert { x = 1 };
Queue.push 2 s;
let x = Queue.peek s in assert { x = 1 };
()
end
module Test
use import random.Random
let test1 () =
init 42;
let x = random_int 10 in
init 42;
let y = random_int 10 in
assert { x = y }
end
theory Test
clone import regexp.Regexp with type char = int
lemma empty_is_empty: forall w: word. not (mem w Empty)
constant a: int = 0
constant b: int = 1
constant c: int = 2
goal G: mem (Cons a (Cons b Nil)) (Concat (Char a) (Star (Char b)))
end
module Test
use import int.Int
use import list.List
use import stack.Stack
let test0 () =
let s = Stack.create () : Stack.t 'a in
assert { s.elts = Nil };
let b = Stack.is_empty s in
assert { b = True };
let n = Stack.length s in
assert { n = 0 }
let test1 () raises { Empty }
= let s = Stack.create () in
Stack.push 1 s;
let x = Stack.top s in assert { x = 1 };
Stack.push 2 s;
let x = Stack.top s in assert { x = 2 };
()
end
......@@ -254,40 +254,3 @@ module NumOf
function numof (a: array elt) (l u: int) : int = num_of a l u
end
module TestArray
use import int.Int
use import Array
let test_append () =
let a1 = make 17 2 in
assert { a1[3] = 2 };
a1[3] <- 4;
assert { a1[3] = 4 };
let a2 = make 25 3 in
assert { a2[0] = 3 }; (* needed to prove a[17]=3 below *)
let a = append a1 a2 in
assert { length a = 42 };
assert { a[3] = 4 };
assert { a[17] = 3 };
()
let test_fill () =
let a = make 17 True in
fill a 10 4 False;
assert { a[9] = True };
assert { a[10] = False };
assert { a[14] = True }
let test_blit () =
let a1 = make 17 True in
let a2 = make 25 False in
blit a1 10 a2 17 7;
assert { a1[10] = True };
assert { a2[16] = False };
assert { a2[17] = True };
assert { a2[23] = True };
assert { a2[24] = False }
end
......@@ -61,111 +61,3 @@ module Hashtbl
*)
end
module TestHashtbl
use import int.Int
use import list.List
use import Hashtbl
function k1: key
function k2: key
function k3: key
axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3
let test1 () =
let h = create 17 in
add h k1 True;
assert { h[k1] = Cons True Nil };
assert { h[k2] = Nil };
let v1 = find h k1 in
assert { v1 = True };
add h k1 False;
assert { h[k1] = Cons False (Cons True Nil) };
replace h k1 True;
assert { h[k1] = Cons True (Cons True Nil) }
end
module HashtblImpl
use import int.Int
use import int.ComputerDivision
use import list.List
use import list.Mem
use import array.Array
type key
function hash key : int
axiom hash_nonneg: forall k: key. 0 <= hash k
function bucket (k: key) (n: int) : int = mod (hash k) n
lemma bucket_bounds:
forall n: int. 0 < n ->
forall k: key. 0 <= bucket k n < n
type t 'a = { mutable size: int; (* total number of elements *)
mutable data: array (list (key, 'a)); }
invariant { let n = Array.length self.data in
0 < n /\
forall i: int. 0 <= i < n ->
forall k: key, v: 'a. mem (k,v) self.data[i] -> bucket k n = i }
function extract (k: key) (l: list (key, 'a)) : list 'a = match l with
| Nil -> Nil
| Cons (k', v) r -> if k = k' then Cons v (extract k r) else extract k r
end
function ([]) (t: t 'a) (k: key): list 'a =
extract k (Array.get t.data (bucket k (length t.data)))
let create (n:int) : t 'a
requires { 1 <= n }
ensures { forall k: key. result[k] = Nil }
= { size = 0; data = Array.make n Nil }
let clear (h: t 'a)
ensures { forall k: key. h[k] = Nil }
= h.size <- 0;
Array.fill h.data 0 (Array.length h.data) Nil
let resize (h: t 'a)
ensures { forall k: key. h[k] = (old h)[k] }
= let odata = h.data in
let osize = Array.length odata in
let nsize = 2 * osize + 1 in
let ndata = Array.make nsize Nil in
let rec rehash l = match l with
| Nil -> ()
| Cons (k, v) r ->
let b = bucket k nsize in
ndata[b] <- Cons (k, v) (Array.([]) ndata b);
rehash r
end
in
for i = 0 to osize - 1 do rehash (Array.([]) odata i) done;
h.data <- ndata
lemma extract_neq:
forall k k': key, v: 'a, l: list (key, 'a).
k <> k' -> extract k' l = extract k' (Cons (k, v) l)
let add (h: t 'a) (k: key) (v: 'a)
ensures { h[k] = Cons v (old h)[k] /\
forall k': key. k' <> k -> h[k'] = (old h)[k'] }
= let b = bucket k (Array.length h.data) in
h.data[b] <- Cons (k, v) (Array.([]) h.data b)
(*
let add (h: t 'a) (k: key) (v: 'a) =
ensures { h[k] = Cons v (old h)[k] /\
forall k': key. k' <> k -> h[k'] = (old h)[k'] }
let b = bucket k (Array.length h.data) in
h.data[b] <- Cons (k, v) (Array.([]) h.data b);
if h.size > 2 * Array.length h.data then resize h
*)
end
......@@ -85,20 +85,3 @@ module Syntax
end
(* {2 Test module} *)
module TestMatrix
use import int.Int
use import Syntax
let test1 () =
let m1 = make 3 3 2 in
assert { m1[(0,0)] = 2 };
m1[(0,0)] <- 4;
assert { m1[(0,0)] = 4 };
assert { m1[(0,1)] = 2 };
assert { m1[(1,0)] = 2 };
()
end
......@@ -63,33 +63,6 @@ module Pqueue
end
module Test
use import list.List
use import Pqueue as P
function v1 : elt
function v2 : elt
axiom values: rel v2 v1 /\ v1 <> v2
let test0 () =
let s = P.create () : P.t in
assert { s.elts = Nil };
let b = P.is_empty s in
assert { b = True };
let n = P.length s in
assert { n = 0 }
let test1 () =
let s = P.create () in
P.push v1 s;
let x = P.peek s in assert { x = v1 };
P.push v2 s;
let x = P.peek s in assert { x = v2 };
()
end
(** {2 Simpler interface}
when duplicate elements are not allowed
......@@ -153,30 +126,3 @@ module PqueueNoDup
ensures { result = cardinal q.elts }
end
module TestNoDup
use import set.Fset
use import PqueueNoDup as P
function v1 : elt
function v2 : elt
axiom values: rel v2 v1 /\ v1 <> v2
let test0 () =
let s = P.create () : P.t in
assert { s.elts = empty };
let b = P.is_empty s in
assert { b = True };
let n = P.length s in
assert { n = 0 }
let test1 () =
let s = P.create () in
P.push v1 s;
let x = P.peek s in assert { x = v1 };
P.push v2 s;
let x = P.peek s in assert { x = v2 };
()
end
......@@ -37,26 +37,3 @@ module Queue
end
module Test
use import int.Int
use import list.List
use import Queue
let test0 () =
let s = Queue.create () : Queue.t 'a in
assert { s.elts = Nil };
let b = Queue.is_empty s in
assert { b = True };
let n = Queue.length s in
assert { n = 0 }
let test1 () =
let s = Queue.create () in
Queue.push 1 s;
let x = Queue.peek s in assert { x = 1 };
Queue.push 2 s;
let x = Queue.peek s in assert { x = 1 };
()
end
......@@ -97,16 +97,3 @@ module Random
= random_int s n
end
module Test