Adapt first part of union monomorphisation to existential types

1 files changed, 75 insertions, 0 deletions

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