Rework memory prims

- Add Memory.[set,read] to represent primitive memory operations
- Override Mem.[set,read] to include desired atomicity behaviour & call new memory prims
- Begin moving arch specific details into a centralised config

libASL/dis.ml

@@ -67,47 +67,6 @@ let () = Printexc.register_printer
         Some ("LibASL.Value.EvalError(\"" ^ e ^ "\") at " ^ pp_loc loc)
     | _ -> None)
 
-(* Don't inline these functions, as we assume their behaviours conform to some spec *)
-let no_inline = [
-  "FPConvert",0;
-  "FPRoundInt",0;
-  "FPRoundIntN",0;
-  "FPToFixed",0;
-  "FixedToFP",0;
-  "FPCompare",0;
-  "FPCompareEQ",0;
-  "FPCompareGE",0;
-  "FPCompareGT",0;
-  "FPToFixedJS_impl",0;
-  "FPSqrt",0;
-  "FPAdd",0;
-  "FPMul",0;
-  "FPDiv",0;
-  "FPMulAdd",0;
-  "FPMulAddH",0;
-  "FPMulX",0;
-  "FPMax",0;
-  "FPMin",0;
-  "FPMaxNum",0;
-  "FPMinNum",0;
-  "FPSub",0;
-  "FPRecpX",0;
-  "FPRecipStepFused",0;
-  "FPRSqrtStepFused",0;
-  "FPRoundBase",0;
-  "FPConvertBF",0;
-  "BFRound",0;
-  "BFAdd",0;
-  "BFMul",0;
-  "FPRecipEstimate",0;
-  "Mem.read",0;
-  "Mem.set",0;
-  "AtomicStart",0;
-  "AtomicEnd",0;
-  "AArch64.MemTag.read",0;
-  "AArch64.MemTag.set",0;
-]
-
 let no_inline_pure = [
   "LSL",0;
   "LSR",0;
@@ -890,11 +849,10 @@ and dis_expr' (loc: l) (x: AST.expr): sym rws =
     | Expr_LitString(s) -> DisEnv.pure (Val (from_stringLit s))
     )
 
-and no_inline_pure_ids = List.map (fun (x,y) -> FIdent(x,y))
+and no_inline_pure_ids = List.map (fun (x,y) -> FIdent (x,y))
   no_inline_pure
 
-and no_inline_ids = List.map (fun (x,y) -> FIdent (x,y))
-  no_inline
+and no_inline_ids = Dis_config.impure_prims
 
 (** Disassemble call to function *)
 and dis_funcall (loc: l) (f: ident) (tvs: sym list) (vs: sym list): sym rws =
@@ -1189,7 +1147,7 @@ and stmt_append (xs: stmt list) (ys: stmt list): stmt list =
 and duplicate_up_to (stmts: AST.stmt list) : (AST.stmt list * AST.stmt list) =
   match stmts with
   (* Don't duplicate AtomicEnd, as they are linked with an AtomicStart *)
-  | Stmt_TCall(FIdent("AtomicEnd", 0), _, _, _)::rest ->
+  | Stmt_TCall(f, _, _, _)::rest when f = Dis_config.atomic_end_prim ->
       ([], stmts)
   | r::rest -> (match duplicate_up_to rest with (f,s) -> (r::f,s))
   | [] -> ([],[])

libASL/dis_config.ml

@@ -0,0 +1,56 @@
+(* Common config for dis transforms *)
+open Asl_ast
+
+(* Memory prims *)
+let mem_read_prim     = FIdent("Memory.read",0)
+let mem_set_prim      = FIdent("Memory.set",0)
+
+(* Atomic bounds prims *)
+let atomic_start_prim = FIdent("AtomicStart",0)
+let atomic_end_prim   = FIdent("AtomicEnd",0)
+
+(* Other memory prims TODO: Can't these be in the override? *)
+let other_mem_prims = [
+  FIdent("AArch64.MemTag.read",0);
+  FIdent("AArch64.MemTag.set",0);
+]
+
+(* FP prims *)
+let fp_prims = [
+  FIdent("FPConvert",0);
+  FIdent("FPRoundInt",0);
+  FIdent("FPRoundIntN",0);
+  FIdent("FPToFixed",0);
+  FIdent("FixedToFP",0);
+  FIdent("FPCompare",0);
+  FIdent("FPCompareEQ",0);
+  FIdent("FPCompareGE",0);
+  FIdent("FPCompareGT",0);
+  FIdent("FPToFixedJS_impl",0);
+  FIdent("FPSqrt",0);
+  FIdent("FPAdd",0);
+  FIdent("FPMul",0);
+  FIdent("FPDiv",0);
+  FIdent("FPMulAdd",0);
+  FIdent("FPMulAddH",0);
+  FIdent("FPMulX",0);
+  FIdent("FPMax",0);
+  FIdent("FPMin",0);
+  FIdent("FPMaxNum",0);
+  FIdent("FPMinNum",0);
+  FIdent("FPSub",0);
+  FIdent("FPRecpX",0);
+  FIdent("FPRecipStepFused",0);
+  FIdent("FPRSqrtStepFused",0);
+  FIdent("FPRoundBase",0);
+  FIdent("FPConvertBF",0);
+  FIdent("BFRound",0);
+  FIdent("BFAdd",0);
+  FIdent("BFMul",0);
+  FIdent("FPRecipEstimate",0);
+]
+
+let impure_prims =
+  [mem_read_prim; mem_set_prim; atomic_start_prim; atomic_end_prim] @
+  other_mem_prims @
+  fp_prims

libASL/dune

@@ -23,7 +23,7 @@
    lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms utils value visitor res
    symbolic_lifter decoder_program call_graph req_analysis
    offline_transform ocaml_backend dis_tc
-   offline_opt
+   offline_opt dis_config
    )
  (libraries pprint zarith z3 str pcre  dune-site))
 

libASL/offline_opt.ml

@@ -1,9 +1,18 @@
 open Asl_utils
 open Asl_ast
 
+let trim_gen f =
+  let prefix = "gen_" in
+  match f with
+  | FIdent(f, i) when String.starts_with ~prefix f ->
+      Some ( FIdent (String.sub f 4 (String.length f - 4), i) )
+  | _ -> None
+
 (* Utility functions to match runtime expressions *)
 let is_memory_load f =
-  f = FIdent ("gen_Mem.read", 0)
+  match trim_gen f with
+  | Some f -> f = Dis_config.mem_read_prim
+  | _ -> false
 let is_var_load f =
   f = Offline_transform.rt_gen_load
 let is_var_store f =
@@ -24,17 +33,13 @@ let is_slice f =
   f = FIdent ("gen_slice", 0)
 
 let is_gen_call f =
-  let prefix = "gen_" in
-  match f with
-  | FIdent(f, _) when String.starts_with ~prefix f -> true
+  match trim_gen f with
+  | Some _ -> true
   | _ -> false
 
 let is_pure_expr f =
-  let prefix = "gen_" in
-  match f with
-  | FIdent(f, 0) when String.starts_with ~prefix f ->
-      let f' = String.sub f 4 (String.length f - 4) in
-      List.mem f' Offline_transform.pure_prims
+  match trim_gen f with
+  | Some (FIdent (f, 0)) -> List.mem f Offline_transform.pure_prims
   | _ -> false
 
 let is_var_decl f =

libASL/offline_transform.ml

@@ -183,13 +183,9 @@ let pure_prims =
     "sdiv_bits";
   ]
 
