inline Elem operations when vectoriser disabled (still not working)

UQ-PAC · Jul 17, 2024 · 54576e0 · 54576e0
1 parent 92a2bba
commit 54576e0
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/libASL/dis.ml b/libASL/dis.ml
@@ -110,15 +110,18 @@ let no_inline = [
   "AArch64.MemTag.set",0;
 ]
 
-let no_inline_pure = [
+let no_inline_pure () = [
   "LSL",0;
   "LSR",0;
   "ASR",0;
   "SignExtend",0;
   "ZeroExtend",0;
+] @ (if !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.
@@ -941,15 +944,15 @@ 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_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 (no_inline_pure_ids ()) &&
       ((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

diff --git a/libASL/offline_transform.ml b/libASL/offline_transform.ml
@@ -174,7 +174,7 @@ 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) @ [
+  (List.map fst (Dis.no_inline_pure ())) @ [
     "lsr_bits";
     "sle_bits";
     "lsl_bits";

diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml
@@ -158,7 +158,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 l2 = IdentSet.of_list (List.map (fun (f,i) -> FIdent (f,i)) Dis.no_inline_pure) 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