Merge pull request #1480 from GaloisInc/heapster/multiline-strings

[Heapster] Reformat heapster SAW scripts using multi-line strings

heapster-saw/examples/arrays.saw

@@ -1,28 +1,50 @@
 enable_experimental;
 env <- heapster_init_env_from_file "arrays.sawcore" "arrays.bc";
 
+// Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
 
 heapster_define_perm env "int64array" "len:bv 64" "llvmptr 64" "array(0,<len,*8,[(W,0) |-> int64<>])";
 
 
-heapster_typecheck_fun env "contains0_rec_" "(len:bv 64).arg0:eq(llvmword(len)), arg1:int64array<len>, arg2:int64<> -o arg0:true, arg1:int64array<len>, arg2:true, ret:int64<>";
+heapster_typecheck_fun env "contains0_rec_"
+  "(len:bv 64). arg0:eq(llvmword(len)), arg1:int64array<len>, arg2:int64<> -o \
+              \ arg0:true, arg1:int64array<len>, arg2:true, ret:int64<>";
 
 // the old way using a block entry hint
-// heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
-// heapster_block_entry_hint env "contains0" 9 "top0:bv 64, top1:llvmptr 64, top2:llvmptr 64" "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64" "top0:true, top1:array(0,<top0,*1,[(W,0) |-> int64<>]), top2:eq(llvmword(top0)), arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(x1)), arg2:ptr((W,0) |-> eq(x0)), arg3:ptr((W,0) |-> int64<>), frm:llvmframe [arg3:8, arg2:8, arg1:8, arg0:8], x0:eq(top2), x1:eq(top1)";
-// heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:true, ret:int64<>";
-
-heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
-
-heapster_typecheck_fun env "zero_array" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:true";
-
-heapster_typecheck_fun env "zero_array_from" "(len:bv 64, off:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o arg0:int64array<len>, arg1:true, ret:true";
+// heapster_block_entry_hint env "contains0" 9
+//   "top0:bv 64, top1:llvmptr 64, top2:llvmptr 64"
+//   "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64"
+//   "top0:true, top1:array(0,<top0,*1,[(W,0) |-> int64<>]),
+//   \ top2:eq(llvmword(top0)), arg0:ptr((W,0) |-> true), \
+//   \ arg1:ptr((W,0) |-> eq(x1)), arg2:ptr((W,0) |-> eq(x0)), arg3:ptr((W,0) |-> int64<>), \
+//   \ frm:llvmframe [arg3:8, arg2:8, arg1:8, arg0:8], x0:eq(top2), x1:eq(top1)";
+// heapster_typecheck_fun env "contains0"
+//   "(len:bv 64). arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:eq(llvmword(len)) -o \
+//               \ arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:true, ret:int64<>";
+
+heapster_typecheck_fun env "contains0"
+  "(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
+              \ arg0:int64array<len>, arg1:true, ret:int64<>";
+
+heapster_typecheck_fun env "zero_array"
+  "(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
+              \ arg0:int64array<len>, arg1:true, ret:true";
+
+heapster_typecheck_fun env "zero_array_from"
+  "(len:bv 64, off:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o \
+                         \ arg0:int64array<len>, arg1:true, arg2:true, ret:true";
 
 heapster_join_point_hint env "filter_and_sum_pos" [];
-heapster_typecheck_fun env "filter_and_sum_pos" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
-
-heapster_typecheck_fun env "sum_2d" "(l1:bv 64,l2:bv 64).arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:true, arg2:true, ret:int64<>";
+heapster_typecheck_fun env "filter_and_sum_pos"
+  "(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
+              \ arg0:int64array<len>, arg1:true, ret:int64<>";
+
+heapster_typecheck_fun env "sum_2d"
+  "(l1:bv 64,l2:bv 64). arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> int64<>])]), \
+                      \ arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o \
+                      \ arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> int64<>])]), \
+                      \ arg1:true, arg2:true, ret:int64<>";
 
 heapster_export_coq env "arrays_gen.v";

heapster-saw/examples/clearbufs.saw

@@ -4,10 +4,21 @@ env <- heapster_init_env_from_file "clearbufs.sawcore" "clearbufs.bc";
 // Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_define_reachability_perm env "Bufs" "x:llvmptr 64" "llvmptr 64" "exists len:(bv 64).ptr((W,0) |-> Bufs<x>) * ptr((W,8) |-> eq(llvmword(len))) * array(16, <len, *8, [(W,0) |-> int64<>])" "Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
+heapster_define_reachability_perm env "Bufs"
+  "x:llvmptr 64" "llvmptr 64"
+  "exists len:(bv 64).ptr((W,0) |-> Bufs<x>) * \
+  \ ptr((W,8) |-> eq(llvmword(len))) * \
+  \ array(16, <len, *8, [(W,0) |-> int64<>])"
+  "Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
 
