Skip to content

Commit b8fa170

Browse files
brianhuffmanbrianhuffman
committed
Update saw-core tuple syntax in heapster-saw/examples.
1 parent aec37ef commit b8fa170

File tree

12 files changed

+88
-79
lines changed

12 files changed

+88
-79
lines changed

‎heapster-saw/examples/arrays.sawcore‎

Lines changed: 31 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -3,39 +3,48 @@ module arrays where
33

44
import Prelude;
55

6+
letRecM_single :
7+
(lrt : LetRecType) ->
8+
(B : sort 0) ->
9+
(lrtToType lrt -> lrtToType lrt) ->
10+
(lrtToType lrt -> CompM B) -> CompM B;
11+
letRecM_single lrt B fn body =
12+
letRecM
13+
(LRT_Cons lrt LRT_Nil) B
14+
(\ (x : lrtToType lrt) -> consTuple (lrtToType lrt) TypeNil (fn x) ())
15+
(\ (x : lrtToType lrt) -> body x);
16+
617
-- The helper function for noErrorsContains0
718
--
819
-- noErrorsContains0H len i v =
920
-- orM (exists x. returnM x) (noErrorsContains0H len (i+1) v)
1021
noErrorsContains0H : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
11-
CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
22+
CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool);
1223
noErrorsContains0H len_top i_top v_top =
13-
letRecM
14-
(LRT_Cons
15-
(LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
16-
LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
17-
LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
18-
LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))))
19-
LRT_Nil)
20-
(BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool)
24+
letRecM_single
25+
(LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
26+
LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
27+
LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
28+
LRT_Ret #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)))))
29+
#(BVVec 64 len_top (Vec 64 Bool), Vec 64 Bool)
2130
(\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
22-
CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
23-
((\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
24-
precondHint
25-
(CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
26-
(and (bvsle 64 0x0000000000000000 i)
27-
(bvsle 64 i 0x0fffffffffffffff))
28-
(orM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
29-
(existsM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
30-
(BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
31-
(returnM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))
32-
(f len (bvAdd 64 i 0x0000000000000001) v))), ()))
31+
CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)) ->
32+
(\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
33+
precondHint
34+
(CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool))
35+
(and (bvsle 64 0x0000000000000000 i)
36+
(bvsle 64 i 0x0fffffffffffffff))
37+
(orM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
38+
(existsM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
39+
#(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
40+
(returnM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)))
41+
(f len (bvAdd 64 i 0x0000000000000001) v))))
3342
(\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
34-
CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
43+
CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)) ->
3544
f len_top i_top v_top);
3645

3746
-- The specification that contains0 has no errors
3847
noErrorsContains0 : (len:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
39-
CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
48+
CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool);
4049
noErrorsContains0 len v =
4150
noErrorsContains0H len 0x0000000000000000 v;

‎heapster-saw/examples/clearbufs.sawcore‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -25,28 +25,28 @@ Mbox_def = Mbox;
2525
(m:Mbox) -> P m;
2626
Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -}
2727

28-
--unfoldMbox : Mbox -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool));
28+
--unfoldMbox : Mbox -> Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool));
2929
primitive
30-
unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool)));
30+
unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> #(Mbox, BVVec 64 len (Vec 64 Bool))));
3131

