Merge branch 'sail2' into rmem_interpreter

15 files changed, 188 insertions, 10 deletions

diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile
index 3a5da685..b9abec80 100644
--- a/aarch64_small/Makefile
+++ b/aarch64_small/Makefile
@@ -24,7 +24,7 @@ armV8.ml: armV8.lem ../src/lem_interp/interp_ast.lem
 	$(LEM) -ocaml -lib ../src/lem_interp/ $<
 
 
-armV8_embed.lem: $(SOURCES) ../etc/regfp2.sail aarch64_regfp.sail
+armV8_embed.lem: $(SOURCES) ../lib/regfp.sail aarch64_regfp.sail
 # also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem
 	$(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^
 
diff --git a/aarch64_small/aarch64_regfp.sail b/aarch64_small/aarch64_regfp.sail
index 55f4a16b..ce155f0a 100644
--- a/aarch64_small/aarch64_regfp.sail
+++ b/aarch64_small/aarch64_regfp.sail
@@ -240,6 +240,32 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
           IK_barrier(Barrier_ISB)
       };
     },
+
+    (DataCache(t,dc_op)) => {
+      iR = appendL(iR,xFP(t));
+
+      ik = match dc_op {
+        IVAC  => not_implemented("DC IVAC"),
+        ISW   => not_implemented("DC ISW"),
+        CSW   => not_implemented("DC CSW"),
+        CISW  => not_implemented("DC CISW"),
+        ZVA   => not_implemented("DC ZVA"),
+        CVAC  => not_implemented("DC CVAC"),
+        CVAU  => IK_cache_op(Cache_op_D_CVAU),
+        CIVAC => not_implemented("DC CIVAC")
+      };
+    },
+
+    (InstructionCache(t,ic_op)) => {
+      iR = appendL(iR,xFP(t));
+
+      ik = match ic_op {
+        IALLUIS => not_implemented("IC IALLUIS"),
+        IALLU   => not_implemented("IC IALLU"),
+        IVAU    => IK_cache_op(Cache_op_I_IVAU)
+      };
+    },
+
     (System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result))  => {
       oR = appendL(oR,xFP(t));
       not_implemented("System"); /* because SysOp_R and SysOp_W */
diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail
index d0278d9d..b1eac1e7 100644
--- a/aarch64_small/armV8.h.sail
+++ b/aarch64_small/armV8.h.sail
@@ -64,6 +64,10 @@ bitfield TMSTATUS_type : bits(64) =
 register TMAbortEffect : TMSTATUS_type /* we abuse the register write to pass out the status value */
 register TMStartEffect : TMSTATUS_type /* we abuse the register read to pass in the status value */
 
+/* abuse register write effect, instead of adding proper effects: */
+register data_cache_operation_CVAU : bits(64)
+register instruction_cache_operation_IVAU : bits(64)
+
 /* General purpose registers */
 
 register R30 : bits(64)
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index 8e893e4b..f125ec72 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -61,6 +61,8 @@ union ast =  {
   ClearExclusiveMonitor : (uinteger),
   Barrier : (MemBarrierOp,MBReqDomain,MBReqTypes),
   System : (reg_index,uinteger,uinteger,uinteger,uinteger,uinteger,boolean),
+  DataCache : (reg_index,DCOp),
+  InstructionCache : (reg_index,ICOp),
   MoveSystemRegister : (reg_index,uinteger,uinteger,uinteger,uinteger,uinteger,boolean),
   TestBitAndBranch : {'R 'bit_pos, RegisterSize('R) & 0 <= 'bit_pos < 'R. (reg_index,int('R),int('bit_pos),bit,bits(64))},
   BranchImmediate : (BranchType,bits(64)),
@@ -462,24 +464,84 @@ function clause execute ( Barrier(op,domain,types) ) = {
 
 /* SYS L=0b0 */
 /* SYSL L=0b1 */
+/* The following are actually aliases of SYS: */
+/* DC L=0b0,SysOp(op1,CRn,CRm,op2) = Sys_DC */
+/* IC L=0b0,SysOp(op1,CRn,CRm,op2) = Sys_IC */
 function clause decodeSystem (0b1101010100@[L]@0b01@(op1 : bits(3))@(CRn : bits(4))@(CRm : bits(4))@(op2 : bits(3))@(Rt:bits(5))) = {
   /* FIXME: we don't allow register reads in the decoding */
   /* ARM: CheckSystemAccess(0b01, op1, CRn, CRm, op2, Rt, L);*/
 
   t : reg_index = UInt_reg(Rt);
 
-  sys_op0 : uinteger = 1;
-  sys_op1 : uinteger = UInt(op1);
-  sys_op2 : uinteger = UInt(op2);
-  sys_crn : uinteger = UInt(CRn);
-  sys_crm : uinteger = UInt(CRm);
-  has_result : boolean = (L == b1);
+  sysop : SystemOp = Sys_SYS;
+  if L == b0 then
+    sysop = SysOp(op1,CRn,CRm,op2);
+
+  match sysop {
+    Sys_AT => not_implemented("AT"),
+
+    Sys_DC =>
+        match (op1, CRm, op2) {
+          (0b000, 0b0110, 0b001) => Some(DataCache(t,IVAC)),
+          (0b000, 0b0110, 0b010) => Some(DataCache(t,ISW)),
+          (0b000, 0b1010, 0b010) => Some(DataCache(t,CSW)),
+          (0b000, 0b1110, 0b010) => Some(DataCache(t,CISW)),
+          (0b011, 0b0100, 0b001) => Some(DataCache(t,ZVA)),
+          (0b011, 0b1010, 0b001) => Some(DataCache(t,CVAC)),
+          (0b011, 0b1011, 0b001) => Some(DataCache(t,CVAU)),
+          (0b011, 0b1110, 0b001) => Some(DataCache(t,CIVAC)),
+          _ => error("should never happen")
+        },
+
+    Sys_IC =>
+        match (op1, CRm, op2) {
+          (0b000, 0b0001, 0b000) => Some(InstructionCache(t,IALLUIS)),
+          (0b000, 0b0101, 0b000) => Some(InstructionCache(t,IALLU)),
+          (0b011, 0b0101, 0b001) => Some(InstructionCache(t,IVAU)),
+          _ => error("should never happen")
+        },
+
+    Sys_TLBI => not_implemented("TLBI"),
+
+    Sys_SYS => {
+      sys_op0 : uinteger = 1;
+      sys_op1 : uinteger = UInt(op1);
+      sys_op2 : uinteger = UInt(op2);
+      sys_crn : uinteger = UInt(CRn);
+      sys_crm : uinteger = UInt(CRm);
+      has_result : boolean = (L == b1);
+
+      Some(System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result));
+    }
+  };
+}
 
-  Some(System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result));
+function clause execute ( DataCache(t,dc_op) ) = {
+  addr : bits(64) = rX(t);
+
+  match dc_op {
+    IVAC  => not_implemented("DC IVAC"),
+    ISW   => not_implemented("DC ISW"),
+    CSW   => not_implemented("DC CSW"),
+    CISW  => not_implemented("DC CISW"),
+    ZVA   => not_implemented("DC ZVA"),
+    CVAC  => not_implemented("DC CVAC"),
+    CVAU  => data_cache_operation_CVAU = addr,
+    CIVAC => not_implemented("DC CIVAC")
+  };
 }
 
-function clause execute ( System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result) ) =
-{
+function clause execute ( InstructionCache(t,ic_op) ) = {
+  addr : bits(64) = rX(t);
+
+  match ic_op {
+    IALLUIS => not_implemented("IC IALLUIS"),
+    IALLU   => not_implemented("IC IALLU"),
+    IVAU    => instruction_cache_operation_IVAU = addr
+  };
+}
+
+function clause execute ( System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result) ) = {
   if has_result then
     wX(t) = SysOp_R(sys_op0, sys_op1, sys_crn, sys_crm, sys_op2)
   else
@@ -2443,6 +2505,7 @@ end execute
 val supported_instructions : ast -> option(ast) effect {escape}
 function supported_instructions (instr) = {
   match instr {
+    Unallocated () => None (),
     _  => Some(instr)
   }
 }
diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail
index ee9eabc9..cc65a03e 100644
--- a/aarch64_small/armV8_A64_lib.sail
+++ b/aarch64_small/armV8_A64_lib.sail
@@ -898,6 +898,70 @@ function Prefetch(address : bits(64), prfop : bits(5)) -> unit = {
 /** ENUMERATE:aarch64/instrs/system/barriers/barrierop/MemBarrierOp */
 /** ENUMERATE:aarch64/instrs/system/hints/syshintop/SystemHintOp */
 /** ENUMERATE:aarch64/instrs/system/register/cpsr/pstatefield/PSTATEField */
+/** FUNCTION:aarch64/instrs/system/sysops/sysop/SysOp */
+
+function SysOp(op1 : bits(3), CRn : bits(4), CRm : bits(4), op2 : bits(3)) -> SystemOp = {
+  match (op1@CRn@CRm@op2) {
+    (0b000@0b0111@0b1000@0b000) => Sys_AT,   /* S1E1R        */
+    (0b100@0b0111@0b1000@0b000) => Sys_AT,   /* S1E2R        */
+    (0b110@0b0111@0b1000@0b000) => Sys_AT,   /* S1E3R        */
+    (0b000@0b0111@0b1000@0b001) => Sys_AT,   /* S1E1W        */
+    (0b100@0b0111@0b1000@0b001) => Sys_AT,   /* S1E2W        */
+    (0b110@0b0111@0b1000@0b001) => Sys_AT,   /* S1E3W        */
+    (0b000@0b0111@0b1000@0b010) => Sys_AT,   /* S1E0R        */
+    (0b000@0b0111@0b1000@0b011) => Sys_AT,   /* S1E0W        */
+    (0b100@0b0111@0b1000@0b100) => Sys_AT,   /* S12E1R       */
+    (0b100@0b0111@0b1000@0b101) => Sys_AT,   /* S12E1W       */
+    (0b100@0b0111@0b1000@0b110) => Sys_AT,   /* S12E0R       */
+    (0b100@0b0111@0b1000@0b111) => Sys_AT,   /* S12E0W       */
+    (0b011@0b0111@0b0100@0b001) => Sys_DC,   /* ZVA          */
+    (0b000@0b0111@0b0110@0b001) => Sys_DC,   /* IVAC         */
+    (0b000@0b0111@0b0110@0b010) => Sys_DC,   /* ISW          */
+    (0b011@0b0111@0b1010@0b001) => Sys_DC,   /* CVAC         */
+    (0b000@0b0111@0b1010@0b010) => Sys_DC,   /* CSW          */
+    (0b011@0b0111@0b1011@0b001) => Sys_DC,   /* CVAU         */
+    (0b011@0b0111@0b1110@0b001) => Sys_DC,   /* CIVAC        */
+    (0b000@0b0111@0b1110@0b010) => Sys_DC,   /* CISW         */
+    (0b000@0b0111@0b0001@0b000) => Sys_IC,   /* IALLUIS      */
+    (0b000@0b0111@0b0101@0b000) => Sys_IC,   /* IALLU        */
+    (0b011@0b0111@0b0101@0b001) => Sys_IC,   /* IVAU         */
+    (0b100@0b1000@0b0000@0b001) => Sys_TLBI, /* IPAS2E1IS    */
+    (0b100@0b1000@0b0000@0b101) => Sys_TLBI, /* IPAS2LE1IS   */
+    (0b000@0b1000@0b0011@0b000) => Sys_TLBI, /* VMALLE1IS    */
+    (0b100@0b1000@0b0011@0b000) => Sys_TLBI, /* ALLE2IS      */
+    (0b110@0b1000@0b0011@0b000) => Sys_TLBI, /* ALLE3IS      */
+    (0b000@0b1000@0b0011@0b001) => Sys_TLBI, /* VAE1IS       */
+    (0b100@0b1000@0b0011@0b001) => Sys_TLBI, /* VAE2IS       */
+    (0b110@0b1000@0b0011@0b001) => Sys_TLBI, /* VAE3IS       */
+    (0b000@0b1000@0b0011@0b010) => Sys_TLBI, /* ASIDE1IS     */
+    (0b000@0b1000@0b0011@0b011) => Sys_TLBI, /* VAAE1IS      */
+    (0b100@0b1000@0b0011@0b100) => Sys_TLBI, /* ALLE1IS      */
+    (0b000@0b1000@0b0011@0b101) => Sys_TLBI, /* VALE1IS      */
+    (0b100@0b1000@0b0011@0b101) => Sys_TLBI, /* VALE2IS      */
+    (0b110@0b1000@0b0011@0b101) => Sys_TLBI, /* VALE3IS      */
+    (0b100@0b1000@0b0011@0b110) => Sys_TLBI, /* VMALLS12E1IS */
+    (0b000@0b1000@0b0011@0b111) => Sys_TLBI, /* VAALE1IS     */
+    (0b100@0b1000@0b0100@0b001) => Sys_TLBI, /* IPAS2E1      */
+    (0b100@0b1000@0b0100@0b101) => Sys_TLBI, /* IPAS2LE1     */
+    (0b000@0b1000@0b0111@0b000) => Sys_TLBI, /* VMALLE1      */
+    (0b100@0b1000@0b0111@0b000) => Sys_TLBI, /* ALLE2        */
+    (0b110@0b1000@0b0111@0b000) => Sys_TLBI, /* ALLE3        */
+    (0b000@0b1000@0b0111@0b001) => Sys_TLBI, /* VAE1         */
+    (0b100@0b1000@0b0111@0b001) => Sys_TLBI, /* VAE2         */
+    (0b110@0b1000@0b0111@0b001) => Sys_TLBI, /* VAE3         */
+    (0b000@0b1000@0b0111@0b010) => Sys_TLBI, /* ASIDE1       */
+    (0b000@0b1000@0b0111@0b011) => Sys_TLBI, /* VAAE1        */
+    (0b100@0b1000@0b0111@0b100) => Sys_TLBI, /* ALLE1        */
+    (0b000@0b1000@0b0111@0b101) => Sys_TLBI, /* VALE1        */
+    (0b100@0b1000@0b0111@0b101) => Sys_TLBI, /* VALE2        */
+    (0b110@0b1000@0b0111@0b101) => Sys_TLBI, /* VALE3        */
+    (0b100@0b1000@0b0111@0b110) => Sys_TLBI, /* VMALLS12E1   */
+    (0b000@0b1000@0b0111@0b111) => Sys_TLBI, /* VAALE1       */
+    _ => Sys_SYS
+  };
+}
+
+/** ENUMERATE:aarch64/instrs/system/sysops/sysop/SystemOp */
 /** FUNCTION:aarch64/translation/faults/AArch64.AlignmentFault */
 
 function AArch64_AlignmentFault(acctype : AccType, iswrite : boolean, secondstage : boolean) -> FaultRecord = {
diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail
index 66071b3a..332ad18c 100644
--- a/aarch64_small/armV8_lib.h.sail
+++ b/aarch64_small/armV8_lib.h.sail
@@ -210,6 +210,13 @@ enum SystemHintOp =
 enum PSTATEField = 
   {PSTATEField_DAIFSet, PSTATEField_DAIFClr, PSTATEField_SP}
 
+enum SystemOp = {Sys_AT, Sys_DC, Sys_IC, Sys_TLBI, Sys_SYS}
+
+enum DCOp = {IVAC, ISW, CSW, CISW, ZVA, CVAC, CVAU, CIVAC}
+
+enum ICOp = {IALLUIS, IALLU, IVAU}
+
+
 val rPC : unit -> bits(64) effect {rreg}
 val rSP : forall 'N, 'N in {8,16,32,64}. implicit('N) -> bits('N) effect {rreg,escape}
 val wX : forall 'N, 'N in {8,16,32,64}. (reg_index,bits('N)) -> unit effect {wreg}
diff --git a/aarch64_small/gen/ast.hgen b/aarch64_small/gen/ast.hgen
index 60f130d7..98148a5c 100644
--- a/aarch64_small/gen/ast.hgen
+++ b/aarch64_small/gen/ast.hgen
@@ -1,3 +1,4 @@
+  | `AArch64Unallocated
   | `AArch64TMStart of inst_reg (* t *)
   | `AArch64TMCommit
   | `AArch64TMAbort of boolean*bit5 (* retry,reason *)
diff --git a/aarch64_small/gen/fold.hgen b/aarch64_small/gen/fold.hgen
index 4062d8e6..fbe52794 100644
--- a/aarch64_small/gen/fold.hgen
+++ b/aarch64_small/gen/fold.hgen
@@ -1,3 +1,4 @@
+| `AArch64Unallocated -> (y_reg, y_sreg)
 | `AArch64TMStart t -> fold_reg t (y_reg, y_sreg)
 | `AArch64TMCommit -> (y_reg, y_sreg)
 | `AArch64TMAbort (retry,reason) -> (y_reg, y_sreg)
diff --git a/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen b/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
index 6fbb3eb2..b8fe851c 100644
--- a/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
+++ b/aarch64_small/gen/herdtools_ast_to_shallow_ast.hgen
@@ -1,3 +1,4 @@
+| `AArch64Unallocated -> Unallocated
 | `AArch64TMStart t -> TMStart (translate_reg "t" t)
 
 | `AArch64TMCommit -> TMCommit
diff --git a/aarch64_small/gen/map.hgen b/aarch64_small/gen/map.hgen
index 62899c91..3d5419b4 100644
--- a/aarch64_small/gen/map.hgen
+++ b/aarch64_small/gen/map.hgen
@@ -1,3 +1,4 @@
+| `AArch64Unallocated -> `AArch64Unallocated
 | `AArch64TMStart t -> `AArch64TMStart (map_reg t)
 | `AArch64TMCommit -> `AArch64TMCommit
 | `AArch64TMAbort (retry,reason) -> `AArch64TMAbort (retry,reason)
diff --git a/aarch64_small/gen/pretty.hgen b/aarch64_small/gen/pretty.hgen
index 2bbf7af7..b412fdda 100644
--- a/aarch64_small/gen/pretty.hgen
+++ b/aarch64_small/gen/pretty.hgen
@@ -1,3 +1,6 @@
+| `AArch64Unallocated ->
+      "UNALLOCATED"
+
 | `AArch64TMStart t ->
       sprintf "TSTART %s" (pp_regzr Set64 t)
 
diff --git a/aarch64_small/gen/regs_out_in.hgen b/aarch64_small/gen/regs_out_in.hgen
index 724a574b..bab53be7 100644
--- a/aarch64_small/gen/regs_out_in.hgen
+++ b/aarch64_small/gen/regs_out_in.hgen
@@ -1,6 +1,7 @@
 (* for each instruction instance, identify the role of the registers
    and possible branching: (outputs, inputs, voidstars, branch) *)
 
+| `AArch64Unallocated -> failwith "UNALLOCATED is not implemented"
 | `AArch64TMStart t -> failwith "TSTART is not implemented"
 | `AArch64TMCommit -> failwith "TCOMMIT is not implemented"
 | `AArch64TMAbort (retry,reason) -> failwith "TABORT is not implemented"
diff --git a/aarch64_small/gen/sail_trans_out.hgen b/aarch64_small/gen/sail_trans_out.hgen
index 84826c18..0399fa8b 100644
--- a/aarch64_small/gen/sail_trans_out.hgen
+++ b/aarch64_small/gen/sail_trans_out.hgen
@@ -1,3 +1,5 @@
+| ("Unallocated", []) -> `AArch64Unallocated
+
 | ("TMStart", [t]) ->
   `AArch64TMStart (translate_out_regzr Set64 t)
 
diff --git a/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen b/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
index 7362304c..55179a97 100644
--- a/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
+++ b/aarch64_small/gen/shallow_ast_to_herdtools_ast.hgen
@@ -1,3 +1,5 @@
+| Unallocated -> `AArch64Unallocated
+
 | TMStart t ->
   `AArch64TMStart (translate_out_regzr Set64 t)
 
diff --git a/aarch64_small/gen/trans_sail.hgen b/aarch64_small/gen/trans_sail.hgen
index 2b176308..df2ed81c 100644
--- a/aarch64_small/gen/trans_sail.hgen
+++ b/aarch64_small/gen/trans_sail.hgen
@@ -1,3 +1,5 @@
+| `AArch64Unallocated -> ("Unallocated", [], [])
+
 | `AArch64TMStart t ->
     ("TMStart", [translate_reg "t" t], [])