1 files changed, 0 insertions, 75 deletions
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