Make sure everything builds correctly

Move updated 0.11 lem files from Shaked's commit into their own directory

Remove the 0.7.1 lem directory that performed a similar purpose during the prompt monad changes

Re-add model changes from Shaked's commit with a feature flag

2 files changed, 220 insertions, 0 deletions

diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
index 34572f8..ec8c96f 100644
--- a/model/riscv_analysis.sail
+++ b/model/riscv_analysis.sail
@@ -10,6 +10,8 @@ let GPRstr : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26
 let CIA_fp = RFull("CIA")
 let NIA_fp = RFull("NIA")
 
+$ifndef FEATURE_UNION_BARRIER
+
 function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = {
   iR = [| |] : regfps;
   oR = [| |] : regfps;
@@ -180,3 +182,177 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
   };
   (iR,oR,aR,Nias,Dia,ik)
 }
+
+$else
+
+function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = {
+  iR = [| |] : regfps;
+  oR = [| |] : regfps;
+  aR = [| |] : regfps;
+  ik = IK_simple() : instruction_kind;
+  Nias = [| NIAFP_successor() |] : niafps;
+  Dia = DIAFP_none() : diafp;
+
+  match instr {
+     EBREAK() => (),
+     UTYPE(imm, rd, op) => {
+            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+     },
+     RISCV_JAL(imm, rd) => {
+            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            let offset : bits(64) = EXTS(imm) in
+            Nias = [| NIAFP_concrete_address (PC + offset) |];
+            ik = IK_branch();
+     },
+     RISCV_JALR(imm, rs, rd) => {
+            if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            let offset : bits(64) = EXTS(imm) in
+            Nias = [| NIAFP_indirect_address() |];
+            ik = IK_branch();
+     },
+     BTYPE(imm, rs2, rs1, op) => {
+            if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+            ik = IK_branch();
+            let offset : bits(64) = EXTS(imm) in
+            Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
+      },
+      ITYPE(imm, rs, rd, op) => {
+            if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+      },
+      SHIFTIOP(imm, rs, rd, op) => {
+             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+      },
+      RTYPE(rs2, rs1, rd, op) => {
+             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+      },
+      CSR(csr, rs1, rd, is_imm, op) => {
+               let isWrite : bool = match op {
+                   CSRRW  => true,
+                   _      => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0
+               };
+               iR = RFull(csr_name(csr)) :: iR;
+               if ~(is_imm) then {
+                  iR = RFull(GPRstr[rs1]) :: iR;
+               };
+               if isWrite then {
+                  oR = RFull(csr_name(csr)) :: oR;
+               };
+               oR = RFull(GPRstr[rd]) :: oR;
+      },
+      LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */
+             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             aR = iR;
+             ik =
+               match (aq, rl) {
+                 (false, false) => IK_mem_read (Read_plain),
+                 (true,  false) => IK_mem_read (Read_RISCV_acquire),
+                 (true,  true)  => IK_mem_read (Read_RISCV_strong_acquire),
+
+                 _  => internal_error("LOAD type not implemented in initial_analysis")
+               }
+      },
+      STORE(imm, rs2, rs1, width, aq, rl) => {
+             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+             if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
+             ik =
+               match (aq, rl) {
+                 (false, false) => IK_mem_write (Write_plain),
+                 (false, true)  => IK_mem_write (Write_RISCV_release),
+                 (true,  true)  => IK_mem_write (Write_RISCV_strong_release),
+
+                 _ => internal_error("STORE type not implemented in initial_analysis")
+               }
+      },
+      ADDIW(imm, rs, rd) => {
+             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+      },
+      SHIFTW(imm, rs, rd, op) => {
+             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+      },
+      RTYPEW(rs2, rs1, rd, op) => {
+             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+      },
+      FENCE(pred, succ) => {
+             ik =
+               match (pred, succ) {
+		 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw ()),
+		 (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw ()),
+		 (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r ()),
+		 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w ()),
+		 (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w ()),
+		 (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw ()),
+		 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r ()),
+		 (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w ()),
+		 (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r ()),
+
+                 (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (),
+
+                 _ => internal_error("barrier type not implemented in initial_analysis")
+               };
+      },
+      FENCE_TSO(pred, succ) => {
+             ik =
+               match (pred, succ) {
+		 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()),
+                 _ => internal_error("barrier type not implemented in initial_analysis")
+               };
+      },
+     FENCEI() => {
+              ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
+     },
+     LOADRES(aq, rl, rs1, width, rd) => {
+            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            aR = iR;
+            ik = match (aq, rl) {
+              (false, false) => IK_mem_read (Read_RISCV_reserved),
+              (true,  false) => IK_mem_read (Read_RISCV_reserved_acquire),
+              (true,  true)  => IK_mem_read (Read_RISCV_reserved_strong_acquire),
+              (false, true)  => internal_error("LOADRES type not implemented in initial_analysis")
+            };
+     },
+     STORECON(aq, rl, rs2, rs1, width, rd) => {
+            if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+            if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
+            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             ik = match (aq, rl) {
+               (false, false) => IK_mem_write (Write_RISCV_conditional),
+               (false, true)  => IK_mem_write (Write_RISCV_conditional_release),
+               (true,  true)  => IK_mem_write (Write_RISCV_conditional_strong_release),
+
+               (true,  false) => internal_error("STORECON type not implemented in initial_analysis")
+             };
+      },
+      AMO(op, aq, rl, rs2, rs1, width, rd) => {
+             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+             if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
+             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             ik = match (aq, rl) {
+               (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional),
+               (false, true)  => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release),
+               (true,  false) => IK_mem_rmw (Read_RISCV_reserved_acquire,
+                                                                       Write_RISCV_conditional),
+               (true,  true)  => IK_mem_rmw (Read_RISCV_reserved_acquire,
+                                                                       Write_RISCV_conditional_release)
+             };
+      },
+        _ => ()
+  };
+  (iR,oR,aR,Nias,Dia,ik)
+}
+
+$endif
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 14a626e..636170b 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -564,6 +564,31 @@ union clause ast = FENCE : (bits(4), bits(4))
 mapping clause encdec = FENCE(pred, succ)
   <-> 0b0000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
