Skip to content

Commit d35ad9e

Browse files
m-yacm-yac
committed
Merge branch 'master' into heapster/widening-offsets
2 parents a0dfd11 + c37a0b2 commit d35ad9e

13 files changed

+609
-172
lines changed

‎heapster-saw/examples/arrays.saw

+39-15
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,54 @@
11
enable_experimental;
22
env <- heapster_init_env_from_file "arrays.sawcore" "arrays.bc";
33

4+
// Integer types
45
heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
56
heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
67

78
heapster_define_perm env "int64array" "len:bv 64" "llvmptr 64" "array(0,<len,*8,[(W,0) |-> int64<>])";
89

910

10-
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<>";
11+
heapster_typecheck_fun env "contains0_rec_"
12+
"(len:bv 64). arg0:eq(llvmword(len)), arg1:int64array<len>, arg2:int64<> -o \
13+
\ arg0:true, arg1:int64array<len>, arg2:true, ret:int64<>";
1114

1215
// the old way using a block entry hint
13-
// heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
14-
// 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)";
15-
// 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<>";
16-
17-
heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
18-
19-
heapster_typecheck_fun env "zero_array" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:true";
20-
21-
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";
16+
// heapster_block_entry_hint env "contains0" 9
17+
// "top0:bv 64, top1:llvmptr 64, top2:llvmptr 64"
18+
// "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64"
19+
// "top0:true, top1:array(0,<top0,*1,[(W,0) |-> int64<>]),
20+
// \ top2:eq(llvmword(top0)), arg0:ptr((W,0) |-> true), \
21+
// \ arg1:ptr((W,0) |-> eq(x1)), arg2:ptr((W,0) |-> eq(x0)), arg3:ptr((W,0) |-> int64<>), \
22+
// \ frm:llvmframe [arg3:8, arg2:8, arg1:8, arg0:8], x0:eq(top2), x1:eq(top1)";
23+
// heapster_typecheck_fun env "contains0"
24+
// "(len:bv 64). arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:eq(llvmword(len)) -o \
25+
// \ arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:true, ret:int64<>";
26+
27+
heapster_typecheck_fun env "contains0"
28+
"(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
29+
\ arg0:int64array<len>, arg1:true, ret:int64<>";
30+
31+
heapster_typecheck_fun env "zero_array"
32+
"(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
33+
\ arg0:int64array<len>, arg1:true, ret:true";
34+
35+
heapster_typecheck_fun env "zero_array_from"
36+
"(len:bv 64, off:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o \
37+
\ arg0:int64array<len>, arg1:true, arg2:true, ret:true";
2238

2339
heapster_join_point_hint env "filter_and_sum_pos" [];
24-
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<>";
25-
26-
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<>";
27-
28-
heapster_typecheck_fun env "sum_inc_ptr" "(len:bv 64).arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:true, ret:int64<>";
40+
heapster_typecheck_fun env "filter_and_sum_pos"
41+
"(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
42+
\ arg0:int64array<len>, arg1:true, ret:int64<>";
43+
44+
heapster_typecheck_fun env "sum_2d"
45+
"(l1:bv 64,l2:bv 64). arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> int64<>])]), \
46+
\ arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o \
47+
\ arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> int64<>])]), \
48+
\ arg1:true, arg2:true, ret:int64<>";
49+
50+
heapster_typecheck_fun env "sum_inc_ptr"
51+
"(len:bv 64). arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(len)) -o \
52+
\ arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:true, ret:int64<>";
2953

3054
heapster_export_coq env "arrays_gen.v";

‎heapster-saw/examples/clearbufs.saw

+14-3
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,21 @@ env <- heapster_init_env_from_file "clearbufs.sawcore" "clearbufs.bc";
44
// Integer types
55
heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
66

7-
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";
7+
heapster_define_reachability_perm env "Bufs"
8+
"x:llvmptr 64" "llvmptr 64"
9+
"exists len:(bv 64).ptr((W,0) |-> Bufs<x>) * \
10+
\ ptr((W,8) |-> eq(llvmword(len))) * \
11+
\ array(16, <len, *8, [(W,0) |-> int64<>])"
12+
"Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
813

9-
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]";
14+
heapster_block_entry_hint env "clearbufs" 3
15+
"top1:llvmptr 64"
16+
"frm:llvmframe 64,ghost:llvmptr 64"
17+
"top1:Bufs<ghost>, \
18+
\ arg0:ptr((W,0) |-> eq(ghost)), \
19+
\ ghost:Bufs<llvmword(0)>,frm:llvmframe [arg0:8]";
1020

