Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rework Memory Prims #60

Draft
wants to merge 1 commit into
base: partial_eval
Choose a base branch
from
Draft

Rework Memory Prims #60

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 3 additions & 45 deletions libASL/dis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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))
| [] -> ([],[])
Expand Down
56 changes: 56 additions & 0 deletions libASL/dis_config.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion libASL/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))

Expand Down
23 changes: 14 additions & 9 deletions libASL/offline_opt.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 =
Expand All @@ -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 =
Expand Down
8 changes: 2 additions & 6 deletions libASL/offline_transform.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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 *)
Expand Down
2 changes: 1 addition & 1 deletion libASL/symbolic_lifter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading