summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/monomorphise.ml18
-rw-r--r--test/mono/addsubexist.sail75
-rw-r--r--test/mono/assert.sail28
-rw-r--r--test/mono/fnreduce.sail8
-rw-r--r--test/mono/set.sail13
-rw-r--r--test/mono/test.ml4
-rw-r--r--test/mono/tests1
-rw-r--r--test/mono/union-exist.sail10
-rw-r--r--test/mono/varmatch.sail8
-rw-r--r--test/mono/vector.sail9
10 files changed, 68 insertions, 106 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index d14097af..2fe7cc33 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -993,6 +993,20 @@ let stop_at_false_assertions e =
let l = Generated Unknown in
E_aux (E_exit (E_aux (E_lit (L_aux (L_unit,l)),(l,None))),(l,None))
in
+ let rec nc_false (NC_aux (nc,_)) =
+ match nc with
+ | NC_false -> true
+ | NC_and (nc1,nc2) -> nc_false nc1 || nc_false nc2
+ | _ -> false
+ in
+ let rec exp_false (E_aux (e,_)) =
+ match e with
+ | E_constraint nc -> nc_false nc
+ | E_lit (L_aux (L_false,_)) -> true
+ | E_app (Id_aux (Id "and_bool",_),[e1;e2]) ->
+ exp_false e1 || exp_false e2
+ | _ -> false
+ in
let rec exp (E_aux (e,ann) as ea) =
match e with
| E_block es ->
@@ -1029,9 +1043,7 @@ let stop_at_false_assertions e =
let e2,stop = exp e2 in
E_aux (E_let (LB_aux (LB_val (p,e1),lbann),e2),ann), stop
end
- | E_assert (E_aux (E_constraint (NC_aux (NC_false,_)),_),_) ->
- ea, Some (typ_of_annot ann)
- | E_assert (E_aux (E_lit (L_aux (L_false,_)),_),_) ->
+ | E_assert (e1,_) when exp_false e1 ->
ea, Some (typ_of_annot ann)
| _ -> ea, None
in fst (exp e)
diff --git a/test/mono/addsubexist.sail b/test/mono/addsubexist.sail
deleted file mode 100644
index f59f596e..00000000
--- a/test/mono/addsubexist.sail
+++ /dev/null
@@ -1,75 +0,0 @@
-(* 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/assert.sail b/test/mono/assert.sail
index 5b4a013a..91826822 100644
--- a/test/mono/assert.sail
+++ b/test/mono/assert.sail
@@ -1,7 +1,21 @@
+$include <smt.sail>
+$include <flow.sail>
+default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+overload operator == = {eq_int, eq_vec}
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+overload operator < = {lt_atom, lt_int}
+
+/* Tests set constraints in different constraints */
+
val f : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
function f(n,m) = {
- assert(constraint('n in {8,16} & 'm < 'n));
+ assert(constraint('n in {8,16} & 'm < 'n), "nconstraint");
let 'p = 2 * n in
let x : bits('p) = replicate_bits(0b0,'p) in
()
@@ -10,7 +24,7 @@ function f(n,m) = {
val g : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
function g(n,m) = {
- assert(constraint('n in {8,16}) & 'm < 'n);
+ assert(constraint('n in {8,16}) & 'm < 'n, "set and exp");
let 'p = 2 * n in
let x : bits('p) = replicate_bits(0b0,'p) in
()
@@ -18,8 +32,16 @@ function g(n,m) = {
val h : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
function h(n,m) = {
- assert(('n == 8 | 'n == 16) & 'm < 'n);
+ assert(('n == 8 | 'n == 16) & 'm < 'n, "all exp");
let 'p = 2 * n in
let x : bits('p) = replicate_bits(0b0,'p) in
()
}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+ f(8,3);
+ g(16,3);
+ h(8,3);
+} \ No newline at end of file
diff --git a/test/mono/fnreduce.sail b/test/mono/fnreduce.sail
index 27d6b14a..cd58e71a 100644
--- a/test/mono/fnreduce.sail
+++ b/test/mono/fnreduce.sail
@@ -77,10 +77,10 @@ function test (x) = {
(a,b,c,d,e)
}
-val run : unit -> bool effect {rreg}
+val run : unit -> unit effect {rreg,escape}
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))
+ assert(test(One) == (Two,3,Two,First,Nonsense(First)));
+ assert(test(Two) == (Two,7,Two,Second,Stuff(Two)));
+ assert(test(Three) == (Three,7,Three,Second,Stuff(Three)));
}
diff --git a/test/mono/set.sail b/test/mono/set.sail
index 203f2219..b7cf4862 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -35,10 +35,11 @@ function depends(n) = {
extz(x)
}
-val run : unit -> bool
+val run : unit -> unit effect {escape}
-function run () =
- parametric(32) == 0x0000000080000000 &
- parametric(64) == 0xffffffff80000000 &
- depends(16) == 0x0000000080000000 &
- depends(32) == 0xffffffff80000000
+function run () = {
+ assert(parametric(32) == 0x0000000080000000);
+ assert(parametric(64) == 0xffffffff80000000);
+ assert(depends(16) == 0x0000000080000000);
+ assert(depends(32) == 0xffffffff80000000);
+}
diff --git a/test/mono/test.ml b/test/mono/test.ml
index efa1de54..dc194792 100644
--- a/test/mono/test.ml
+++ b/test/mono/test.ml
@@ -1 +1,3 @@
-if Testout.run() then print_endline "OK" else print_endline "Failed";;
+match Testout.run() with
+| Done _ -> print_endline "OK"
+| _ -> print_endline "Failed";;
diff --git a/test/mono/tests b/test/mono/tests
index 8847f03e..8f2c346d 100644
--- a/test/mono/tests
+++ b/test/mono/tests
@@ -7,3 +7,4 @@ varmatch -auto_mono
vector -auto_mono
union-exist -auto_mono
set -auto_mono
+assert -auto_mono
diff --git a/test/mono/union-exist.sail b/test/mono/union-exist.sail
index 9ec3ee33..f1e01e75 100644
--- a/test/mono/union-exist.sail
+++ b/test/mono/union-exist.sail
@@ -28,11 +28,11 @@ val use : myunion -> bits(32)
function use(MyConstr((n,v) as (atom('n),bits('n)))) = extz(v)
-val run : unit -> bool
+val run : unit -> unit effect {escape}
function run () = {
- use(make(0b00)) == 0x00000012 &
- use(make(0b01)) == 0x00001234 &
- use(make(0b10)) == 0x00000056 &
- use(make(0b11)) == 0x00005678
+ assert(use(make(0b00)) == 0x00000012);
+ assert(use(make(0b01)) == 0x00001234);
+ assert(use(make(0b10)) == 0x00000056);
+ assert(use(make(0b11)) == 0x00005678);
}
diff --git a/test/mono/varmatch.sail b/test/mono/varmatch.sail
index 279c16be..c3c2994d 100644
--- a/test/mono/varmatch.sail
+++ b/test/mono/varmatch.sail
@@ -15,10 +15,10 @@ function foo(x) = {
}
}
-val run : unit -> bool
+val run : unit -> unit effect {escape}
function run () = {
- foo(One) == Two &
- foo(Two) == Two &
- foo(Three) == Three
+ assert(foo(One) == Two);
+ assert(foo(Two) == Two);
+ assert(foo(Three) == Three);
}
diff --git a/test/mono/vector.sail b/test/mono/vector.sail
index 5740075b..93cc2d41 100644
--- a/test/mono/vector.sail
+++ b/test/mono/vector.sail
@@ -1,6 +1,5 @@
default Order dec
type bits ('n : Int) = vector('n, dec, bit)
-val operator & = "and_bool" : (bool, bool) -> bool
val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
overload operator == = {eq_int, eq_vec}
@@ -20,10 +19,10 @@ function test((sel : bits(2)) @ (_ : bits(30))) = {
}
}
-val run : unit -> bool
+val run : unit -> unit effect {escape}
function run () = {
- test(0x0f353533) == 5 &
- test(0x84534656) == 1 &
- test(0xf3463903) == 0
+ assert(test(0x0f353533) == 5);
+ assert(test(0x84534656) == 1);
+ assert(test(0xf3463903) == 0);
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 08:54:16 +0000