11-
heapster_typecheck_fun env "clearbufs" "().arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
21+
heapster_typecheck_fun env "clearbufs"
22+
"(). arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
1223

1324
heapster_export_coq env "clearbufs_gen.v";

‎heapster-saw/examples/iso_recursive.saw

+14-3
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,21 @@
11
enable_experimental;
22
env <- heapster_init_env_from_file "iso_recursive.sawcore" "iso_recursive.bc";
33

4-
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>)"];
4+
// Integer types
5+
heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
56

6-
heapster_define_irt_recursive_shape env "ListS" 64 "X:llvmshape 64" "(fieldsh(eq(llvmword(0)))) orsh (fieldsh(eq(llvmword(1)));X;ListS<X>)";
7+
heapster_define_irt_recursive_perm env "List"
8+
"X:perm(llvmptr 64), l:lifetime, rw:rwmodality"
9+
"llvmptr 64"
10+
[ "eq(llvmword(0))",
11+
"[l]ptr((rw,0) |-> X) * ptr((rw,8) |-> List<X,l,rw>)" ];
712

8-
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))";
13+
heapster_define_irt_recursive_shape env "ListS" 64
14+
"X:llvmshape 64"
15+
"fieldsh(eq(llvmword(0))) orsh (fieldsh(eq(llvmword(1))); X; ListS<X>)";
16+
17+
heapster_typecheck_fun env "is_elem"
18+
"(x:bv 64). arg0:eq(llvmword(x)), arg1:List<int64<>,always,R> -o \
19+
\ arg0:true, arg1:true, ret:int64<>";
920

1021
heapster_export_coq env "iso_recursive_gen.v";

‎heapster-saw/examples/iter_linked_list.saw

+40-13
Original file line numberDiff line numberDiff line change
@@ -4,18 +4,45 @@ env <- heapster_init_env_from_file "iter_linked_list.sawcore" "iter_linked_list.
44
// Integer types
55
heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
66

7-
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";
8-
9-
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]";
10-
11-
heapster_typecheck_fun env "is_elem" "().arg0:int64<>, arg1:ListF<int64<>,always,R,llvmword(0)> -o arg0:true, arg1:true, ret:int64<>";
12-
13-
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]";
14-
15-
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";
16-
17-
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]";
18-
19-
heapster_typecheck_fun env "length" "().arg0:ListF<int64<>,always,W,llvmword(0)> -o arg0:true, ret:int64<>";
7+
heapster_define_reachability_perm env "ListF"
8+
"X:perm(llvmptr 64), l:lifetime, rw:rwmodality, y:llvmptr 64"
9+
"llvmptr 64"
10+
"[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> ListF<X,l,rw,y>)"
11+
"List_def" "foldList" "unfoldList" "appendList";
12+
13+
heapster_block_entry_hint env "is_elem" 3
14+
"top_ptr:llvmptr 64, top_ptr1:llvmptr 64"
15+
"ghost_frm:llvmframe 64, ghost_ptr:llvmptr 64"
16+
"top_ptr:int64<>, top_ptr1:true, \
17+
\ arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(top_ptr)), \
18+
\ arg2:ptr((W,0) |-> eq(ghost_ptr)), \
19+
\ ghost_ptr:ListF<int64<>,always,R,llvmword(0)>, \
20+
\ ghost_frm:llvmframe [arg2:8, arg1:8, arg0:8]";
21+
22+
heapster_typecheck_fun env "is_elem"
23+
"(). arg0:int64<>, arg1:ListF<int64<>,always,R,llvmword(0)> -o \
24+
\ arg0:true, arg1:true, ret:int64<>";
25+
26+
heapster_block_entry_hint env "incr_list" 3
27+
"top1:llvmptr 64"
28+
"frm:llvmframe 64,ghost:llvmptr 64"
29+
"top1:ListF<int64<>,always,W,ghost>, \
30+
\ arg0:ptr((W,0) |-> eq(ghost)), \
31+
\ ghost:ListF<int64<>,always,W,llvmword(0)>, frm:llvmframe [arg0:8]";
32+
33+
heapster_typecheck_fun env "incr_list"
34+
"(). arg0:ListF<int64<>,always,W,llvmword(0)> -o \
35+
\ arg0:ListF<int64<>,always,W,llvmword(0)>, ret:true";
36+
37+
heapster_block_entry_hint env "length" 3
38+
"top1:llvmptr 64"
39+
"frm:llvmframe 64, ghost:llvmptr 64"
40+
"top1:ListF<int64<>,always,W,ghost>, \
41+
\ arg0:ptr((W,0) |-> eq(ghost)), arg1:ptr((W,0) |-> int64<>), \
42+
\ ghost:ListF<int64<>,always,W,llvmword(0)>, frm:llvmframe [arg1:8,arg0:8]";
43+
44+
heapster_typecheck_fun env "length"
45+
"(). arg0:ListF<int64<>,always,W,llvmword(0)> -o \
46+
\ arg0:true, ret:int64<>";
2047