-heapster_block_entry_hint env "clearbufs" 3 "top1:llvmptr 64" "frm:llvmframe 64,ghost:llvmptr 64" "top1:Bufs<ghost>, arg0:ptr((W,0) |-> eq(ghost)), ghost:Bufs<llvmword(0)>,frm:llvmframe [arg0:8]";
+heapster_block_entry_hint env "clearbufs" 3
+  "top1:llvmptr 64"
+  "frm:llvmframe 64,ghost:llvmptr 64"
+  "top1:Bufs<ghost>, \
+  \ arg0:ptr((W,0) |-> eq(ghost)), \
+  \ ghost:Bufs<llvmword(0)>,frm:llvmframe [arg0:8]";
 
-heapster_typecheck_fun env "clearbufs" "().arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
+heapster_typecheck_fun env "clearbufs"
+  "(). arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
 
 heapster_export_coq env "clearbufs_gen.v";

heapster-saw/examples/iso_recursive.saw

@@ -1,10 +1,21 @@
 enable_experimental;
 env <- heapster_init_env_from_file "iso_recursive.sawcore" "iso_recursive.bc";
 
-heapster_define_irt_recursive_perm env "List" "X:perm(llvmptr 64), l:lifetime, rw:rwmodality" "llvmptr 64" ["eq(llvmword(0))","[l]ptr((rw,0) |-> X) * ptr((rw,8) |-> List<X,l,rw>)"];
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_define_irt_recursive_shape env "ListS" 64 "X:llvmshape 64" "(fieldsh(eq(llvmword(0)))) orsh (fieldsh(eq(llvmword(1)));X;ListS<X>)";
+heapster_define_irt_recursive_perm env "List"
+  "X:perm(llvmptr 64), l:lifetime, rw:rwmodality"
+  "llvmptr 64"
+  [ "eq(llvmword(0))",
+    "[l]ptr((rw,0) |-> X) * ptr((rw,8) |-> List<X,l,rw>)" ];
 
-heapster_typecheck_fun env "is_elem" "(x:bv 64).arg0:eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,R> -o arg0:true, arg1:true, ret:exists z:(bv 64).eq(llvmword(z))";
+heapster_define_irt_recursive_shape env "ListS" 64
+  "X:llvmshape 64"
+  "fieldsh(eq(llvmword(0))) orsh (fieldsh(eq(llvmword(1))); X; ListS<X>)";
+
+heapster_typecheck_fun env "is_elem"
+  "(x:bv 64). arg0:eq(llvmword(x)), arg1:List<int64<>,always,R> -o \
+            \ arg0:true, arg1:true, ret:int64<>";
 
 heapster_export_coq env "iso_recursive_gen.v";

heapster-saw/examples/iter_linked_list.saw

@@ -4,18 +4,45 @@ env <- heapster_init_env_from_file "iter_linked_list.sawcore" "iter_linked_list.
 // Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_define_reachability_perm env "ListF" "X:perm(llvmptr 64), l:lifetime, rw:rwmodality, y:llvmptr 64" "llvmptr 64" "[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> ListF<X,l,rw,y>)" "List_def" "foldList" "unfoldList" "appendList";
