Adds the DC and IC instructions to AArch64_small;

Also, removes etc/regfp.sail and etc/regfp2.sail in favour of lib/regfp.sail

11 files changed, 187 insertions, 205 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 5e0b8cf9..d52099c0 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"); None ();},
+
+    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)),
+          _ => {assert(false); None ();}
+        },
+
+    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)),
+          _ => {assert(false); None ();}
+        },
+
+    Sys_TLBI => {not_implemented("TLBI"); None ();},
+
+    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
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/etc/regfp.sail b/etc/regfp.sail
deleted file mode 100644
index de842c5c..00000000
--- a/etc/regfp.sail
+++ /dev/null
@@ -1,95 +0,0 @@
-(* iR : input registers,
- * oR : output registers,
- * aR : registers feeding into the memory address *)
-
-(* branch instructions currently are not writing to NIA *)
-
-typedef regfp = const union {
-   (string) RFull;
-   (string,nat,nat) RSlice;
-   (string,nat) RSliceBit;
-   (string,string) RField;
-}
-
-typedef regfps = list <regfp>
-
-typedef niafp = const union {
-  NIAFP_successor;
-  (bit[64]) NIAFP_concrete_address;
-  NIAFP_indirect_address;
-}
-
-typedef niafps = list <niafp>
-
-(* only for MIPS *)
-typedef diafp = const union {
-  DIAFP_none;
-  (bit[64]) DIAFP_concrete;
-  (regfp) DIAFP_reg;
-}
-
-typedef read_kind = enumerate {
-  Read_plain;
-  Read_reserve;
-  Read_acquire;
-  Read_exclusive;
-  Read_exclusive_acquire;
-  Read_stream;
-  Read_RISCV_acquire;
-  Read_RISCV_strong_acquire;
-  Read_RISCV_reserved;
-  Read_RISCV_reserved_acquire;
-  Read_RISCV_reserved_strong_acquire;
-  Read_X86_locked;
-}
-
-typedef write_kind = enumerate {
-  Write_plain;
-  Write_conditional;
-  Write_release;
-  Write_exclusive;
-  Write_exclusive_release;
-  Write_RISCV_release;
-  Write_RISCV_strong_release;
-  Write_RISCV_conditional;
-  Write_RISCV_conditional_release;
-  Write_RISCV_conditional_strong_release;
-  Write_X86_locked;
-}
-
-typedef barrier_kind = enumerate {
-  Barrier_Sync;
-  Barrier_LwSync;
-  Barrier_Eieio;
-  Barrier_Isync;
-  Barrier_DMB;
-  Barrier_DMB_ST;
-  Barrier_DMB_LD;
-  Barrier_DSB;
-  Barrier_DSB_ST;
-  Barrier_DSB_LD;
-  Barrier_ISB;
-  Barrier_MIPS_SYNC;
-  Barrier_RISCV_rw_rw;
-  Barrier_RISCV_r_rw;
-  Barrier_RISCV_r_r;
-  Barrier_RISCV_rw_w;
-  Barrier_RISCV_w_w;
-  Barrier_RISCV_tso;
-  Barrier_RISCV_i;
-  Barrier_x86_MFENCE;
-}
-
-typedef trans_kind = enumerate {
-  Transaction_start; Transaction_commit; Transaction_abort;
-}
-
-typedef instruction_kind = const union {
-  (barrier_kind) IK_barrier;
-  (read_kind) IK_mem_read;
-  (write_kind) IK_mem_write;
-  (read_kind, write_kind) IK_mem_rmw;
-  IK_branch;
-  (trans_kind) IK_trans;
-  IK_simple
-}
diff --git a/etc/regfp2.sail b/etc/regfp2.sail
deleted file mode 100644
index 85141853..00000000
--- a/etc/regfp2.sail
+++ /dev/null
@@ -1,97 +0,0 @@
-/* iR : input registers,
- * oR : output registers,
- * aR : registers feeding into the memory address */
-
-/* branch instructions currently are not writing to NIA */
-
-union regfp = {
-   RFull : string,
-   RSlice : (string,nat,nat),
-   RSliceBit : (string,nat),
-   RField : (string,string),
-}
-
-type regfps = list(regfp)
-
-union niafp = {
-  NIAFP_successor : unit,
-  NIAFP_concrete_address : bits(64),
-  NIAFP_indirect_address : unit,
-}
-
-type niafps = list(niafp)
-
-/* only for MIPS */
-union diafp = {
-  DIAFP_none : unit,
-  DIAFP_concrete : bits(64),
-  DIAFP_reg : regfp,
-}
-
-enum read_kind = {
-  Read_plain,
-  Read_reserve,
-  Read_acquire,
-  Read_exclusive,
-  Read_exclusive_acquire,
-  Read_stream,
-  Read_RISCV_acquire,
-  Read_RISCV_strong_acquire,
-  Read_RISCV_reserved,
-  Read_RISCV_reserved_acquire,
-  Read_RISCV_reserved_strong_acquire,
-  Read_X86_locked
-}
-
-enum write_kind = {
-  Write_plain,
-  Write_conditional,
-  Write_release,
-  Write_exclusive,
-  Write_exclusive_release,
-  Write_RISCV_release,
-  Write_RISCV_strong_release,
-  Write_RISCV_conditional,
-  Write_RISCV_conditional_release,
-  Write_RISCV_conditional_strong_release,
-  Write_X86_locked
-}
-
-enum barrier_kind = {
-  Barrier_Sync,
-  Barrier_LwSync,
-  Barrier_Eieio,
-  Barrier_Isync,
-  Barrier_DMB,
-  Barrier_DMB_ST,
-  Barrier_DMB_LD,
-  Barrier_DSB,
-  Barrier_DSB_ST,
-  Barrier_DSB_LD,
-  Barrier_ISB,
-  Barrier_MIPS_SYNC,
-  Barrier_RISCV_rw_rw,
-  Barrier_RISCV_r_rw,
-  Barrier_RISCV_r_r,
-  Barrier_RISCV_rw_w,
-  Barrier_RISCV_w_w,
-  Barrier_RISCV_tso,
-  Barrier_RISCV_i,
-  Barrier_x86_MFENCE
-}
-
-enum trans_kind = {
-  Transaction_start, 
-  Transaction_commit, 
-  Transaction_abort
-}
-
-union instruction_kind = {
-  IK_barrier : barrier_kind,
-  IK_mem_read : read_kind,
-  IK_mem_write : write_kind,
-  IK_mem_rmw : (read_kind, write_kind),
-  IK_branch : unit,
-  IK_trans : trans_kind,
-  IK_simple : unit,
-}
diff --git a/lib/regfp.sail b/lib/regfp.sail
index cc017585..6044e1cc 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -90,6 +90,16 @@ enum trans_kind = {
   Transaction_abort
 }
 