2148
heapster_export_coq env "iter_linked_list_gen.v";

‎heapster-saw/examples/linked_list.saw

+36-14
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,41 @@
1-
// This script expects to be run from the saw-script root directory
21
enable_experimental;
32
env <- heapster_init_env_from_file "linked_list.sawcore" "linked_list.bc";
43

5-
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";
6-
7-
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))";
8-
9-
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";
10-
11-
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))";
12-
13-
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>";
14-
15-
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>";
16-
17-
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>";
4+
// Integer types
5+
heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
6+
7+
heapster_define_recursive_perm env "List"
8+
"X:perm(llvmptr 64), l:lifetime, rw:rwmodality"
9+
"llvmptr 64"
10+
[ "eq(llvmword(0))",
11+
"[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> List<X,l,rw>)" ]
12+
"List_def" "foldList" "unfoldList";
13+
14+
heapster_typecheck_fun env "is_elem"
15+
"(). arg0:int64<>, arg1:List<int64<>,always,R> -o \
16+
\ arg0:true, arg1:true, ret:int64<>";
17+
18+
heapster_assume_fun env "malloc"
19+
"(sz:bv 64). arg0:eq(llvmword(8*sz)) -o \
20+
\ arg0:true, ret:array(0,<sz,*8,[(W,0) |-> true])"
21+
"mallocSpec";
22+
23+
heapster_typecheck_fun env "any"
24+
"(). arg0:llvmfunptr{1,64}((). arg0:int64<> -o arg0:true, ret:int64<>), \
25+
\ arg1:List<int64<>,always,R> -o \
26+
\ arg0:true, arg1:true, ret:int64<>";
27+
28+
heapster_typecheck_fun env "find_elem"
29+
"(). arg0:int64<>, arg1:List<int64<>,always,W> -o \
30+
\ arg0:true, arg1:true, ret:List<int64<>,always,W>";
31+
32+
heapster_typecheck_fun env "sorted_insert"
33+
"(). arg0:int64<>, arg1:List<int64<>,always,W> -o \
34+
\ arg0:true, arg1:true, ret:List<int64<>,always,W>";
35+
36+
heapster_typecheck_fun env "sorted_insert_no_malloc"
37+
"(). arg0:ptr((W,0) |-> int64<>) * ptr((W,8) |-> eq(llvmword(0))), \
38+
\ arg1:List<int64<>,always,W> -o \
39+
\ arg0:true, arg1:true, ret:List<int64<>,always,W>";
1840

1941
heapster_export_coq env "linked_list_gen.v";

‎heapster-saw/examples/loops.saw

+14-4
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,24 @@
11
enable_experimental;
22
env <- heapster_init_env_from_file "loops.sawcore" "loops.bc";
33

4+
// Integer types
45
heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
56

6-
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)";
7+
heapster_block_entry_hint env "add_loop" 3
8+
"top0:llvmptr 64, top1:llvmptr 64"
9+
"frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64"
10+
"top0:int64<>, top1:int64<>, \
11+
\ arg0:ptr((W,0) |-> int64<>), arg1:ptr((W,0) |-> int64<>), \
12+
\ frm:llvmframe [arg1:8,arg0:8,x1:8,x0:8], \
13+
\ x0:ptr((W,0) |-> true), x1:ptr((W,0) |-> true)";
714

8-
heapster_typecheck_fun env "add_loop" "().arg0:int64<>, arg1:int64<> -o ret:int64<>";
15+
heapster_typecheck_fun env "add_loop"
16+
"(). arg0:int64<>, arg1:int64<> -o ret:int64<>";
917

10-
heapster_typecheck_fun env "sign_of_sum" "().arg0:int64<>, arg1:int64<> -o ret:int64<>";
18+
heapster_typecheck_fun env "sign_of_sum"
19+
"(). arg0:int64<>, arg1:int64<> -o ret:int64<>";
1120

12-
heapster_typecheck_fun env "compare_sum" "().arg0:int64<>, arg1:int64<>, arg2:int64<> -o ret:int64<>";
21+
heapster_typecheck_fun env "compare_sum"
22+
"(). arg0:int64<>, arg1:int64<>, arg2:int64<> -o ret:int64<>";
1323

1424
heapster_export_coq env "loops_gen.v";

0 commit comments

Comments
 (0)