-
-heapster_block_entry_hint env "is_elem" 3 "top_ptr:llvmptr 64, top_ptr1:llvmptr 64" "ghost_frm:llvmframe 64, ghost_ptr:llvmptr 64" "top_ptr:int64<>, top_ptr1:true, arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(top_ptr)), arg2:ptr((W,0) |-> eq(ghost_ptr)), ghost_ptr:ListF<int64<>,always,R,llvmword(0)>, ghost_frm:llvmframe [arg2:8, arg1:8, arg0:8]";
-
-heapster_typecheck_fun env "is_elem" "().arg0:int64<>, arg1:ListF<int64<>,always,R,llvmword(0)> -o arg0:true, arg1:true, ret:int64<>";
-
-heapster_block_entry_hint env "incr_list" 3 "top1:llvmptr 64" "frm:llvmframe 64,ghost:llvmptr 64" "top1:ListF<(exists y:(bv 64).eq(llvmword(y))),always,W,ghost>, arg0:ptr((W,0) |-> eq(ghost)),ghost:ListF<(exists y:(bv 64).eq(llvmword(y))),always,W,llvmword(0)>,frm:llvmframe [arg0:8]";
-
-heapster_typecheck_fun env "incr_list" "().arg0:ListF<(exists y:(bv 64).eq(llvmword(y))),always,W,llvmword(0)> -o arg0:ListF<(exists y:(bv 64).eq(llvmword(y))),always,W,llvmword(0)>, ret:true";
-
-heapster_block_entry_hint env "length" 3 "top1:llvmptr 64" "frm:llvmframe 64,ghost:llvmptr 64" "top1:ListF<(int64<>),always,W,ghost>, arg0:ptr((W,0) |-> eq(ghost)),ghost:ListF<(int64<>),always,W,llvmword(0)>,arg1:ptr((W,0) |-> int64<>),frm:llvmframe [arg1:8,arg0:8]";
-
-heapster_typecheck_fun env "length" "().arg0:ListF<int64<>,always,W,llvmword(0)> -o arg0:true, ret:int64<>";
+heapster_define_reachability_perm env "ListF"
+  "X:perm(llvmptr 64), l:lifetime, rw:rwmodality, y:llvmptr 64"
+  "llvmptr 64"
+  "[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> ListF<X,l,rw,y>)"
+  "List_def" "foldList" "unfoldList" "appendList";
+
+heapster_block_entry_hint env "is_elem" 3
+  "top_ptr:llvmptr 64, top_ptr1:llvmptr 64"
+  "ghost_frm:llvmframe 64, ghost_ptr:llvmptr 64"
+  "top_ptr:int64<>, top_ptr1:true, \
+  \ arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(top_ptr)), \
+  \ arg2:ptr((W,0) |-> eq(ghost_ptr)), \
+  \ ghost_ptr:ListF<int64<>,always,R,llvmword(0)>, \
+  \ ghost_frm:llvmframe [arg2:8, arg1:8, arg0:8]";
+
+heapster_typecheck_fun env "is_elem"
+  "(). arg0:int64<>, arg1:ListF<int64<>,always,R,llvmword(0)> -o \
+     \ arg0:true, arg1:true, ret:int64<>";
+
+heapster_block_entry_hint env "incr_list" 3
+  "top1:llvmptr 64"
+  "frm:llvmframe 64,ghost:llvmptr 64"
+  "top1:ListF<int64<>,always,W,ghost>, \
+  \ arg0:ptr((W,0) |-> eq(ghost)), \
+  \ ghost:ListF<int64<>,always,W,llvmword(0)>, frm:llvmframe [arg0:8]";
+
+heapster_typecheck_fun env "incr_list"
+  "(). arg0:ListF<int64<>,always,W,llvmword(0)> -o \
+     \ arg0:ListF<int64<>,always,W,llvmword(0)>, ret:true";
+
+heapster_block_entry_hint env "length" 3
+  "top1:llvmptr 64"
+  "frm:llvmframe 64, ghost:llvmptr 64"
+  "top1:ListF<int64<>,always,W,ghost>, \
+  \ arg0:ptr((W,0) |-> eq(ghost)), arg1:ptr((W,0) |-> int64<>), \
+  \ ghost:ListF<int64<>,always,W,llvmword(0)>, frm:llvmframe [arg1:8,arg0:8]";
+
+heapster_typecheck_fun env "length"
+  "(). arg0:ListF<int64<>,always,W,llvmword(0)> -o \
+     \ arg0:true, ret:int64<>";
 
 heapster_export_coq env "iter_linked_list_gen.v";

heapster-saw/examples/linked_list.saw

@@ -1,19 +1,41 @@
-// This script expects to be run from the saw-script root directory
 enable_experimental;
 env <- heapster_init_env_from_file "linked_list.sawcore" "linked_list.bc";
 