+/* cache maintenance instructions */
+enum cache_op_kind = {
+  /* AArch64 DC */
+  Cache_op_D_IVAC, Cache_op_D_ISW,  Cache_op_D_CSW,  Cache_op_D_CISW,
+  Cache_op_D_ZVA,  Cache_op_D_CVAC, Cache_op_D_CVAU, Cache_op_D_CIVAC,
+  /* AArch64 IC */
+  Cache_op_I_IALLUIS, Cache_op_I_IALLU, Cache_op_I_IVAU
+}
+
+
 union instruction_kind = {
   IK_barrier : barrier_kind,
   IK_mem_read : read_kind,
@@ -97,5 +107,6 @@ union instruction_kind = {
   IK_mem_rmw : (read_kind, write_kind),
   IK_branch : unit,
   IK_trans : trans_kind,
-  IK_simple : unit
+  IK_simple : unit,
+  IK_cache_op : cache_op_kind
 }
diff --git a/power/Makefile b/power/Makefile
index f7c49e00..be97aa0b 100644
--- a/power/Makefile
+++ b/power/Makefile
@@ -1,7 +1,7 @@
 SAIL:=../src/sail.native
 LEM:=../../lem/lem
 
-SOURCES:=power.sail ../etc/regfp.sail power_regfp.sail
+SOURCES:=power.sail ../lib/regfp.sail power_regfp.sail
 
 
 all: power.lem power.ml power_embed.lem
diff --git a/x86/Makefile b/x86/Makefile
index 6863714d..0c6e830e 100644
--- a/x86/Makefile
+++ b/x86/Makefile
@@ -1,7 +1,7 @@
 SAIL=../src/sail.native
 LEM:=../../lem/lem
 
-SOURCES=../etc/regfp.sail x64.sail
+SOURCES=../lib/regfp.sail x64.sail
 
 all: x86.lem x86.ml x86_embed.lem