Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change saw-core tuple representation. #1612

Draft
wants to merge 27 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
4a961b3
Change saw-core tuple representation.
Mar 16, 2022
8e5b70c
Reinstate pair-related functions to Verifier/SAW/OpenTerm.hs
Mar 16, 2022
1e00330
Adapt heapster-saw to changed tuple representation.
Mar 16, 2022
7a1f95f
Adapt saw-core-coq to changed tuple representation.
Mar 16, 2022
4854f0d
Adapt saw-script to changed tuple representation.
Mar 16, 2022
453cdb0
Adapt crux-mir-comp to changed tuple representation.
Mar 16, 2022
84e0573
Fix definition of `ensureTupleType` in SCTypeCheck.hs.
Mar 17, 2022
0b43f8f
Remove saw-core parenthesized tuple selector syntax "x.(1)".
Mar 18, 2022
aec37ef
Rewrite CompM combinators in Prelude.sawcore to use new tuple types.
Mar 18, 2022
454b0da
Update saw-core tuple syntax in heapster-saw/examples.
Mar 18, 2022
e29f98f
Restore special cases to tuple operations in Heapster/SAWTranslation.
Mar 18, 2022
75b639c
Change saw-core tuple representation.
Mar 16, 2022
016cdbc
Reinstate pair-related functions to Verifier/SAW/OpenTerm.hs
Mar 16, 2022
65966e7
Adapt heapster-saw to changed tuple representation.
Mar 16, 2022
3051800
Adapt saw-core-coq to changed tuple representation.
Mar 16, 2022
46a0c6d
Adapt saw-script to changed tuple representation.
Mar 16, 2022
b6f308a
Adapt crux-mir-comp to changed tuple representation.
Mar 16, 2022
7ce2fce
Fix definition of `ensureTupleType` in SCTypeCheck.hs.
Mar 17, 2022
4af3cbf
Remove saw-core parenthesized tuple selector syntax "x.(1)".
Mar 18, 2022
b1fad07
Rewrite CompM combinators in Prelude.sawcore to use new tuple types.
Mar 18, 2022
5c93c78
Update saw-core tuple syntax in heapster-saw/examples.
Mar 18, 2022
2edef5f
Restore special cases to tuple operations in Heapster/SAWTranslation.
Mar 18, 2022
aa624a8
Export typeListOpenTerm from OpenTerm library.
Mar 18, 2022
6d50ea7
Add Coq definitions for `Tuple` and `{head,tail,cons}Tuple` functions.
Mar 18, 2022
d601299
fixed a bug in translateBlockMapBodies, which was iteratively buildin…
Mar 18, 2022
e311d74
Merge branch 'saw-tuples' of github.com:GaloisInc/saw-script into saw…
Mar 18, 2022
c59371b
added saw-core-coq translations for all the tuple-related definitions
Mar 18, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update saw-core tuple syntax in heapster-saw/examples.
  • Loading branch information
Brian Huffman committed Mar 18, 2022

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit 454b0da616f97c8226841bc51bf6ae3027e122d1
53 changes: 31 additions & 22 deletions heapster-saw/examples/arrays.sawcore
Original file line number Diff line number Diff line change
@@ -3,39 +3,48 @@ module arrays where

import Prelude;

letRecM_single :
(lrt : LetRecType) ->
(B : sort 0) ->
(lrtToType lrt -> lrtToType lrt) ->
(lrtToType lrt -> CompM B) -> CompM B;
letRecM_single lrt B fn body =
letRecM
(LRT_Cons lrt LRT_Nil) B
(\ (x : lrtToType lrt) -> consTuple (lrtToType lrt) TypeNil (fn x) ())
(\ (x : lrtToType lrt) -> body x);

-- The helper function for noErrorsContains0
--
-- 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_Nil)
(BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool)
letRecM_single
(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)))))
#(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)) ->
((\ (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))
(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)))
(f len (bvAdd 64 i 0x0000000000000001) v))), ()))
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))
(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)))
(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
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions heapster-saw/examples/global_var.sawcore
Original file line number Diff line number Diff line change
@@ -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);
18 changes: 9 additions & 9 deletions heapster-saw/examples/iter_linked_list.sawcore
Original file line number Diff line number Diff line change
@@ -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 =
2 changes: 1 addition & 1 deletion heapster-saw/examples/mbox.saw
Original file line number Diff line number Diff line change
@@ -73,7 +73,7 @@ heapster_assume_fun env "__memcpy_chk"
"(len:bv 64). arg0:byte_array<W,len>, arg1:byte_array<W,len>, arg2:eq(llvmword (len)) -o \
\ arg0:byte_array<W,len>, arg1:byte_array<W,len>"
"\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> \
\ returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)";
\ returnM #(BVVec 64 len (Vec 8 Bool), BVVec 64 len (Vec 8 Bool)) (src, src)";