-(* Prims that will always produce runtime *)
-let impure_prims =
-  List.map fst Dis.no_inline
-
 let prim_ops (f: ident) (targs: taint list) (args: taint list): taint option =
   if List.mem (name_of_FIdent f) pure_prims then Some (join_taint_l (targs @ args))
-  else if List.mem (name_of_FIdent f) impure_prims then Some RunTime
+  else if List.mem f Dis_config.impure_prims then Some RunTime
   else None
 
 (* Transfer function for a call, pulling a primop def or looking up registered fn signature.
@@ -821,7 +817,7 @@ and gen_expr loc e : (taint * expr) wrm =
           let@ lo = lt_expr loc lo in
           let@ wd = lt_expr loc wd in
           gen_slice_expr e lo wd
-      | Expr_TApply(f,tes,es) -> 
+      | Expr_TApply(f,tes,es) ->
           gen_prim loc f tes es
 
       (* State loads *)

libASL/symbolic_lifter.ml

@@ -161,7 +161,7 @@ let unsupported f = IdentSet.mem f unsupported_set
 
 let get_inlining_frontier =
   (* Collect all functions dis will not inline *)
-  let l1 = IdentSet.of_list (List.map (fun (f,i) -> FIdent (f,i)) Dis.no_inline) in
+  let l1 = IdentSet.of_list (Dis_config.impure_prims) in
   let l2 = IdentSet.of_list (List.map (fun (f,i) -> FIdent (f,i)) Dis.no_inline_pure) in
   (* Collect all prims *)
   let l3 = IdentSet.of_list (List.map (fun f -> FIdent (f,0)) Value.prims_pure) in