-
Notifications
You must be signed in to change notification settings - Fork 62
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
whoops, forgot to add clearbufs saw files
- Loading branch information
Eddy Westbrook
committed
Jul 9, 2021
1 parent
5420dad
commit 8f09d0b
Showing
2 changed files
with
76 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
enable_experimental; | ||
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_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_export_coq env "clearbufs.v"; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,63 @@ | ||
|
||
module clearbufs where | ||
|
||
import Prelude; | ||
|
||
BV64 : sort 0; | ||
BV64 = Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #()); | ||
|
||
V64 : sort 0; | ||
V64 = Vec 64 Bool; | ||
|
||
-- Harcoded 64 length bitvector value 16, used for mbox definitions | ||
bv64_16 : Vec 64 Bool; | ||
bv64_16 = [False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,True,False,False,False,False]; | ||
|
||
data Mbox : sort 0 where { | ||
Mbox_nil : Mbox; | ||
Mbox_cons : Mbox -> (len : Vec 64 Bool) -> BVVec 64 len BV64 -> Mbox; | ||
} | ||
|
||
-- A definition for the Mbox datatype; currently needed as a workaround in Heapster | ||
Mbox_def : sort 0; | ||
Mbox_def = Mbox; | ||
|
||
{- Mbox__rec : (P : Mbox -> sort 0) -> | ||
(P Mbox_nil) -> | ||
((m:Mbox) -> P m -> (len:BV64) -> (d:BVVec 64 bv64_16 BV64) -> P (Mbox_cons m len d)) -> | ||
(m:Mbox) -> P m; | ||
Mbox__rec P f1 f2 m = Mbox#rec P f1 f2 m; -} | ||
|
||
--unfoldMbox : Mbox -> Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()); | ||
primitive | ||
unfoldMbox : Mbox -> Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len BV64 * #())); | ||
|
||
{-unfoldMbox m = | ||
Mbox__rec (\ (_:Mbox) -> Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #())) | ||
(Left #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()) ()) | ||
(\ (m:Mbox) (_:Either #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #())) (len:BV64) (d:BVVec 64 bv64_16 BV64) -> | ||
Right #() (Mbox * BV64 * BVVec 64 bv64_16 BV64 * #()) (m, len, d, ())) | ||
m; | ||
-} | ||
|
||
primitive | ||
foldMbox : Either #() (Sigma (V64) (\ (len : V64) -> Mbox * BVVec 64 len BV64 * #())) -> Mbox; | ||
|
||
--(Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #()) -> Mbox; | ||
{- | ||
foldMbox = | ||
either #() (Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #()) Mbox | ||
(\ (_:#()) -> Mbox_nil) | ||
(\ (tup : (Mbox * BV64 * (BVVec 64 bv64_16 BV64) * #())) -> | ||
Mbox_cons tup.1 tup.2 tup.3); | ||
-} | ||
|
||
primitive | ||
transMbox : Mbox -> Mbox -> Mbox; | ||
{- | ||
transMbox m1 m2 = | ||
Mbox__rec (\ (_ : Mbox) -> Mbox) | ||
m2 | ||
(\ (_ : Mbox) (rec:Mbox) (len : BV64) (vec : BVVec 64 bv64_16 BV64) -> Mbox_cons rec len vec) | ||
m1; | ||
-} |