Changes to support CAS and RMW atomicity

plugins/asli/asli_lifter.ml

@@ -163,6 +163,14 @@ module Make(CT : Theory.Core) = struct
         KB.return (Z.to_int (Z.of_string_base 10 s))
     | _ -> fail (Failed_conversion "Unable to get option")
 
+  let invoke_symbol name =
+    let name = KB.Name.create
+        ~package:"intrinsic"
+        KB.Name.(unqualified@@read name) in
+    let* dst = Theory.Label.for_name (KB.Name.show name) in
+    KB.provide Theory.Label.is_subroutine dst (Some true) >>= fun () ->
+    CT.goto dst
+
   let rec compile_var (t: Asl_ast.ty) (ident: string) (value: Asl_ast.expr option): unit Theory.eff =
     let add_state t' = 
       let* var = Theory.Var.fresh t' in
@@ -369,7 +377,12 @@ module Make(CT : Theory.Core) = struct
         let value' = compile_expr value |> to_bits in
         let oldMem = get_var "mem" |> to_mem in
         let newMem = CT.storew CT.b0 oldMem addr' value' >>| Theory.Value.forget in
-        data @@ CT.set memVar newMem 
+        data @@ CT.set memVar newMem
+
+    | Stmt_TCall(FIdent("AtomicStart", 0), _, _, _) ->
+        ctrl @@ invoke_symbol "AtomicStart"
+    | Stmt_TCall(FIdent("AtomicEnd", 0), _, _, _) ->
+        ctrl @@ invoke_symbol "AtomicEnd"
 
     (* TODO: perform some kind of intrinsic call *)
     | Stmt_Assert(_, _) -> nop

plugins/asli/semantics/override.asl

@@ -1,7 +1,12 @@
+AtomicStart()
+  return;
+
+AtomicEnd()
+  return;
+
 bits(64) AArch64.BranchAddr(bits(64) vaddress)
     return vaddress;
 
-
 AArch64.CheckFPAdvSIMDEnabled()
     return;
 
@@ -318,7 +323,7 @@ integer LowestSetBit(bits(N) x)
     elsif (63 < N && x[63] == '1') then
         return 63;
     else
-        return -1;
+        return N;
 
 
 
@@ -352,21 +357,19 @@ AArch64.MemSingle[bits(64) vaddress, integer size, AccType acctype, boolean wasa
 
     _Mem[address, size, access] = value;
 
-
-bits(size) MemAtomicCompareAndSwap(bits(64) address, bits(size) expectedvalue,
-                                   bits(size) newvalue, AccType ldacctype, AccType stacctype)
-    bits(size) oldvalue = Mem[address, size DIV 8, ldacctype];
-
-    if oldvalue == expectedvalue then
-        Mem[address, size DIV 8, stacctype] = newvalue;
-    return oldvalue;
-
 bits(size) MemAtomic(bits(64) address, MemAtomicOp op, bits(size) value, AccType ldacctype, AccType stacctype)
     bits(size) newvalue;
+    //memaddrdesc = AArch64.TranslateAddressForAtomicAccess(address, size);
+    //ldaccdesc = CreateAccessDescriptor(ldacctype);
+    //staccdesc = CreateAccessDescriptor(stacctype);
+
+    AtomicStart();
 
     // All observers in the shareability domain observe the
     // following load and store atomically.
     oldvalue = Mem[address, size DIV 8, ldacctype];
+    if BigEndian() then
+        oldvalue = BigEndianReverse(oldvalue);
 
     case op of
         when MemAtomicOp_ADD   newvalue = oldvalue + value;
@@ -379,13 +382,25 @@ bits(size) MemAtomic(bits(64) address, MemAtomicOp op, bits(size) value, AccType
         when MemAtomicOp_UMIN  newvalue = if UInt(oldvalue) > UInt(value) then value else oldvalue;
         when MemAtomicOp_SWP   newvalue = value;
 
+    if BigEndian() then
+        newvalue = BigEndianReverse(newvalue);
     Mem[address, size DIV 8, stacctype] = newvalue;
 
+    AtomicEnd();
+
     // Load operations return the old (pre-operation) value
     return oldvalue;
 
-boolean AArch64.ExclusiveMonitorsPass(bits(64) address, integer size)
-    return TRUE;
+bits(size) MemAtomicCompareAndSwap(bits(64) address, bits(size) expectedvalue,
+                                   bits(size) newvalue, AccType ldacctype, AccType stacctype)
+    AtomicStart();
+    bits(size) oldvalue = Mem[address, size DIV 8, ldacctype];
+    if BigEndian() then
+        oldvalue = BigEndianReverse(oldvalue);
 
-AArch64.SetExclusiveMonitors(bits(64) address, integer size)
-    return;
+    if oldvalue == expectedvalue then
+        if BigEndian() then
+            newvalue = BigEndianReverse(newvalue);
+        Mem[address, size DIV 8, stacctype] = newvalue;
+    AtomicEnd();
+    return oldvalue;