Skip to content

Commit

Permalink
Fix saw-core tuple syntax in heapster-saw examples directory.
Browse files Browse the repository at this point in the history
  • Loading branch information
Brian Huffman committed Mar 17, 2022
1 parent 453cdb0 commit b4b33c8
Show file tree
Hide file tree
Showing 8 changed files with 64 additions and 64 deletions.
22 changes: 11 additions & 11 deletions heapster-saw/examples/arrays.sawcore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,34 +8,34 @@ import Prelude;
-- noErrorsContains0H len i v =
-- orM (exists x. returnM x) (noErrorsContains0H len (i+1) v)
noErrorsContains0H : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool);
noErrorsContains0H len_top i_top v_top =
letRecM
(LRT_Cons
(LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))))
LRT_Ret #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)))))
LRT_Nil)
(BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool)
#(BVVec 64 len_top (Vec 64 Bool), Vec 64 Bool)
(\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)) ->
((\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
precondHint
(CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
(CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool))
(and (bvsle 64 0x0000000000000000 i)
(bvsle 64 i 0x0fffffffffffffff))
(orM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
(existsM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
(BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
(returnM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))
(orM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
(existsM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
#(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)
(returnM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)))
(f len (bvAdd 64 i 0x0000000000000001) v))), ()))
(\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool)) ->
f len_top i_top v_top);

-- The specification that contains0 has no errors
noErrorsContains0 : (len:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
CompM #(BVVec 64 len (Vec 64 Bool), Vec 64 Bool);
noErrorsContains0 len v =
noErrorsContains0H len 0x0000000000000000 v;
22 changes: 11 additions & 11 deletions heapster-saw/examples/clearbufs.sawcore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,28 +25,28 @@ Mbox_def = Mbox;
(m:Mbox) -> P m;
Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -}

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