3232
{-unfoldMbox m =
33-
Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()))
34-
(Left #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()) ())
35-
(\ (m:Mbox) (_:Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #())) (len:Vec 64 Bool) (d:BVVec 64 bv64_16 (Vec 64 Bool)) ->
36-
Right #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()) (m, len, d, ()))
33+
Mbox__rec (\ (_:Mbox) -> Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()))
34+
(Left #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) ())
35+
(\ (m:Mbox) (_:Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #())) (len:Vec 64 Bool) (d:BVVec 64 bv64_16 (Vec 64 Bool)) ->
36+
Right #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) (m, len, d, ()))
3737
m;
3838
-}
3939

4040
primitive
41-
foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len (Vec 64 Bool))) -> Mbox;
41+
foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> #(Mbox, BVVec 64 len (Vec 64 Bool)))) -> Mbox;
4242

43-
--(Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) -> Mbox;
43+
--#(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool))) -> Mbox;
4444
{-
4545
foldMbox =
46-
either #() (Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) Mbox
46+
either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) Mbox
4747
(\ (_:#()) -> Mbox_nil)
48-
(\ (tup : (Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #())) ->
49-
Mbox_cons tup.1 tup.2 tup.3);
48+
(\ (tup : #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #())) ->
49+
Mbox_cons tup.0 tup.1 tup.2);
5050
-}
5151

5252
primitive

‎heapster-saw/examples/global_var.sawcore‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ module GlobalVar where
22

33
import Prelude;
44

5-
acquireLockM : Vec 64 Bool -> CompM (Vec 64 Bool * Vec 64 Bool);
6-
acquireLockM u = returnM (Vec 64 Bool * Vec 64 Bool)
5+
acquireLockM : Vec 64 Bool -> CompM #(Vec 64 Bool, Vec 64 Bool);
6+
acquireLockM u = returnM #(Vec 64 Bool, Vec 64 Bool)
77
(u,u);
88

99
releaseLockM : Vec 64 Bool -> Vec 64 Bool -> CompM (Vec 64 Bool);

‎heapster-saw/examples/iter_linked_list.sawcore‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -27,20 +27,20 @@ ListF__rec : (a b:sort 0) -> (P : ListF a b -> sort 0) ->
2727
(l:ListF a b) -> P l;
2828
ListF__rec a b P f1 f2 l = ListF#rec a b P f1 f2 l;
2929

30-
unfoldListF : (a b:sort 0) -> ListF a b -> Either b (a * ListF a b);
30+
unfoldListF : (a b:sort 0) -> ListF a b -> Either b #(a, ListF a b);
3131
unfoldListF a b l =
32-
ListF__rec a b (\ (_:ListF a b) -> Either b (a * ListF a b))
33-
(\ (x:b) -> Left b (a * ListF a b) x)
34-
(\ (x:a) (l:ListF a b) (_:Either b (a * ListF a b)) ->
35-
Right b (a * ListF a b) (x, l))
32+
ListF__rec a b (\ (_:ListF a b) -> Either b #(a, ListF a b))
33+
(\ (x:b) -> Left b #(a, ListF a b) x)
34+
(\ (x:a) (l:ListF a b) (_:Either b #(a, ListF a b)) ->
35+
Right b #(a, ListF a b) (x, l))
3636
l;
3737

38-
foldListF : (a b:sort 0) -> Either b (a * ListF a b) -> ListF a b;
38+
foldListF : (a b:sort 0) -> Either b #(a, ListF a b) -> ListF a b;
3939
foldListF a b =
40-
either b (a * ListF a b) (ListF a b)
40+
either b #(a, ListF a b) (ListF a b)
4141
(\ (x : b) -> NilF a b x)
42-
(\ (tup : (a * ListF a b)) ->
43-
ConsF a b tup.(1) tup.(2));
42+
(\ (tup : #(a, ListF a b)) ->
43+
ConsF a b tup.0 tup.1);
4444

4545
getListF : (a b:sort 0) -> ListF a b -> b;
4646
getListF a b =

‎heapster-saw/examples/mbox.sawcore‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -31,20 +31,20 @@ Mbox__rec : (P : Mbox -> sort 0) ->
3131
(m:Mbox) -> P m;
3232
Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m;
3333

34-
unfoldMbox : Mbox -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool));
34+
unfoldMbox : Mbox -> Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool));
3535
unfoldMbox m =
36-
Mbox__rec (\ (_:Mbox) -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)))
37-
(Left #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) ())
38-
(\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
39-
Right #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
36+
Mbox__rec (\ (_:Mbox) -> Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)))
37+
(Left #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) ())
38+
(\ (strt:Vec 64 Bool) (len:Vec 64 Bool) (m:Mbox) (_:Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool))) (d:BVVec 64 bv64_128 (Vec 8 Bool)) ->
39+
Right #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
4040
m;
4141

42-
foldMbox : Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
42+
foldMbox : Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
4343
foldMbox =
44-
either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
44+
either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
4545
(\ (_:#()) -> Mbox_nil)
46-
(\ (tup : (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) ->
47-
Mbox_cons tup.1 tup.2 tup.3 tup.(2).(2).(2));
46+
(\ (tup : #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool))) ->
47+
Mbox_cons tup.0 tup.1 tup.2 tup.3);
4848

4949
{-
5050
getMbox : (a : sort 0) -> Mbox a -> a;

‎heapster-saw/examples/memcpy.saw‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
1010
\ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(len,b)), \
1111
\ arg2:eq(llvmword(len)) -o \
1212
\ arg0:[l1]memblock(W,0,len,eqsh(len,b)), arg1:[l2]memblock(rw,0,len,eqsh(len,b))"
13-
"\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
13+
"\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM #(#(), #()) ((),())";
1414

1515

1616
heapster_typecheck_fun env "copy_int"

‎heapster-saw/examples/rust_data.saw‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ heapster_define_opaque_llvmshape env "Vec" 64
105105
// Opaque type for HashMap<T,U>
106106
heapster_define_opaque_llvmshape env "HashMap" 64
107107
"T:llvmshape 64, U:llvmshape 64" "56"
108-
"\\ (T:sort 0) (U:sort 0) -> List (T * U)";
108+
"\\ (T:sort 0) (U:sort 0) -> List #(T, U)";
109109

110110
// BinTree<X> type
111111
heapster_define_rust_type env

‎heapster-saw/examples/rust_data.sawcore‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,17 +3,17 @@ module rust_data where
33

44
import Prelude;
55

6-
unfoldListPermH : (a:sort 0) -> List a -> Either #() (#() * a * List a);
6+
unfoldListPermH : (a:sort 0) -> List a -> Either #() #(#(), a, List a);
77
unfoldListPermH a l =
8-
List__rec a (\ (_:List a) -> Either #() (#() * a * List a))
9-
(Left #() (#() * a * List a) ())
10-
(\ (x:a) (l:List a) (_:Either #() (#() * a * List a)) ->
11-
Right #() (#() * a * List a) ((), x, l))
8+
List__rec a (\ (_:List a) -> Either #() #(#(), a, List a))
9+
(Left #() #(#(), a, List a) ())
10+
(\ (x:a) (l:List a) (_:Either #() #(#(), a, List a)) ->
11+
Right #() #(#(), a, List a) ((), x, l))
1212
l;
1313

14-
foldListPermH : (a:sort 0) -> Either #() (#() * a * List a) -> List a;
14+
foldListPermH : (a:sort 0) -> Either #() #(#(), a, List a) -> List a;
1515
foldListPermH a =
16-
either #() (#() * a * List a) (List a)
16+
either #() #(#(), a, List a) (List a)
1717
(\ (_ : #()) -> Nil a)
18-
(\ (tup : (#() * a * List a)) ->
19-
Cons a tup.(2).(1) tup.(2).(2));
18+
(\ (tup : #(#(), a, List a)) ->
19+
Cons a tup.1 tup.2);

‎heapster-saw/examples/rust_lifetimes.saw‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ heapster_assume_fun env "llvm.uadd.with.overflow.i64"
2626
"(). arg0:int64<>, arg1:int64<> -o \
2727
\ ret:struct(int64<>,int1<>)"
2828
"\\ (x y:Vec 64 Bool) -> \
29-
\ returnM (Vec 64 Bool * Vec 1 Bool) \
29+
\ returnM #(Vec 64 Bool, Vec 1 Bool) \
3030
\ (bvAdd 64 x y, gen 1 Bool (\\ (_:Nat) -> bvCarry 64 x y))";
3131

3232
// llvm.expect.i1

‎heapster-saw/examples/rust_lifetimes.sawcore‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,17 +3,17 @@ module rust_lifetimes where
33

44
import Prelude;
55

6-
unfoldListPermH : (a:sort 0) -> List a -> Either #() (#() * a * List a);
6+
unfoldListPermH : (a:sort 0) -> List a -> Either #() #(#(), a, List a);
77
unfoldListPermH a l =
8-
List__rec a (\ (_:List a) -> Either #() (#() * a * List a))
9-
(Left #() (#() * a * List a) ())
10-
(\ (x:a) (l:List a) (_:Either #() (#() * a * List a)) ->
11-
Right #() (#() * a * List a) ((), x, l))
8+
List__rec a (\ (_:List a) -> Either #() #(#(), a, List a))
9+
(Left #() #(#(), a, List a) ())
10+
(\ (x:a) (l:List a) (_:Either #() #(#(), a, List a)) ->
11+
Right #() #(#(), a, List a) ((), x, l))
1212
l;
1313

14-
foldListPermH : (a:sort 0) -> Either #() (#() * a * List a) -> List a;
14+
foldListPermH : (a:sort 0) -> Either #() #(#(), a, List a) -> List a;
1515
foldListPermH a =
16-
either #() (#() * a * List a) (List a)
16+
either #() #(#(), a, List a) (List a)
1717
(\ (_ : #()) -> Nil a)
18-
(\ (tup : (#() * a * List a)) ->
19-
Cons a tup.(2).(1) tup.(2).(2));
18+
(\ (tup : #(#(), a, List a)) ->
19+
Cons a tup.1 tup.2);

0 commit comments

Comments
 (0)