Series of Minor Fixes

libASL/dis.ml

@@ -67,60 +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;
-  "ASR",0;
-  "SignExtend",0;
-  "ZeroExtend",0;
-] @ (if !Symbolic.use_vectoriser then [
-  "Elem.set",0;
-  "Elem.read",0;
-] else [])
-
-
-
 (** A variable's stack level and original identifier name.
     The "stack level" is how many scopes deep it is.
     For example, globals are level 0 and this increases
@@ -942,15 +888,9 @@ 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))
-  (no_inline_pure ())
-
-and no_inline_ids = List.map (fun (x,y) -> FIdent (x,y))
-  no_inline
-
 (** Disassemble call to function *)
 and dis_funcall (loc: l) (f: ident) (tvs: sym list) (vs: sym list): sym rws =
-    if List.mem f (no_inline_pure_ids ()) &&
+    if List.mem f (Symbolic.prims_pure ()) &&
       ((List.exists (function Exp _ -> true | _ -> false) tvs) ||
         (List.exists (function Exp _ -> true | _ -> false) vs)) then
       let expr = Exp (Expr_TApply (f, List.map sym_expr tvs, List.map sym_expr vs)) in
@@ -979,7 +919,7 @@ and dis_call (loc: l) (f: ident) (tes: sym list) (es: sym list): sym option rws
 and dis_call' (loc: l) (f: ident) (tes: sym list) (es: sym list): sym option rws =
     let@ fn = DisEnv.getFun loc f in
     (match fn with
-    | Some (rty, _, targs, _, _, _) when List.mem f no_inline_ids ->
+    | Some (rty, _, targs, _, _, _) when List.mem f (Symbolic.prims_impure ()) ->
         (* impure functions are not visited. *)
         (match sym_prim_simplify (name_of_FIdent f) tes es with
         | Some x -> DisEnv.pure (Some x)

libASL/dis_tc.ml

@@ -54,7 +54,6 @@ let prim_type fi targs =
   | ("mul_int",           [      ])     -> Some (Value.type_integer )
   | ("zdiv_int",          [      ])     -> Some (Value.type_integer )
   | ("zrem_int",          [      ])     -> Some (Value.type_integer )
-  | ("sdiv_int",          [      ])     -> Some (Value.type_integer )
   | ("fdiv_int",          [      ])     -> Some (Value.type_integer )
   | ("frem_int",          [      ])     -> Some (Value.type_integer )
   | ("mod_pow2_int",      [      ])     -> Some (Value.type_integer )

libASL/offline_opt.ml

@@ -37,7 +37,7 @@ let is_pure_expr f =
   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
+      List.mem (FIdent(f',0)) Offline_transform.pure_prims
   | _ -> false
 
 let is_var_decl f =

libASL/offline_transform.ml

@@ -172,24 +172,14 @@ let join_state (a: state) (b: state): state =
   }
 
 (* Produce a runtime value if any arg is runtime *)
-let pure_prims =
-  Value.prims_pure @
-  (List.map fst (Dis.no_inline_pure ())) @ [
-    "lsr_bits";
-    "sle_bits";
-    "lsl_bits";
-    "asr_bits";
-    "slt_bits";
-    "sdiv_bits";
-  ]
+let pure_prims = Symbolic.prims_pure ()
 
 (* Prims that will always produce runtime *)
-let impure_prims =
-  List.map fst Dis.no_inline
+let impure_prims = Symbolic.prims_impure ()
 
 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
+  if List.mem f pure_prims then Some (join_taint_l (targs @ args))
+  else if List.mem f impure_prims then Some RunTime
   else None
 
 (* Transfer function for a call, pulling a primop def or looking up registered fn signature.

libASL/scala_backend.ml

@@ -60,7 +60,7 @@ module StringSet = Set.Make(String)
         "f_gen_lsr_bits"; "f_gen_mul_bits"; "f_gen_ne_bits"; "f_gen_not_bits";
         "f_gen_not_bool"; "f_gen_or_bits"; "f_gen_or_bool"; "f_gen_sdiv_bits";
         "f_gen_sle_bits"; "f_gen_slt_bits"; "f_gen_sub_bits";
-        "f_gen_AArch64_MemTag_set"; "f_gen_Mem_read"; "f_gen_slice";
+        "f_gen_AArch64_MemTag_read"; "f_gen_AArch64_MemTag_set"; "f_gen_Mem_read"; "f_gen_slice";
         "f_gen_replicate_bits"; "f_gen_append_bits"; "f_gen_array_load";
         "f_gen_array_store"; "f_gen_Mem_set"; "f_gen_assert";
         "f_switch_context"; "f_true_branch"; "f_false_branch"; "f_merge_branch"])

libASL/symbolic.ml

@@ -377,6 +377,13 @@ let rec sym_mul_int (loc: l) (x: sym) (y: sym) =
       sym_add_int loc base offset
   | _ -> Exp (Expr_TApply (FIdent ("mul_int", 0), [], [sym_expr x; sym_expr y]))
 
+let sym_zdiv_int (loc: l) (x: sym) (y: sym) =
+  match x, y with
+  | Val x, Val y -> Val (VInt (prim_zdiv_int (to_integer loc x) (to_integer loc y)))
+  (* x / 1 = x *)
+  | _, Val (VInt i) when i = Z.one -> x
+  | _ -> Exp (Expr_TApply (FIdent ("zdiv_int", 0), [], [sym_expr x; sym_expr y]))
+
 (*** Symbolic Boolean Operations ***)
 
 let sym_not_bool loc (x: sym) =
@@ -643,12 +650,6 @@ let sym_lsl_bits loc w x y =
   | _ ->
       sym_prim (FIdent ("LSL", 0)) [sym_of_int w] [x;y]
 
-let zdiv_int x y =
-  match x, y with
-  | Val (VInt i), Val (VInt j) -> Val (VInt (Z.div i j))
-  | _, Val (VInt i) when i = Z.one -> x
-  | _ -> Exp (Expr_TApply (FIdent ("sdiv_int", 0), [], [sym_expr x; sym_expr y]))
-
 (** Overwrite bits from position lo up to (lo+wd) exclusive of old with the value v.
     Needs to know the widths of both old and v to perform the operation.
     Assumes width of v is equal to wd.
@@ -668,7 +669,7 @@ let sym_insert_bits loc (old_width: int) (old: sym) (lo: sym) (wd: sym) (v: sym)
           (sym_append_bits loc wd lo v (sym_slice loc old 0 lo))
   | (_, _, Val wd', _) when Primops.prim_zrem_int (Z.of_int old_width) (to_integer Unknown wd') = Z.zero && !use_vectoriser ->
       (* Elem.set *)
-      let pos = zdiv_int lo wd in
+      let pos = sym_zdiv_int loc lo wd in
       Exp ( Expr_TApply (FIdent("Elem.set", 0), [expr_of_int old_width ; sym_expr wd],
           List.map sym_expr [old ; pos ; wd ; v]) )
   | (_, Val (VInt l), _, _) when l = Z.zero && !use_vectoriser ->
@@ -920,3 +921,94 @@ let rec expr_access_chain (x: expr) (a: access_chain list): expr =
   | (Index i)::a -> expr_access_chain (Expr_Array(x,val_expr i)) a
   | (SymIndex e)::a -> expr_access_chain (Expr_Array(x,e)) a
   | [] -> x)
+
+(****************************************************************)
+(** {2 Function and Expression Purity}                          *)
+(****************************************************************)
+
+(** Primitives that can be evaluated, reordered, duplicated and eliminated.
+    Semantically, should have no influence on the evaluation trace. *)
+let prims_pure () =
+  (List.map (fun f -> FIdent(f,0)) Value.prims_pure) @
+  [
+    FIdent("LSL",0);
+    FIdent("LSR",0);
+    FIdent("ASR",0);
+    FIdent("SignExtend",0);
+    FIdent("ZeroExtend",0);
+    FIdent("asr_bits",0);
+    FIdent("lsr_bits",0);
+    FIdent("lsl_bits",0);
+    FIdent("slt_bits",0);
+    FIdent("sle_bits",0);
+    FIdent("sdiv_bits",0);
+  ] @ (if !use_vectoriser then [
+    FIdent("Elem.set",0);
+    FIdent("Elem.read",0);
+  ] else [])
+
+(** Primitives that are placed into the evaluation trace. They must be
+    preserved in the output, retaining their ordering with respect to each other
+    and any accesses to global state. *)
+let prims_impure () =
+  (List.map (fun f -> FIdent(f,0)) Value.prims_impure) @
+  [
+    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);
+    FIdent("Mem.read",0);
+    FIdent("Mem.set",0);
+    FIdent("AtomicStart",0);
+    FIdent("AtomicEnd",0);
+    FIdent("AArch64.MemTag.read",0);
+    FIdent("AArch64.MemTag.set",0);
+    FIdent("SetTagCheckedInstruction",0);
+    FIdent("SpeculativeStoreBypassBarrierToPA",0);
+    FIdent("SpeculationBarrier",0);
+    FIdent("SpeculativeStoreBypassBarrierToVA",0);
+  ]
+
+(** Test if an expression is only over constants, variables and pure operations. Does not
+    determine whether a variable access can be considered pure. *)
+let rec is_pure e =
+  match e with
+  | Expr_Var _ -> true
+  | Expr_LitBits _ -> true
+  | Expr_LitInt _ -> true
+  | Expr_Slices(e, [Slice_LoWd(lo, wd)]) ->
+      is_pure e && is_pure lo && is_pure wd
+  | Expr_TApply(f, tes, es) ->
+      List.mem f (prims_pure ()) &&
+      List.for_all is_pure tes &&
+      List.for_all is_pure es
+  | Expr_Field(e,_) -> is_pure e
+  | Expr_Array(e,i) -> is_pure e && is_pure i
+  | _ -> false

libASL/symbolic_lifter.ml

@@ -135,9 +135,9 @@ module RemoveUnsupported = struct
       | Stmt_Dep_ImpDef (_, loc)
       | Stmt_See (_, loc)
       | Stmt_Throw (_, loc)
-      | Stmt_DecodeExecute (_, _, loc) -> ChangeTo (assert_false loc)
-
-      | _ -> failwith @@ "Unknown stmt: " ^ (pp_stmt e))
+      | Stmt_DecodeExecute (_, _, loc)
+      | Stmt_Try (_, _, _, _, loc)
+      | Stmt_Repeat (_, _, loc) -> ChangeTo (assert_false loc))
   end
 
   let run unsupported env body =
@@ -152,13 +152,10 @@ 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 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
-  let l4 = IdentSet.of_list (List.map (fun f -> FIdent (f,0)) Value.prims_impure) in
+  let l1 = IdentSet.of_list (Symbolic.prims_impure ()) in
+  let l2 = IdentSet.of_list (Symbolic.prims_pure ()) in
   (* Union with the unsupported function set *)
-  IdentSet.union l1 (IdentSet.union l2 (IdentSet.union l3 (IdentSet.union l4 unsupported_set)))
+  IdentSet.union l1 l2
 
 (* Count individual stmts present after disassembly *)
 let rec stmt_count s =