{-unfoldMbox m =
Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()))
(Left #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()) ())
(\ (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)) ->
Right #() (Mbox * Vec 64 Bool * BVVec 64 bv64_16 (Vec 64 Bool) * #()) (m, len, d, ()))
Mbox__rec (\ (_:Mbox) -> Either #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()))
(Left #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) ())
(\ (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)) ->
Right #() #(Mbox, Vec 64 Bool, BVVec 64 bv64_16 (Vec 64 Bool), #()) (m, len, d, ()))
m;
-}

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

--(Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) -> Mbox;
--#(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #()) -> Mbox;
{-
foldMbox =
either #() (Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #()) Mbox
either #() #(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #()) Mbox
(\ (_:#()) -> Mbox_nil)
(\ (tup : (Mbox * Vec 64 Bool * (BVVec 64 bv64_16 (Vec 64 Bool)) * #())) ->
Mbox_cons tup.1 tup.2 tup.3);
(\ (tup : #(Mbox, Vec 64 Bool, (BVVec 64 bv64_16 (Vec 64 Bool)), #())) ->
Mbox_cons tup.0 tup.1 tup.2);
-}

primitive
Expand Down
4 changes: 2 additions & 2 deletions heapster-saw/examples/global_var.sawcore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ module GlobalVar where

import Prelude;

acquireLockM : Vec 64 Bool -> CompM (Vec 64 Bool * Vec 64 Bool);
acquireLockM u = returnM (Vec 64 Bool * Vec 64 Bool)
acquireLockM : Vec 64 Bool -> CompM #(Vec 64 Bool, Vec 64 Bool);
acquireLockM u = returnM #(Vec 64 Bool, Vec 64 Bool)
(u,u);

releaseLockM : Vec 64 Bool -> Vec 64 Bool -> CompM (Vec 64 Bool);
Expand Down
18 changes: 9 additions & 9 deletions heapster-saw/examples/iter_linked_list.sawcore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,20 +27,20 @@ ListF__rec : (a b:sort 0) -> (P : ListF a b -> sort 0) ->
(l:ListF a b) -> P l;
ListF__rec a b P f1 f2 l = ListF#rec a b P f1 f2 l;

unfoldListF : (a b:sort 0) -> ListF a b -> Either b (a * ListF a b);
unfoldListF : (a b:sort 0) -> ListF a b -> Either b #(a, ListF a b);
unfoldListF a b l =
ListF__rec a b (\ (_:ListF a b) -> Either b (a * ListF a b))
(\ (x:b) -> Left b (a * ListF a b) x)
(\ (x:a) (l:ListF a b) (_:Either b (a * ListF a b)) ->
Right b (a * ListF a b) (x, l))
ListF__rec a b (\ (_:ListF a b) -> Either b #(a, ListF a b))
(\ (x:b) -> Left b #(a, ListF a b) x)
(\ (x:a) (l:ListF a b) (_:Either b #(a, ListF a b)) ->
Right b #(a, ListF a b) (x, l))
l;

foldListF : (a b:sort 0) -> Either b (a * ListF a b) -> ListF a b;
foldListF : (a b:sort 0) -> Either b #(a, ListF a b) -> ListF a b;
foldListF a b =
either b (a * ListF a b) (ListF a b)
either b #(a, ListF a b) (ListF a b)
(\ (x : b) -> NilF a b x)
(\ (tup : (a * ListF a b)) ->
ConsF a b tup.(1) tup.(2));
(\ (tup : #(a, ListF a b)) ->
ConsF a b tup.0 tup.1);

getListF : (a b:sort 0) -> ListF a b -> b;
getListF a b =
Expand Down
18 changes: 9 additions & 9 deletions heapster-saw/examples/mbox.sawcore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,20 +31,20 @@ Mbox__rec : (P : Mbox -> sort 0) ->
(m:Mbox) -> P m;
Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m;

unfoldMbox : Mbox -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool));
unfoldMbox : Mbox -> Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool));
unfoldMbox m =
Mbox__rec (\ (_:Mbox) -> Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)))
(Left #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) ())
(\ (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)) ->
Right #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
Mbox__rec (\ (_:Mbox) -> Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)))
(Left #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) ())
(\ (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)) ->
Right #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) (strt, len, m, d))
m;

foldMbox : Either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
foldMbox : Either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) -> Mbox;
foldMbox =
either #() (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
either #() #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool)) Mbox
(\ (_:#()) -> Mbox_nil)
(\ (tup : (Vec 64 Bool * Vec 64 Bool * Mbox * BVVec 64 bv64_128 (Vec 8 Bool))) ->
Mbox_cons tup.1 tup.2 tup.3 tup.(2).(2).(2));
(\ (tup : #(Vec 64 Bool, Vec 64 Bool, Mbox, BVVec 64 bv64_128 (Vec 8 Bool))) ->
Mbox_cons tup.0 tup.1 tup.2 tup.3);

{-
getMbox : (a : sort 0) -> Mbox a -> a;
Expand Down
18 changes: 9 additions & 9 deletions heapster-saw/examples/rust_data.sawcore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@ module rust_data where

import Prelude;

unfoldListPermH : (a:sort 0) -> List a -> Either #() (#() * a * List a);
unfoldListPermH : (a:sort 0) -> List a -> Either #() #(#(), a, List a);
unfoldListPermH a l =
List__rec a (\ (_:List a) -> Either #() (#() * a * List a))
(Left #() (#() * a * List a) ())
(\ (x:a) (l:List a) (_:Either #() (#() * a * List a)) ->
Right #() (#() * a * List a) ((), x, l))
List__rec a (\ (_:List a) -> Either #() #(#(), a, List a))
(Left #() #(#(), a, List a) ())
(\ (x:a) (l:List a) (_:Either #() #(#(), a, List a)) ->
Right #() #(#(), a, List a) ((), x, l))
l;

foldListPermH : (a:sort 0) -> Either #() (#() * a * List a) -> List a;
foldListPermH : (a:sort 0) -> Either #() #(#(), a, List a) -> List a;
foldListPermH a =
either #() (#() * a * List a) (List a)
either #() #(#(), a, List a) (List a)
(\ (_ : #()) -> Nil a)
(\ (tup : (#() * a * List a)) ->
Cons a tup.(2).(1) tup.(2).(2));
(\ (tup : #(#(), a, List a)) ->
Cons a tup.(1) tup.(2));
18 changes: 9 additions & 9 deletions heapster-saw/examples/rust_lifetimes.sawcore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,17 +3,17 @@ module rust_lifetimes where

import Prelude;

unfoldListPermH : (a:sort 0) -> List a -> Either #() (#() * a * List a);
unfoldListPermH : (a:sort 0) -> List a -> Either #() #(#(), a, List a);
unfoldListPermH a l =
List__rec a (\ (_:List a) -> Either #() (#() * a * List a))
(Left #() (#() * a * List a) ())
(\ (x:a) (l:List a) (_:Either #() (#() * a * List a)) ->
Right #() (#() * a * List a) ((), x, l))
List__rec a (\ (_:List a) -> Either #() #(#(), a, List a))
(Left #() #(#(), a, List a) ())
(\ (x:a) (l:List a) (_:Either #() #(#(), a, List a)) ->
Right #() #(#(), a, List a) ((), x, l))
l;

foldListPermH : (a:sort 0) -> Either #() (#() * a * List a) -> List a;
foldListPermH : (a:sort 0) -> Either #() #(#(), a, List a) -> List a;
foldListPermH a =
either #() (#() * a * List a) (List a)
either #() #(#(), a, List a) (List a)
(\ (_ : #()) -> Nil a)
(\ (tup : (#() * a * List a)) ->
Cons a tup.(2).(1) tup.(2).(2));
(\ (tup : #(#(), a, List a)) ->
Cons a tup.(1) tup.(2));
8 changes: 4 additions & 4 deletions heapster-saw/examples/string_set.sawcore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,10 @@ listInsertM a l s =
returnM (List a) (Cons a s l);

listRemoveM : (a : sort 0) -> (a -> a -> Bool) -> List a -> a ->
CompM (List a * a);
CompM #(List a, a);
listRemoveM a test_eq l s =
returnM
(List a * a)
#(List a, a)
(List__rec
a (\ (_:List a) -> List a)
(Nil a)
Expand All @@ -30,10 +30,10 @@ stringListInsertM : List String -> String -> CompM (List String);
stringListInsertM l s =
returnM (List String) (Cons String s l);

stringListRemoveM : List String -> String -> CompM (stringList * String);
stringListRemoveM : List String -> String -> CompM #(stringList, String);
stringListRemoveM l s =
returnM
(stringList * String)
#(stringList, String)
(List__rec
String (\ (_:List String) -> List String)
(Nil String)
Expand Down

0 comments on commit b4b33c8

Please sign in to comment.