added prompt.lem for connecting to concurrency model and {power,armv8}_extras.lem; fixes

1 files changed, 35 insertions, 0 deletions

diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
new file mode 100644
index 00000000..f2941aff
--- /dev/null
+++ b/src/gen_lib/power_extras.lem
@@ -0,0 +1,35 @@
+open import Pervasives
+open import State
+open import Sail_values
+
+(*
+let rec countLeadingZeros_helper bits =  
+((match bits with
+    | (Interp.V_lit (L_aux( L_zero, _)))::bits -> 
+      let (Interp.V_lit (L_aux( (L_num n), loc))) = (countLeadingZeros_helper bits) in
+      Interp.V_lit (L_aux( (L_num (Nat_big_num.add n(Nat_big_num.of_int 1))), loc))
+    | _ -> Interp.V_lit (L_aux( (L_num(Nat_big_num.of_int 0)), Interp_ast.Unknown))
+))
+let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
+  | [Interp.V_track( v, r);Interp.V_track( v2, r2)] -> 
+    Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) ( Pset.(union) r r2)
+  | [Interp.V_track( v, r);v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
+  | [v;Interp.V_track( v2, r2)] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
+  | [Interp.V_unknown;_] -> Interp.V_unknown
+  | [_;Interp.V_unknown] -> Interp.V_unknown
+  | [Interp.V_vector( _, _, bits);Interp.V_lit (L_aux( (L_num n), _))] -> 
+    countLeadingZeros_helper (snd (Lem_list.split_at (abs (Nat_big_num.to_int n)) bits))
+))
+ *)
+
+let MEMr (addr,l) = read_memory (unsigned addr) l
+let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
+
+let MEMw (addr,l,value) = write_memory (unsigned addr) l value
+let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return true
+
+let I_Sync () = return ()
+let H_Sync () = return ()
+let LW_Sync () = return ()
+let EIEIO_Sync () = return ()
+