-
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.
Add integration test for using
llvm_points_to
with Cryptol tuples.
Fixes #159.
- Loading branch information
Brian Huffman
committed
Jan 20, 2021
1 parent
6d6b6a2
commit 05ca990
Showing
5 changed files
with
49 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,2 @@ | ||
test.bc : test.c | ||
clang -c -emit-llvm -g -o test.bc test.c |
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,21 @@ | ||
#include <stdint.h> | ||
|
||
struct triple { | ||
uint8_t first[4]; | ||
uint16_t second; | ||
uint16_t third; | ||
}; | ||
|
||
void swap (struct triple *p) { | ||
uint8_t temp1; | ||
uint16_t temp2; | ||
temp1 = p->first[0]; | ||
p->first[0] = p->first[3]; | ||
p->first[3] = temp1; | ||
temp1 = p->first[1]; | ||
p->first[1] = p->first[2]; | ||
p->first[2] = temp1; | ||
temp2 = p->second; | ||
p->second = p->third; | ||
p->third = temp2; | ||
} |
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,25 @@ | ||
// This is a test demonstrating the use of `llvm_points_to` with a | ||
// struct pointer and a single Cryptol term of tuple type. | ||
// https://github.com/GaloisInc/saw-script/issues/159 | ||
|
||
bc <- llvm_load_module "test.bc"; | ||
|
||
let i8 = llvm_int 8; | ||
let i16 = llvm_int 16; | ||
|
||
let {{ | ||
swap_spec : ([4][8], [16], [16]) -> ([4][8], [16], [16]) | ||
swap_spec (xs, y, z) = (reverse xs, z, y) | ||
}}; | ||
|
||
swap_ov <- | ||
llvm_verify bc "swap" [] false | ||
do { | ||
let t = llvm_struct "struct.triple"; | ||
p <- llvm_alloc t; | ||
x <- llvm_fresh_var "x" t; | ||
llvm_points_to p (llvm_term x); | ||
llvm_execute_func [p]; | ||
llvm_points_to p (llvm_term {{ swap_spec x }}); | ||
} | ||
z3; |
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 @@ | ||
$SAW test.saw |