+/* For future versions of Sail where barriers can be parameterised */
+$ifdef FEATURE_UNION_BARRIER
+
+function clause execute (FENCE(pred, succ)) = {
+  match (pred, succ) {
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw()),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw()),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r()),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w()),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w()),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw()),
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r()),
+    (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w()),
+    (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r()),
+
+    (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
+
+    _ => { print("FIXME: unsupported fence");
+           () }
+  };
+  RETIRE_SUCCESS
+}
+
+$else
+
 function clause execute (FENCE(pred, succ)) = {
   match (pred, succ) {
     (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw),
@@ -584,6 +609,8 @@ function clause execute (FENCE(pred, succ)) = {
   RETIRE_SUCCESS
 }
 
+$endif
+
 mapping bit_maybe_r : bits(1) <-> string = {
   0b1 <-> "r",
   0b0 <-> ""
@@ -617,6 +644,21 @@ union clause ast = FENCE_TSO : (bits(4), bits(4))
 mapping clause encdec = FENCE_TSO(pred, succ)
   <-> 0b1000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
+$ifdef FEATURE_UNION_BARRIER
+
+function clause execute (FENCE_TSO(pred, succ)) = {
+  match (pred, succ) {
+    (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso()),
+    (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
+
+    _ => { print("FIXME: unsupported fence");
+           () }
+  };
+  RETIRE_SUCCESS
+}
+
+$else
+
 function clause execute (FENCE_TSO(pred, succ)) = {
   match (pred, succ) {
     (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso),
@@ -628,6 +670,8 @@ function clause execute (FENCE_TSO(pred, succ)) = {
   RETIRE_SUCCESS
 }
 
+$endif
+
 mapping clause assembly = FENCE_TSO(pred, succ)
   <-> "fence.tso" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)