Skip to content

Commit

Permalink
Remove references to LSS in intTests
Browse files Browse the repository at this point in the history
Fixes #493.
  • Loading branch information
Aaron Tomb committed Oct 16, 2019
1 parent 8277a5e commit b57d881
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 12 deletions.
8 changes: 4 additions & 4 deletions intTests/test0012_jss_aig/README
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@ The tests in 'test.saw' only make sense for the SAW backend; the
default backend encodes the arguments and results in a different
way.

There used to be a bug in JSS and LSS where multiple AIG writes
interacted, causing the number of input bits in the AIG to grow with
each write. So in 'test.sh' we are careful to check that the number of
input bits is always 16.
There used to be a bug in JSS where multiple AIG writes interacted,
causing the number of input bits in the AIG to grow with each write. So
in 'test.sh' we are careful to check that the number of input bits is
always 16.

Besides checking predicates, where the input encoding does not matter,
and the output is a single bit, we also check the input and output
Expand Down
11 changes: 5 additions & 6 deletions intTests/test0015_sawscript_aig/README
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,8 @@ Test AIG generation in SAWScript.
These examples provide some documentation of the SAWScript AIG
encoding.

Note that, compared to LSS and JSS, the arguments here are reversed:
for functions '\x -> \y -> e' the arguments are packed as 'x # y'
here, but as 'y # x' for LSS and JSS. However, in LSS and JSS you
don't actually write the arguments explicitly -- rather, open terms
are closed over the symbolic variables in scope -- so I'm not sure the
comparison is fair.
Note that, compared to JSS, the arguments here are reversed: for
functions '\x -> \y -> e' the arguments are packed as 'x # y' here, but
as 'y # x' for JSS. However, in JSS you don't actually write the
arguments explicitly -- rather, open terms are closed over the symbolic
variables in scope -- so I'm not sure the comparison is fair.
3 changes: 1 addition & 2 deletions intTests/test0015_sawscript_aig/test.saw
Original file line number Diff line number Diff line change
Expand Up @@ -9,13 +9,12 @@ write_aig "tmp/yy.aig" {{ \(x:[8]) -> \(y:[8]) -> y + y }};
write_aig "tmp/2y.aig" {{ \(x:[8]) -> \(y:[8]) -> 2 * y }};

// The code below is very similar to '../test0012_jss_aig/test.saw'
// and '../test0014_lss_aig/test.saw'.

// Many of these Cryptol functions have types more specific than
// necessary. The point is to document the behavior of SAWScript
// AIG generation.
let {{
// Arguments are reversed, compared to LSS and JSS.
// Arguments are reversed, compared to JSS.

run_pred : ([16] -> [1]) -> [8] -> [8] -> [1]
run_pred f x y = f (((zero # x) <<< 8) + (zero # y))
Expand Down

0 comments on commit b57d881

Please sign in to comment.