-heapster_define_recursive_perm env "List" "X:perm(llvmptr 64), l:lifetime, rw:rwmodality" "llvmptr 64" ["eq(llvmword(0))","[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> List<X,l,rw>)"] "List_def" "foldList" "unfoldList";
-
-heapster_typecheck_fun env "is_elem" "(x:bv 64).arg0:eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,R> -o arg0:true, arg1:true, ret:exists z:(bv 64).eq(llvmword(z))";
-
-heapster_assume_fun env "malloc" "(sz:bv 64).arg0:eq(llvmword(8*sz)) -o arg0:true, ret:array(0,<sz,*8,[(W,0) |-> true])" "mallocSpec";
-
-heapster_typecheck_fun env "any" "().arg0:llvmfunptr{1,64}(().arg0:(exists x:(bv 64).eq(llvmword(x))) -o arg0:true, ret:(exists x:(bv 64).eq(llvmword(x)))), arg1:List<(exists x:(bv 64).eq(llvmword(x))),always,R> -o arg0:true, arg1:true, ret:exists x:(bv 64).eq(llvmword(x))";
-
-heapster_typecheck_fun env "find_elem" "().arg0:exists x:(bv 64).eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,W> -o arg0:true, arg1:true, ret:List<(exists x:(bv 64).eq(llvmword(x))),always,W>";
-
-heapster_typecheck_fun env "sorted_insert" "(x:bv 64).arg0:eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,W> -o arg0:true, arg1:true, ret:List<(exists y:(bv 64).eq(llvmword(y))),always,W>";
-
-heapster_typecheck_fun env "sorted_insert_no_malloc" "(x:bv 64).arg0:ptr((W,0) |-> eq(llvmword(x))) * ptr((W,8) |-> eq(llvmword(0))), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,W> -o arg0:true, arg1:true, ret:List<(exists y:(bv 64).eq(llvmword(y))),always,W>";
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+heapster_define_recursive_perm env "List"
+  "X:perm(llvmptr 64), l:lifetime, rw:rwmodality"
+  "llvmptr 64"
+  [ "eq(llvmword(0))",
+    "[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> List<X,l,rw>)" ]
+  "List_def" "foldList" "unfoldList";
+
+heapster_typecheck_fun env "is_elem"
+  "(). arg0:int64<>, arg1:List<int64<>,always,R> -o \
+     \ arg0:true, arg1:true, ret:int64<>";
+
+heapster_assume_fun env "malloc"
+  "(sz:bv 64). arg0:eq(llvmword(8*sz)) -o \
+             \ arg0:true, ret:array(0,<sz,*8,[(W,0) |-> true])"
+  "mallocSpec";
+
+heapster_typecheck_fun env "any"
+  "(). arg0:llvmfunptr{1,64}((). arg0:int64<> -o arg0:true, ret:int64<>), \
+     \ arg1:List<int64<>,always,R> -o \
+     \ arg0:true, arg1:true, ret:int64<>";
+
+heapster_typecheck_fun env "find_elem"
+  "(). arg0:int64<>, arg1:List<int64<>,always,W> -o \
+     \ arg0:true, arg1:true, ret:List<int64<>,always,W>";
+
+heapster_typecheck_fun env "sorted_insert"
+  "(). arg0:int64<>, arg1:List<int64<>,always,W> -o \
+     \ arg0:true, arg1:true, ret:List<int64<>,always,W>";
+
+heapster_typecheck_fun env "sorted_insert_no_malloc"
+  "(). arg0:ptr((W,0) |-> int64<>) * ptr((W,8) |-> eq(llvmword(0))), \
+     \ arg1:List<int64<>,always,W> -o \
+     \ arg0:true, arg1:true, ret:List<int64<>,always,W>";
 
 heapster_export_coq env "linked_list_gen.v";

heapster-saw/examples/loops.saw

@@ -1,14 +1,24 @@
 enable_experimental;
 env <- heapster_init_env_from_file "loops.sawcore" "loops.bc";
 
+// Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_block_entry_hint env "add_loop" 3 "top0:llvmptr 64,top1:llvmptr 64" "frm:llvmframe 64,x0:llvmptr 64,x1:llvmptr 64" "top0:int64<>,top1:int64<>,arg0:ptr((W,0) |-> int64<>),arg1:ptr((W,0) |-> int64<>),frm:llvmframe [arg1:8,arg0:8,x1:8,x0:8],x0:ptr((W,0) |-> true),x1:ptr((W,0) |-> true)";
+heapster_block_entry_hint env "add_loop" 3
+  "top0:llvmptr 64, top1:llvmptr 64"
+  "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64"
+  "top0:int64<>, top1:int64<>, \
+  \ arg0:ptr((W,0) |-> int64<>), arg1:ptr((W,0) |-> int64<>), \
+  \ frm:llvmframe [arg1:8,arg0:8,x1:8,x0:8], \
+  \ x0:ptr((W,0) |-> true), x1:ptr((W,0) |-> true)";
 
-heapster_typecheck_fun env "add_loop" "().arg0:int64<>, arg1:int64<> -o ret:int64<>";
+heapster_typecheck_fun env "add_loop"
+  "(). arg0:int64<>, arg1:int64<> -o ret:int64<>";
 
-heapster_typecheck_fun env "sign_of_sum" "().arg0:int64<>, arg1:int64<> -o ret:int64<>";
+heapster_typecheck_fun env "sign_of_sum"
+  "(). arg0:int64<>, arg1:int64<> -o ret:int64<>";
 
-heapster_typecheck_fun env "compare_sum" "().arg0:int64<>, arg1:int64<>, arg2:int64<> -o ret:int64<>";
+heapster_typecheck_fun env "compare_sum"
+  "(). arg0:int64<>, arg1:int64<>, arg2:int64<> -o ret:int64<>";
 
 heapster_export_coq env "loops_gen.v";