diff options
Diffstat (limited to 'test/mono')
| -rw-r--r-- | test/mono/.gitignore | 1 | ||||
| -rw-r--r-- | test/mono/addsubexist.sail | 75 | ||||
| -rw-r--r-- | test/mono/fnreduce.sail | 69 | ||||
| -rw-r--r-- | test/mono/test.ml | 1 | ||||
| -rwxr-xr-x | test/mono/test.sh | 44 | ||||
| -rw-r--r-- | test/mono/tests | 4 | ||||
| -rw-r--r-- | test/mono/union-exist.sail | 33 | ||||
| -rw-r--r-- | test/mono/varmatch.sail | 19 | ||||
| -rw-r--r-- | test/mono/vector.sail | 21 |
9 files changed, 267 insertions, 0 deletions
diff --git a/test/mono/.gitignore b/test/mono/.gitignore new file mode 100644 index 00000000..2dd3daa3 --- /dev/null +++ b/test/mono/.gitignore @@ -0,0 +1 @@ +test-out
\ No newline at end of file diff --git a/test/mono/addsubexist.sail b/test/mono/addsubexist.sail new file mode 100644 index 00000000..f59f596e --- /dev/null +++ b/test/mono/addsubexist.sail @@ -0,0 +1,75 @@ +(* Adapted from hand-written ARM model *) + +default Order dec +typedef boolean = bit +typedef reg_size = bit[5] +typedef reg_index = [|31|] + +val reg_size -> reg_index effect pure UInt_reg +val unit -> unit effect pure (* probably not pure *) ReservedValue +function forall Nat 'N. bit['N] NOT((bit['N]) x) = ~(x) +val forall Nat 'M, Nat 'N. bit['M] -> bit['N] effect pure ZeroExtend +val forall Nat 'N. (bit['N], bit['N], bit) -> (bit['N],bit[4]) effect pure AddWithCarry +val forall Nat 'N, 'N IN {8,16,32,64}. (*broken? implicit<'N>*)unit -> bit['N] effect {rreg} rSP +val forall Nat 'N, 'N IN {8,16,32,64}. ((*ditto implicit<'N>,*)reg_index) -> bit['N] effect {rreg}rX +val (unit, bit[4]) -> unit effect {wreg} wPSTATE_NZCV +val forall Nat 'N, 'N IN {32,64}. (unit, bit['N]) -> unit effect {rreg,wreg} wSP +val forall Nat 'N, 'N IN {32,64}. (reg_index,bit['N]) -> unit effect {wreg} wX + +typedef ast = const union +{ + (exist 'R, 'R in {32,64}. (reg_index,reg_index,[:'R:],boolean,boolean,bit['R])) AddSubImmediate; +} + +val ast -> unit effect {rreg,wreg(*,rmem,barr,eamem,wmv,escape*)} execute +scattered function unit execute + +val bit[32] -> option<(ast)> effect pure decodeAddSubtractImmediate + +(* ADD/ADDS (immediate) *) +(* SUB/SUBS (immediate) *) +function option<(ast)> effect pure decodeAddSubtractImmediate ([sf]:[op]:[S]:0b10001:(bit[2]) shift:(bit[12]) imm12:(reg_size) Rn:(reg_size) Rd) = +{ + (reg_index) d := UInt_reg(Rd); + (reg_index) n := UInt_reg(Rn); + let (exist 'R, 'R in {32,64}. [:'R:]) 'datasize = if sf then 64 else 32 in { + (boolean) sub_op := op; + (boolean) setflags := S; + (bit['datasize]) imm := 0; (* ARM: uninitialized *) + + switch shift { + case 0b00 -> imm := ZeroExtend(imm12) + case 0b01 -> imm := ZeroExtend(imm12 : (0b0 ^^ 12)) + case [bitone,_] -> ReservedValue() + }; + + Some(AddSubImmediate( (d,n,datasize,sub_op,setflags,imm) )); +}} + +function clause execute (AddSubImmediate('datasize)) = { +switch datasize { +case (d,n,datasize,sub_op,setflags,imm) -> +{ + (bit['datasize]) operand1 := if n == 31 then rSP() else rX(n); + (bit['datasize]) operand2 := imm; + (bit) carry_in := bitzero; (* ARM: uninitialized *) + + if sub_op then { + operand2 := NOT(operand2); + carry_in := bitone; + } + else + carry_in := bitzero; + + let (result,nzcv) = (AddWithCarry(operand1, operand2, carry_in)) in { + + if setflags then + wPSTATE_NZCV() := nzcv; + + if (d == 31 & ~(setflags)) then + wSP() := result + else + wX(d) := result; + } +}}} +end execute diff --git a/test/mono/fnreduce.sail b/test/mono/fnreduce.sail new file mode 100644 index 00000000..f39fb87d --- /dev/null +++ b/test/mono/fnreduce.sail @@ -0,0 +1,69 @@ +(* Test constant propagation part of monomorphisation involving + functions. We should reduce a function application when the + arguments are suitable values, the function is pure and the result + is a value. + *) + +typedef AnEnum = enumerate { One; Two; Three } + +typedef EnumlikeUnion = const union { First; Second } + +typedef ProperUnion = const union { + (AnEnum) Stuff; + (EnumlikeUnion) Nonsense; +} + +function AnEnum canReduce ((AnEnum) x) = { + switch (x) { + case One -> Two + case x -> x + } +} + +function nat cannotReduce ((AnEnum) x) = { + let (nat) y = switch (x) { case One -> 1 case _ -> 5 } in + 2 + y +} + +function AnEnum effect {rreg} fakeUnpure ((AnEnum) x) = { + switch (x) { + case One -> Two + case x -> x + } +} + +function EnumlikeUnion canReduceUnion ((AnEnum) x) = { + switch (x) { + case One -> First + case _ -> Second + } +} + +function ProperUnion canReduceUnion2 ((AnEnum) x) = { + switch (x) { + case One -> Nonsense(First) + case y -> Stuff(y) + } +} + +(* FIXME LATER: once effect handling is in place we should get an error + because this isn't pure *) + +val AnEnum -> (AnEnum,nat,AnEnum,EnumlikeUnion,ProperUnion) effect pure test + +function test (x) = { + let a = canReduce(x) in + let b = cannotReduce(x) in + let c = fakeUnpure(x) in + let d = canReduceUnion(x) in + let e = canReduceUnion2(x) in + (a,b,c,d,e) +} + +val unit -> bool effect pure run + +function run () = { + test(One) == (Two,3,Two,First,Nonsense(First)) & + test(Two) == (Two,7,Two,Second,Stuff(Two)) & + test(Three) == (Three,7,Three,Second,Stuff(Three)) +} diff --git a/test/mono/test.ml b/test/mono/test.ml new file mode 100644 index 00000000..f99abfb8 --- /dev/null +++ b/test/mono/test.ml @@ -0,0 +1 @@ +if Testout_embed_sequential.run() then print_endline "OK" else print_endline "Failed";; diff --git a/test/mono/test.sh b/test/mono/test.sh new file mode 100755 index 00000000..2a5aa80b --- /dev/null +++ b/test/mono/test.sh @@ -0,0 +1,44 @@ +#!/bin/bash + +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +SAILDIR="$DIR/../.." +LEMDIR="$DIR/../../../lem" +OUTDIR="$DIR/test-out" +ZARITH="$LEMDIR/ocaml-lib/dependencies/zarith" + +if [ ! -d "$OUTDIR" ]; then + mkdir -- "$OUTDIR" +fi +cd "$OUTDIR" + +TESTONLY="$1" +if [ -n "$TESTONLY" ]; then shift; fi + +LOG="$DIR/log" +date > "$LOG" + +exec 3< "$DIR/tests" +set +e + +while read -u 3 TEST ARGS; do + if [ -z "$TESTONLY" -o "$TEST" = "$TESTONLY" ]; then +# echo "$TEST ocaml" +# rm -f -- "$OUTDIR"/* +# "$SAILDIR/sail" -ocaml "$SAILDIR/lib/prelude.sail" "$SAILDIR/lib/prelude_wrappers.sail" "$DIR/$TEST" -o "$OUTDIR/testout" $ARGS +# cp -- "$SAILDIR"/src/gen_lib/sail_values.ml . +# cp -- "$DIR"/test.ml . +# ocamlc -I "$ZARITH" "$ZARITH/zarith.cma" -dllpath "$ZARITH" -I "$LEMDIR/ocaml-lib" "$LEMDIR/ocaml-lib/extract.cma" -I "$SAILDIR/src/_build/lem_interp" "$SAILDIR/src/_build/lem_interp/extract.cma" sail_values.ml testout.ml test.ml -o test +# ./test + + echo "$TEST lem - ocaml" | tee -a -- "$LOG" + rm -f -- "$OUTDIR"/* + "$SAILDIR/sail" -lem -lem_sequential -lem_mwords "$SAILDIR/lib/prelude.sail" "$SAILDIR/lib/prelude_wrappers.sail" "$DIR/$TEST".sail -o "$OUTDIR/testout" $ARGS $@ &>> "$LOG" && \ + "$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$SAILDIR/src/gen_lib/sail_values.lem" "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" "$SAILDIR/src/gen_lib/state.lem" testout_embed_types_sequential.lem testout_embed_sequential.lem -outdir "$OUTDIR" &>> "$LOG" && \ + cp -- "$DIR"/test.ml "$OUTDIR" && \ + ocamlc -I "$ZARITH" "$ZARITH/zarith.cma" -dllpath "$ZARITH" -I "$LEMDIR/ocaml-lib" "$LEMDIR/ocaml-lib/extract.cma" -I "$SAILDIR/src/_build/lem_interp" "$SAILDIR/src/_build/lem_interp/extract.cma" sail_values.ml sail_operators_mwords.ml state.ml testout_embed_types_sequential.ml testout_embed_sequential.ml test.ml -o test &>> "$LOG" && \ + ./test |& tee -a -- "$LOG" || \ + (echo "Failed:"; echo; tail -- "$LOG"; echo; echo) + fi +done diff --git a/test/mono/tests b/test/mono/tests new file mode 100644 index 00000000..0825c686 --- /dev/null +++ b/test/mono/tests @@ -0,0 +1,4 @@ +fnreduce -mono-split fnreduce.sail:43:x +varmatch -mono-split varmatch.sail:7:x +vector -mono-split vector.sail:7:sel +union-exist -mono-split union-exist.sail:9:v diff --git a/test/mono/union-exist.sail b/test/mono/union-exist.sail new file mode 100644 index 00000000..74ab429a --- /dev/null +++ b/test/mono/union-exist.sail @@ -0,0 +1,33 @@ +default Order dec + +typedef myunion = const union { + (exist 'n, 'n in {8,16}. ([:'n:],bit['n])) MyConstr; +} + +val bit[2] -> myunion effect pure make + +function make(v) = + (* Can't mention these below without running into exp/nexp parsing conflict! *) + let eight = 8 in let sixteen = 16 in + switch v { + case 0b00 -> MyConstr( ( eight, 0x12) ) + case 0b01 -> MyConstr( (sixteen,0x1234) ) + case 0b10 -> MyConstr( ( eight, 0x56) ) + case 0b11 -> MyConstr( (sixteen,0x5678) ) + } + +val myunion -> bit[32] effect pure use + +function use(MyConstr('n)) = { + switch n { + case (n,v) -> extz(v) + } +} +val unit -> bool effect pure run + +function run () = { + use(make(0b00)) == 0x00000012 & + use(make(0b01)) == 0x00001234 & + use(make(0b10)) == 0x00000056 & + use(make(0b11)) == 0x00005678 +} diff --git a/test/mono/varmatch.sail b/test/mono/varmatch.sail new file mode 100644 index 00000000..7d2b9b73 --- /dev/null +++ b/test/mono/varmatch.sail @@ -0,0 +1,19 @@ +(* Check that when we case split on a variable that the constant propagation + handles the default case correctly. *) + +typedef AnEnum = enumerate { One; Two; Three } + +function AnEnum foo((AnEnum) x) = { + switch (x) { + case One -> Two + case y -> y + } +} + +val unit -> bool effect pure run + +function run () = { + foo(One) == Two & + foo(Two) == Two & + foo(Three) == Three +} diff --git a/test/mono/vector.sail b/test/mono/vector.sail new file mode 100644 index 00000000..03f36da5 --- /dev/null +++ b/test/mono/vector.sail @@ -0,0 +1,21 @@ +(* Check case splitting on a vector *) + +default Order dec + +val bit[32] -> nat effect pure test + +function nat test((bit[2]) sel : (bit[30]) _) = { + switch (sel) { + case 0b00 -> 5 + case 0b10 -> 1 + case _ -> 0 + } +} + +val unit -> bool effect pure run + +function run () = { + test(0x0f353533) == 5 & + test(0x84534656) == 1 & + test(0xf3463903) == 0 +} |