//------------------------------------------------------------------------------
18 changes: 9 additions & 9 deletions heapster-saw/examples/mbox.sawcore
Original file line number Diff line number Diff line change
@@ -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;
2 changes: 1 addition & 1 deletion heapster-saw/examples/memcpy.saw
Original file line number Diff line number Diff line change
@@ -10,7 +10,7 @@ heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
\ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(len,b)), \
\ arg2:eq(llvmword(len)) -o \
\ arg0:[l1]memblock(W,0,len,eqsh(len,b)), arg1:[l2]memblock(rw,0,len,eqsh(len,b))"
"\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
"\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM #(#(), #()) ((),())";


heapster_typecheck_fun env "copy_int"
6 changes: 3 additions & 3 deletions heapster-saw/examples/rust_data.saw
Original file line number Diff line number Diff line change
@@ -105,7 +105,7 @@ heapster_define_opaque_llvmshape env "Vec" 64
// Opaque type for HashMap<T,U>
heapster_define_opaque_llvmshape env "HashMap" 64
"T:llvmshape 64, U:llvmshape 64" "56"
"\\ (T:sort 0) (U:sort 0) -> List (T * U)";
"\\ (T:sort 0) (U:sort 0) -> List #(T, U)";

// BinTree<X> type
heapster_define_rust_type env
@@ -234,7 +234,7 @@ heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc"
heapster_assume_fun env "llvm.uadd.with.overflow.i64"
"(). arg0:int64<>, arg1:int64<> -o ret:struct(int64<>,int1<>)"
"\\ (x y:Vec 64 Bool) -> \
\ returnM (Vec 64 Bool * Vec 1 Bool) (bvAdd 64 x y, single Bool (bvCarry 64 x y))";
\ returnM #(Vec 64 Bool, Vec 1 Bool) (bvAdd 64 x y, single Bool (bvCarry 64 x y))";

// llvm.expect.i1
heapster_assume_fun env "llvm.expect.i1"
@@ -248,7 +248,7 @@ heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
\ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(len,b)), \
\ arg2:eq(llvmword(len)) -o \
\ arg0:[l1]memblock(W,0,len,eqsh(len,b)), arg1:[l2]memblock(rw,0,len,eqsh(len,b))"
"\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
"\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM #(#(), #()) ((),())";

// Box<List20<u64>>::clone
box_list20_u64_clone_sym <- heapster_find_symbol_with_type env
18 changes: 9 additions & 9 deletions heapster-saw/examples/rust_data.sawcore
Original file line number Diff line number Diff line change
@@ -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);
2 changes: 1 addition & 1 deletion heapster-saw/examples/rust_lifetimes.saw
Original file line number Diff line number Diff line change
@@ -26,7 +26,7 @@ heapster_assume_fun env "llvm.uadd.with.overflow.i64"
"(). arg0:int64<>, arg1:int64<> -o \
\ ret:struct(int64<>,int1<>)"
"\\ (x y:Vec 64 Bool) -> \
\ returnM (Vec 64 Bool * Vec 1 Bool) \
\ returnM #(Vec 64 Bool, Vec 1 Bool) \
\ (bvAdd 64 x y, gen 1 Bool (\\ (_:Nat) -> bvCarry 64 x y))";

// llvm.expect.i1
18 changes: 9 additions & 9 deletions heapster-saw/examples/rust_lifetimes.sawcore
Original file line number Diff line number Diff line change
@@ -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);
2 changes: 1 addition & 1 deletion heapster-saw/examples/sha512.saw
Original file line number Diff line number Diff line change
@@ -10,7 +10,7 @@ heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
heapster_assume_fun env "CRYPTO_load_u64_be"
"(). arg0:ptr((R,0) |-> int64<>) -o \
\ arg0:ptr((R,0) |-> int64<>), ret:int64<>"
"\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 64 Bool) (x, x)";
"\\ (x:Vec 64 Bool) -> returnM #(Vec 64 Bool, Vec 64 Bool) (x, x)";

heapster_typecheck_fun env "return_state"
"(). arg0:array(W,0,<8,*8,fieldsh(int64<>)) -o \
8 changes: 4 additions & 4 deletions heapster-saw/examples/string_set.sawcore
Original file line number Diff line number Diff line change
@@ -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)
@@ -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)