-
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.
Merge pull request #1778 from GaloisInc/heapster-itree
Use itree SpecM monad instead of CompM in Heapster
- Loading branch information
Showing
41 changed files
with
2,852 additions
and
1,011 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
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
Binary file not shown.
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
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
Binary file not shown.
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,7 @@ | ||
#include<unistd.h> | ||
|
||
#define HELLO "Hello, World!" | ||
|
||
void hello_world () { | ||
write (1, HELLO, sizeof(HELLO)); | ||
} |
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,30 @@ | ||
enable_experimental; | ||
env <- heapster_init_env_from_file "io.sawcore" "io.bc"; | ||
|
||
// Set the event type | ||
heapster_set_event_type env "ioEv"; | ||
|
||
// Integer types | ||
heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))"; | ||
heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))"; | ||
heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))"; | ||
|
||
heapster_define_perm env "int8array" "rw:rwmodality,len:bv 64" "llvmptr 64" | ||
"array(rw,0,<len,*1,fieldsh(8,int8<>))"; | ||
|
||
// Assume the read and write functions call their corresponding events | ||
heapster_assume_fun env "\01_write" | ||
"(len:bv 64). \ | ||
\ arg0:int32<>, arg1:int8array<R,len>, arg2:eq(llvmword(len)) -o ret:int64<>" | ||
"\\ (len:Vec 64 Bool) (fd:Vec 32 Bool) (buf:buffer len) -> \ | ||
\ triggerS ioEv emptyFunStack (writeEv fd len buf)"; | ||
|
||
|
||
/// | ||
/// And now to start type-checking! | ||
/// | ||
|
||
heapster_typecheck_fun env "hello_world" "(). empty -o empty"; | ||
|
||
// Finally, export everything to Coq | ||
heapster_export_coq env "io_gen.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,31 @@ | ||
|
||
module io where | ||
|
||
import Prelude; | ||
|
||
bitvector : Nat -> sort 0; | ||
bitvector n = Vec n Bool; | ||
|
||
-- The type of buffers of a given length | ||
buffer : bitvector 64 -> sort 0; | ||
buffer len = BVVec 64 len (bitvector 8); | ||
|
||
data ioEvArgs : sort 0 where { | ||
writeEv : bitvector 32 -> (len:bitvector 64) -> buffer len -> | ||
ioEvArgs; | ||
readEv : bitvector 32 -> bitvector 64 -> ioEvArgs; | ||
} | ||
|
||
ioEvRet : ioEvArgs -> sort 0; | ||
ioEvRet args = | ||
ioEvArgs#rec | ||
(\ (_:ioEvArgs) -> sort 0) | ||
(\ (_:bitvector 32) (len:bitvector 64) (_:buffer len) -> bitvector 64) | ||
(\ (_:bitvector 32) (len:bitvector 64) -> | ||
Sigma (bitvector 64) | ||
(\ (len_ret:bitvector 64) -> | ||
is_bvule 64 len_ret len * buffer len_ret)) | ||
args; | ||
|
||
ioEv : EvType; | ||
ioEv = Build_EvType ioEvArgs ioEvRet; |
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,19 @@ | ||
From Coq Require Import Lists.List. | ||
From Coq Require Import String. | ||
From Coq Require Import Vectors.Vector. | ||
From CryptolToCoq Require Import SAWCoreScaffolding. | ||
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. | ||
From CryptolToCoq Require Import SAWCoreBitvectors. | ||
|
||
From CryptolToCoq Require Import SAWCorePrelude. | ||
From CryptolToCoq Require Import SpecMExtra. | ||
From EnTree Require Import Automation. | ||
Import SAWCorePrelude. | ||
Import SpecMNotations. | ||
Local Open Scope entree_scope. | ||
|
||
Require Import Examples.io_gen. | ||
Import io. | ||
|
||
Print hello_world__bodies. | ||
Print __x1_write. |
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
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
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
Oops, something went wrong.