diff --git a/.gitignore b/.gitignore index 780ae51d..82c82b8e 100644 --- a/.gitignore +++ b/.gitignore @@ -24,7 +24,8 @@ scripts/total.txt build/ offlineASL/aarch64_* -offlineASL-scala/lifter/src/generated/* offlineASL-cpp/subprojects/aslp-lifter/src/generated/* offlineASL-cpp/subprojects/aslp-lifter/include/aslp/generated/* + + diff --git a/bin/asli.ml b/bin/asli.ml index 3377e3fe..c0e9d5af 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -27,6 +27,7 @@ let opt_export_aarch64_dir = ref "" let opt_verbose = ref false + let () = Printexc.record_backtrace true ; Printexc.register_printer diff --git a/libASL/cpp_backend.ml b/libASL/cpp_backend.ml index 386e1536..76c7f25b 100644 --- a/libASL/cpp_backend.ml +++ b/libASL/cpp_backend.ml @@ -155,6 +155,7 @@ let rec prints_expr e st = | Expr_LitString s -> "\"" ^ s ^ "\"" | Expr_Tuple(es) -> "std::make_tuple(" ^ (String.concat "," (List.map (fun e -> prints_expr e st) es)) ^ ")" | Expr_Unknown(ty) -> default_value ty st + | Expr_If(_, c, t, [], e) -> Printf.sprintf "((%s) ? (%s) : (%s))" (prints_expr c st) (prints_expr t st) (prints_expr e st) | _ -> failwith @@ "prints_expr: " ^ pp_expr e diff --git a/libASL/ocaml_backend.ml b/libASL/ocaml_backend.ml index 0e57ff3d..5579ef9e 100644 --- a/libASL/ocaml_backend.ml +++ b/libASL/ocaml_backend.ml @@ -133,6 +133,7 @@ let rec prints_expr e st = | Expr_LitString s -> "\"" ^ s ^ "\"" | Expr_Tuple(es) -> "(" ^ (String.concat "," (List.map (fun e -> prints_expr e st) es)) ^ ")" | Expr_Unknown(ty) -> default_value ty st + | Expr_If (ty, c, t, [], e) -> Printf.sprintf "(if (%s) then (%s) else (%s))" (prints_expr c st) (prints_expr t st) (prints_expr e st) | _ -> failwith @@ "prints_expr: " ^ pp_expr e diff --git a/libASL/offline_opt.ml b/libASL/offline_opt.ml index 87f2af3b..3ef7a2bd 100644 --- a/libASL/offline_opt.ml +++ b/libASL/offline_opt.ml @@ -43,6 +43,8 @@ let is_pure_expr f = let is_var_decl f = f = Offline_transform.rt_decl_bv || f = Offline_transform.rt_decl_bool + + (* module CopyProp = struct type clas = Declared | @@ -180,7 +182,7 @@ module CopyProp = struct self#add_dep impure_ident; let _ = List.map (self#vexpr) es in SkipChildren - | e -> failwith @@ "Unknown runtime expression: " ^ (pp_expr e) + | e -> (Printf.printf "Unknown runtime expression: %s\n" (pp_expr e)); DoChildren end let get_deps e = @@ -305,6 +307,7 @@ module CopyProp = struct Asl_visitor.visit_stmts v body end +*) module DeadContextSwitch = struct (* Backwards walk to reduce consecutive context switches. @@ -325,3 +328,570 @@ module DeadContextSwitch = struct let run fn body = let (s,_) = walk_stmts body false in s end + + +module RtCopyProp = struct + + type clas = + Declared | + Defined of IdentSet.t | + Clobbered of IdentSet.t | + Essential + + let pp_clas c = + match c with + | Declared -> "Declared" + | Defined ids -> "Defined (" ^ pp_identset ids ^ ")" + | Clobbered ids -> "Clobbered (" ^ pp_identset ids ^ ")" + | Essential -> "Essential" + + let merge_clas a b = + match a, b with + | Declared, Declared -> Declared + + (* Ignore declared? *) + | Declared, Defined d + | Defined d, Declared -> Defined d + | Declared, Clobbered c + | Clobbered c , Declared -> Clobbered c + + (* Can't drop essential though - needs to hold once set *) + | Declared, Essential + | Essential, Declared -> Essential + + (* Union deps, consider essential even if only conditional *) + | Defined d, Defined d' -> Defined (IdentSet.union d d') + | Defined d, Clobbered d' + | Clobbered d, Clobbered d' + | Clobbered d, Defined d' -> Clobbered (IdentSet.union d d') + | Defined _, Essential + | Essential, Defined _ -> Essential + + (* *) + | Clobbered _, Essential + | Essential, Clobbered _ + | Essential, Essential -> Essential + + + + type state = { + var_clas : clas Bindings.t; + ctx : (ident * MLBDD.t) list; + (* maps idents to the condution under which they are clobbered *) + cond_clobbered: (MLBDD.t) Bindings.t; (* ident -> clobber condition (any dep updated) *) + (* maps idents to the condition under which they are read after clobbering *) + cond_read: (MLBDD.t) Bindings.t; (* ident -> clobber condition (any dep updated) *) + + (*deps: IdentSet.t Bindings.t; (* ident -> ident *) *) + + (* not used; stores dep sets for bindings (and the def reachability) *) + cond_dep: (MLBDD.t * IdentSet.t) Bindings.t; (* binding -> condition * deps *) + (**) + bdd: Transforms.BDDSimp.state; + } + + type rt = state + type olt = MLBDD.t + + + let pp_state st = + (pp_bindings pp_clas st.var_clas) ^ "\n" ^ + "cond read: " ^ + (pp_bindings (fun i -> Printf.sprintf "%s\n" (Transforms.BDDSimp.pp_abs (Val [i]))) st.cond_read) ^ + "\ncond clob: " ^ + (pp_bindings (fun i -> Printf.sprintf "%s\n" (Transforms.BDDSimp.pp_abs (Val [i]))) st.cond_clobbered) + + let pp_essential st = + pp_bindings pp_clas (Bindings.filter (fun f v -> v = Essential) st.var_clas) + + let set_var v k st = + let var_clas = Bindings.add v k st.var_clas in + (* TODO: need to be adapted for new lattice ? *) + { st with var_clas } + + + let cond_merge al bl = Bindings.merge (fun i a b -> match a,b with + | Some a, Some b -> Some (MLBDD.dor a b) + | Some a, _ -> Some a + | _ , Some b -> Some b + | _ -> None) al bl + + let add_cond i c bs = Bindings.add i (match (Bindings.find_opt i bs) with + | Some x -> (MLBDD.dor c x) + | None -> c + ) bs + + let add_conds is c bs = cond_merge bs (Seq.map (fun i -> i, c) is |> Bindings.of_seq) + + + (* only update deps *) + let clobber_var v st = + let var_clas = Bindings.map (fun c -> match c with Defined ids | Clobbered ids when IdentSet.mem v ids -> Clobbered ids | _ -> c) st.var_clas in + (*let st = {st with cond_clobbered = (add_cond v (st.bdd.ctx) st.cond_clobbered)} in *) + let st = Seq.fold_left (fun st (i,c) -> + match c with + | Defined ids + | Clobbered ids when IdentSet.mem v ids + -> {st with cond_clobbered = (add_cond i (st.bdd.ctx) st.cond_clobbered)} + | _ -> st + ) st (Bindings.to_seq var_clas) in + { st with var_clas } + + let update_clobbers st = + (* update everything based on the conditions of their dependencies *) + let ids = Bindings.to_seq st.cond_clobbered in + Seq.fold_left (fun st (iv,cond) -> + let var_clas = Bindings.map (fun c -> match c with Defined ids | Clobbered ids when IdentSet.mem iv ids -> Clobbered ids | _ -> c) st.var_clas in + let st = Seq.fold_left (fun st (ii,c) -> match c with + | Defined ids + | Clobbered ids when IdentSet.mem ii ids -> {st with cond_clobbered = (add_cond ii cond st.cond_clobbered)} + | _ -> st + ) st (Bindings.to_seq var_clas) in + { st with var_clas } + ) st ids + + + + let get_var v st = Bindings.find_opt v st.var_clas + + let merge_st (ts:MLBDD.t) (fs:MLBDD.t) (joined: Transforms.BDDSimp.state) xa xb = + let merge_cond a b = (MLBDD.dor (MLBDD.dand ts a) (MLBDD.dand fs b)) in + let merged_bdd = Bindings.merge (fun (k:ident) a b -> match a,b with + | Some a, Some b -> Some (merge_cond a b) + | Some a, None -> Some (MLBDD.dand ts a) + | None, Some a -> Some (MLBDD.dand fs a) + | None, None -> None) in + let cond_clobbered = merged_bdd xa.cond_clobbered xb.cond_clobbered in + let cond_read = merged_bdd xa.cond_read xb.cond_read in + let cond_dep = Bindings.merge (fun k a b -> match a,b with + | Some (isa, a), Some (isb, b) -> Option.map (fun x -> x, IdentSet.union a b) (Some (merge_cond isa isb)) + | Some (isa, a), None -> Some (MLBDD.dand ts isa, a) + | None, Some (isa, a) -> Some (MLBDD.dand fs isa, a) + | _ -> None + ) xa.cond_dep xb.cond_dep in + let var_clas = Bindings.merge (fun k a b -> + match a, b with + | Some a, Some b -> Some (merge_clas a b) + | Some a, None + | None, Some a -> Some a + | None, None -> None) xa.var_clas xb.var_clas in + let st : state = {xa with bdd=joined; var_clas ; cond_clobbered=cond_clobbered; cond_read=cond_read; cond_dep=cond_dep } in + st + + + let init_state reachable = {bdd=Transforms.BDDSimp.init_state reachable; + var_clas = Bindings.empty; ctx = []; + cond_clobbered = Bindings.empty ; + cond_read = Bindings.empty ; + cond_dep = Bindings.empty} + + let push_context m st = { st with ctx = m::st.ctx } + let peek_context st = match st.ctx with x::xs -> x | _ -> invalid_arg "peek_context" + let pop_context st = let (i,c),tl = (match st.ctx with x::xs -> x,xs | _ -> invalid_arg "pop_context") in + { st with ctx = tl ; bdd = {st.bdd with ctx = c} } + + let has_context st = List.length st.ctx > 0 + + let decl_var v st = set_var v Declared st + let define_var v deps st = + let r = set_var v (Defined deps) st in + let cond_dep = Bindings.find_opt v st.cond_dep |> + Option.map (fun (c,b) -> MLBDD.dor c (st.bdd.ctx), IdentSet.union b deps) |> + function + | Some c -> Bindings.add v c st.cond_dep + | None -> st.cond_dep + in + {r with cond_dep } + + type xform = + | Prop + | PropCond of MLBDD.t (* encoding whether prop is allowed *) + | No + + let read_var v (st,i) = + let st = {st with cond_read = (add_cond v (st.bdd.ctx) st.cond_read )} in + match get_var v st with + (* Reading undeclared generally means a value that is gradually constructed through partial updates *) + | Some (Declared) -> (set_var v Essential st, i) + (* Reading clobbered implies we cannot reorder *) + | Some (Clobbered deps) -> (st, IdentSet.union i deps) + (*if (Transforms.BDDSimp.is_true clobbered st.bdd) then (set_var v Essential st, i) else st, i) *) + (* Collect ids for transitive walk given a defined variable *) + | Some (Defined ids) -> (st, IdentSet.union i ids) + | _ -> (st, i) + + let write_var v (st,i) = + let st = if has_context st then (set_var v Essential st) else st in + (* cannot copy-prop exprs dependent on a run-time branch*) + let st = clobber_var v st in + let (st,i) = match get_var v st with + | Some (Declared) -> (set_var v (Defined i) st, i) + | Some (Defined ids) -> ((set_var v (Clobbered i) st), i) + | Some (Clobbered deps) -> (st, i) + | Some Essential -> (st, i) + | None -> (st, i) + in (st,i) + + + let impure_ident = Ident "CopyProp_impure" + + let read_vars (vs: IdentSet.t) (st: state): state = + let read_set s st = IdentSet.fold read_var s (st,IdentSet.empty) in + (* If impure is in the readset, the reads are not pure. Clobber any impure dependencies now. *) + let st = if IdentSet.mem impure_ident vs then clobber_var impure_ident st else st in + (* Reading variables after they are clobbered shifts them to essential vars *) + let rec iter delta seen st = + let (st,deps) = read_set delta st in + let seen = IdentSet.union seen delta in + let delta = IdentSet.diff deps seen in + if IdentSet.cardinal delta = 0 then st + else iter delta seen st in + iter vs IdentSet.empty st + + (* TODO: Updating, check if this has some context dependence *) + let update_deps v deps st = + if has_context st then (set_var v Essential st) (* cannot copy-prop exprs dependent on a run-time branch*) + else + match get_var v st with + | Some (Declared) -> + set_var v (Defined deps) st + | Some (Defined d') -> + set_var v (Defined (IdentSet.union deps d')) st + | Some (Clobbered d') -> + set_var v (Clobbered (IdentSet.union deps d')) st + | _ -> st + + class deps_walker = object (self) + inherit Asl_visitor.nopAslVisitor + val mutable deps = IdentSet.empty + + method add_dep i = deps <- IdentSet.add i deps + method get_deps = deps + + method! vexpr = function + | Expr_TApply (f, _, _) when is_lit f -> + SkipChildren + | Expr_TApply (f, [], [Expr_Var v]) when is_var_load f -> + self#add_dep v; + SkipChildren + | Expr_TApply (f, [], [e;_;_]) when is_slice f -> + let _ = self#vexpr e in + SkipChildren + | Expr_TApply (f, tes, es) when is_pure_expr f -> + let _ = List.map (self#vexpr) es in + SkipChildren + | Expr_TApply (f, [], [Expr_Var a;i]) when is_array_load f -> + self#add_dep a; + SkipChildren + | Expr_TApply(f, _, es) when is_gen_call f -> + self#add_dep impure_ident; + let _ = List.map (self#vexpr) es in + SkipChildren + | e -> (Printf.printf "Unknown runtime expression: %s\n" (pp_expr e)); DoChildren + end + + let get_deps e = + let v = new deps_walker in + let _ = Asl_visitor.visit_expr v e in + v#get_deps + + + + + let rec walk_stmt s st = + match s with + (* Var decl *) + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> + decl_var v st + + (* Var assign *) + | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> + (* Collect reads and process them all *) + let deps = get_deps e in + let st = read_vars deps st in + (* Clobber anything dependent on v *) + let st,deps = write_var v (st,deps) in + (* Update deps for v *) + st + (*update_deps v deps st*) + + (* Array assign *) + | Stmt_TCall(f, [], [Expr_Var a; i; e], loc) when is_array_store f -> + (* Collect reads and process them all *) + let deps = get_deps e in + let st = read_vars deps st in + (* Clobber anything dependent on a *) + let st,deps = write_var a (st,deps) in + st + + (* Assert *) + | Stmt_TCall(f, [], [e], loc) when is_assert f -> + (* Collect reads and process them all *) + let deps = get_deps e in + read_vars deps st + + (* LiftTime branch *) + | Stmt_If(c, t, [], f, loc) -> + (* merge in the bdds as well *) + let deps = get_deps c in + read_vars deps st + (* branches handled by caller splitting, walking children, and joining *) + + (* + let cond = Transforms.BDDSimp.eval_expr c st.bdd in + let c = Transforms.BDDSimp.rebuild_expr c cond st.bdd in + let ncond = Transforms.BDDSimp.not_bool cond in + let tst:state = walk_stmts t {st with bdd = (Transforms.BDDSimp.restrict_ctx cond {st.bdd with stmts = []})} in + let fst:state = walk_stmts f {st with bdd = (Transforms.BDDSimp.restrict_ctx ncond {st.bdd with stmts = []})} in + + let condbdd = match cond with + | Val [t] -> t + | _ -> failwith (Printf.sprintf "unable to eval cond branch %s %s %s" (Transforms.BDDSimp.pp_abs cond) (Transforms.BDDSimp.pp_state st.bdd) (pp_expr c) ) + in + + let st': state = merge_st cond tst fst in + let st'= {st' with bdd = Transforms.BDDSimp.writeall st.bdd.stmts st'.bdd} in + let st' = {st' with bdd = Transforms.BDDSimp.write (Stmt_If (c, tst.bdd.stmts, [], fst.bdd.stmts, loc)) st'.bdd} in + *) + + + (* RunTime branch *) + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], [c]), loc) when is_branch f -> + (* Collect reads and process them all *) + let deps = get_deps c in + let st = read_vars deps st in + (* Push the merge point *) + push_context (v, st.bdd.ctx) st + + (* Context switch *) + | Stmt_TCall(f, [], [Expr_TApply(f2, [], [Expr_Var i])], loc) when is_context_switch f && is_merge_target f2 -> + let top = fst (peek_context st) in + if i = top then ((pop_context st)) else st + + (* Impure effect *) + | Stmt_TCall(f, _, es, loc) when is_gen_call f -> + (* Collect reads and process them all *) + let st = List.fold_right (fun e st -> + let deps = get_deps e in + read_vars deps st) es st in + (* Clobber everything linked to global state *) + clobber_var impure_ident st + + | v -> st + + and walk_stmts s st : state = + List.fold_left (fun st s -> walk_stmt s st) st s + + + (* To change this, you'd need to know : + - The condition under which its safe to copy prop + - The current reachability + + If you can't establish you are guarded, implies you need to introduce a branch. + The branch will have the outcomes of both exp reduction and maintaining the current temp. + Then need to specialise everything downstream for this point based on this introduced branch. + + This means you need to pull the condition out to the front. + Which means its needs to be fully reduced and in terms of enc. + BDD approach gives us this flexibility, every single condition in the program in terms of original enc. + Relatively simple to reduce from that point: eliminate guards based on reachability, etc. + + You can implement constant-prop and dead code in a similar fashion, as long as your notions of conditional + use / redefinition / loss of constant precision is purely in terms of the original enc. + +statement s is the only definition of x reaching u
on every path from s to u there are no assignments to y
 + + *) + + + (* + variable is not clobbered then read + *) + let cond_candidate v st rtst = + match get_var v st with + | Some Essential -> No + | Some Clobbered deps -> + let c = Bindings.find_opt v st.cond_read in + let b = Bindings.find_opt v st.cond_clobbered in + (match c,b with + | Some read,Some clob -> + let cond = (MLBDD.dand read (MLBDD.dnot clob)) in + (if (Transforms.BDDSimp.is_true (Val [cond]) rtst) then + ( + (*Printf.printf "Condcopyprop prop var %s read => clobbered %s simplifies to FALSE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [MLBDD.dand read (MLBDD.dnot clob)])) ; *) + Prop + ) + else + if (Transforms.BDDSimp.is_false (Val [cond]) rtst) then + ( + (* we don't need to generate a condition at read if we know statically *) + (*Printf.printf "Condcopyprop noprop var %s read => clobbered %s simplifies to TRUE\n" (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [cond])); *) + No) + else PropCond (cond)) + | Some _, None -> Printf.printf "UNCONCD PROP\n" ; Prop + | _,_ -> (*Printf.printf "Condcopyprop: Clobbered variable missing cond read %s\n" (pprint_ident v); *) + No) (* TODO: clobbered but not subsequently read? *) + | Some Defined _ -> (*Printf.printf "Condcopyprop ONLY DEFINED %s\n" (pprint_ident v);*) Prop + | Some Declared -> No + | None -> No + + + + let cp_idents = function + | Ident c -> Ident (c) , Ident (c ^ "_copyprop") + | _ -> failwith "only copyprop vars" + + type cand = { + typ: ty + } + + + + class cond_copyprop_transform cpst = object(self) + inherit Asl_visitor.nopAslVisitor + val mutable rtst = None + + val mutable candidates : cand Bindings.t = Bindings.empty + + method xf_stmt (x:stmt) (st:Transforms.BDDSimp.state) : stmt list = + rtst <- Some st; Asl_visitor.visit_stmt self x + + method candidate v = (Prop = (cond_candidate v cpst (Option.get rtst))) + method essential v = (No = (cond_candidate v cpst (Option.get rtst))) + + method! vstmt s = ChangeDoChildrenPost ([s], fun s -> List.concat_map self#stmt_xform s) + method! vexpr e = ChangeDoChildrenPost (e, fun e -> self#expr_xform e) + + + (* + Decl of candidate -> decl of expr ref + decl of tmp (unless its never clobbered) + Write to candidate -> if !clobbered, write to expr ref, else write to tmp + Read of candidate -> Wrap whole statement in same test, read from appropriate var + *) + + (* + For run-time variables that we have determined we can copyprop, + pull them to lift-time variables so they can be conditionally + copy-propagated at lift time. + *) + method stmt_xform (s : stmt) : stmt list = + let cp_cond c = Option.get (Transforms.BDDSimp.bdd_to_expr (Val [c]) (Option.get rtst)) in + match s with + (* Transform runtime variable decls into expression decls *) + | Stmt_ConstDecl(t, v, Expr_TApply(f, [], args), loc) when is_var_decl f -> + candidates <- Bindings.add v {typ=t} candidates; + (match (cond_candidate v cpst (Option.get rtst)) with + | No -> + Printf.printf "Condcopyprop: NOT PROP at DEFINITION of var %s\n " (pprint_ident v); + [s] + | Prop -> + (* move run-time to lift-time *) + (*Printf.printf "Condcopyprop: UNCOND prop at DEFINITION of var %s\n " (pprint_ident v); *) + [Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [snd (cp_idents v)], Unknown)] + | PropCond cond -> + let ncp,cp = cp_idents v in + (* if (cond) lift-time else run-time *) + Printf.printf "Condcopyprop: CONDITIONAL prop at DEFINITION %s: %s\n " (pprint_ident v) (Transforms.BDDSimp.pp_abs (Val [cond])); + (*let c = cp_cond cond in *) + (* lift-time conditionally generates the copy-propagated or non-propagated form *) + [ + Stmt_ConstDecl (Offline_transform.rt_expr_ty, ncp, Expr_TApply(f, [], args), Unknown); + Stmt_VarDeclsNoInit (Offline_transform.rt_expr_ty, [cp], Unknown); + ] + ) + (* Transform stores into assigns *) + | Stmt_TCall(f, [], [Expr_Var v; e], loc) when is_var_store f -> + (match (cond_candidate v cpst (Option.get rtst)) with + | No -> (*(Printf.printf "Condcopyprop: UNCOND DISABLE PROP on STORE of var %s\n " (pprint_ident v));*) [s] + | Prop -> + (Printf.printf "Condcopyprop: UNCOND RT PROP on STORE of var %s\n " (pprint_ident v); + [(Stmt_Assign (LExpr_Var (snd (cp_idents v)), e, loc))]) + | PropCond cond -> let nocp,cp = cp_idents v in + Printf.printf "Condcopyprop: CONDITIONAL rt prop on STORE of var %s\n " (pprint_ident v); + (* + - if copy-prop'ed form is reachable then generate a store statement + - if non-copyprop'ed form is reachable then generate an assignment statement + *) + (* can re-evaluating an expression have side effects? *) + + let gen_store_rt_var = Stmt_TCall(f, [], [Expr_Var nocp; e], loc) in + let assign_lt_var = Stmt_Assign(LExpr_Var cp, e, loc) in + (* TODO: could further narrow cases here using bdd*) + [Stmt_If ( cp_cond cond, [assign_lt_var], [], [gen_store_rt_var], Unknown)] + ) + | Stmt_TCall(f, _, _, _) when is_var_store f -> failwith "unhandled store" + | _ -> [s] + + method expr_xform (e:expr) : expr = match e with + | Expr_TApply(f, [], [Expr_Var v]) when is_var_load f -> + (match (cond_candidate v cpst (Option.get rtst)) with + | No -> e + | Prop -> Expr_Var (snd (cp_idents v)) + | PropCond cpcond -> let ncp,cp = cp_idents v in + let load = Expr_TApply(f, [], [Expr_Var ncp]) in + let prop = Expr_Var cp in + let yescpcond = Option.get (Transforms.BDDSimp.bdd_to_expr (Val [cpcond]) (Option.get rtst)) in + let vt = Bindings.find v candidates in + (* TODO: might be good to check that yes and no are disjoint here *) + let e = Expr_If (vt.typ, yescpcond, prop, [] , load) in + e + ) + + | Expr_TApply(f, [], [Expr_Var v; e]) when is_var_store f -> failwith "store expression"; + | _ -> e + end + + module AnalysisLat = struct + type rt = state + type olt = Transforms.BDDSimp.state + let xfer_stmt (l:olt) (r:rt) (s:stmt) : rt * stmt list = + (*Printf.printf "%s ::\n%s\n" (pp_stmt s) (Transforms.BDDSimp.pp_state l);*) + (walk_stmt s r,[s]) + let join (ts:olt) (fs:olt) (js:olt) (rta: rt) (rtb: rt) = Printf.printf "ts %s fs %s" + (Transforms.BDDSimp.pp_abs (Val [ts.ctx])) + (Transforms.BDDSimp.pp_abs (Val [fs.ctx])) + ; + Printf.printf "\n--------------\n"; + let p s rta = Printf.printf "%s: %s\n" s (pp_state rta) in + p "\nTRUE BRANCH: " rta; p "\nFALSE BRANCH: " rtb ; + + let j = merge_st ts.ctx fs.ctx (js:olt) rta rtb in + p "\nJOIN STATE: " j; + Printf.printf "\n==============\n"; + j + + let init s = init_state s + end + + module TransformLat = struct + (* warning: internally mutable because order should not matter etc, join is no-op *) + type rt = {cpst: cond_copyprop_transform} + type olt = Transforms.BDDSimp.state + let xfer_stmt ol ss s = ss,ss.cpst#xf_stmt s ol + let join t f j a b = if (a != b) then (failwith "not allowed") else a (* only have one instance of the object so should be fine *) + let init st = {cpst = new cond_copyprop_transform st} + end + + module BDDAnalysis = Transforms.BDDSimp.EvalWithXfer(AnalysisLat) + module BDDTransform = Transforms.BDDSimp.EvalWithXfer(TransformLat) + + let do_transform reachable copyprop_st stmts = + (* apply BDD AI a second time to compare reachability with candidates in analysis pass *) + let st = Transforms.BDDSimp.init_state reachable in + let st = Transforms.BDDSimp.set_enc st in + let olt,ort = BDDTransform.eval_stmts (TransformLat.init copyprop_st) stmts st in + olt.stmts + + let run fn reachable body = + flush stdout; + Printf.printf "transforming %s\n" (pprint_ident fn); + let st : AnalysisLat.rt = init_state reachable in + let rtst = Transforms.BDDSimp.init_state reachable in + let rtst = Transforms.BDDSimp.set_enc rtst in + (*let st = walk_stmts body st in *) + let a,b = BDDAnalysis.eval_stmts st body rtst in + (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_essential st); *) + (* Printf.printf "%s : %s\n" (pprint_ident fn) (pp_state st); *) + do_transform reachable b body + +end diff --git a/libASL/rt_funs.ml b/libASL/rt_funs.ml new file mode 100644 index 00000000..5217f13d --- /dev/null +++ b/libASL/rt_funs.ml @@ -0,0 +1,26 @@ + +open Asl_ast + +let rt_var_ty = Type_Constructor (Ident "rt_sym") +let rt_label_ty = Type_Constructor (Ident "rt_label") +let rt_expr_ty = Type_Constructor (Ident "rt_expr") + +let rt_decl_bv = FIdent("decl_bv", 0) (* string -> int -> sym *) +let rt_decl_bool = FIdent("decl_bool", 0) (* string -> sym *) +let rt_gen_bit_lit = FIdent("gen_bit_lit", 0) (* bv -> bv rt *) +let rt_gen_bool_lit = FIdent("gen_bool_lit", 0) (* bool -> bool rt *) +let rt_gen_int_lit = FIdent("gen_int_lit", 0) (* int -> int rt *) +let rt_gen_slice = FIdent("gen_slice", 0) (* bv rt -> int -> int -> bv rt *) + +let rt_gen_branch = FIdent("gen_branch", 0) (* bool rt -> (rt_label, rt_label, rt_label) *) +let rt_true_branch = FIdent("true_branch", 0) +let rt_false_branch = FIdent("false_branch", 0) +let rt_merge_branch = FIdent("merge_branch", 0) + +let rt_switch_context = FIdent("switch_context", 0) (* rt_label -> unit *) +let rt_gen_load = FIdent("gen_load", 0) (* sym -> 'a rt *) +let rt_gen_store = FIdent("gen_store", 0) (* sym -> 'a rt -> unit *) +let rt_gen_assert = FIdent("gen_assert", 0) (* bool rt -> unit *) + +let rt_gen_array_store = FIdent("gen_array_store", 0) (* sym -> int -> 'a rt -> unit *) +let rt_gen_array_load = FIdent("gen_array_load", 0) (* sym -> int -> 'a rt *) diff --git a/libASL/scala_backend.ml b/libASL/scala_backend.ml index 3b00f7f9..981316b2 100644 --- a/libASL/scala_backend.ml +++ b/libASL/scala_backend.ml @@ -327,6 +327,7 @@ let rec prints_expr ?(deref:bool=true) e (st:st) = | Expr_LitString s -> "\"" ^ s ^ "\"" | Expr_Tuple(es) -> "(" ^ (String.concat "," (List.map (fun e -> prints_expr e st) es)) ^ ")" | Expr_Unknown(ty) -> default_value ty st (* Sound? *) + | Expr_If(_, c, t, [], e) -> Printf.sprintf "(if (%s) then (%s) else (%s))" (prints_expr c st) (prints_expr t st) (prints_expr e st) | _ -> failwith @@ "prints_expr: " ^ pp_expr e diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml index dbee16de..e5ddb131 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -374,13 +374,17 @@ let run include_pc iset pat env = let env' = Eval.Env.copy env in Bindings.iter (fun fn fnsig -> Eval.Env.addFun Unknown env' fn fnsig) fns; (* Run dis over the entry set identifiers with this new environment *) + + let debug = false in + let fns = Bindings.filter_map (fun fn fnsig -> - if not (Bindings.mem fn instrs) then None + if (debug && (fn <> (FIdent ("aarch64_branch_unconditional_register", 0)))) || (not (Bindings.mem fn instrs)) then None else Option.map (fnsig_set_body fnsig) (dis_wrapper fn fnsig env')) fns in Printf.printf " Succeeded for %d instructions\n\n" (Bindings.cardinal fns); let decoder = Eval.Env.getDecoder env (Ident iset) in - let fns = Transforms.BDDSimp.transform_all fns decoder in + let decoderst : Transforms.DecoderChecks.st = Transforms.DecoderChecks.do_transform decoder in + let fns = Transforms.BDDSimp.transform_all fns decoderst in let (_,globals) = Dis.build_env env in let fns = Bindings.map (fnsig_upd_body (Transforms.RemoveUnused.remove_unused globals)) fns in @@ -401,8 +405,21 @@ let run include_pc iset pat env = Printf.printf "Stages 7-8: Offline Transform\n"; flush stdout; let offline_fns = Offline_transform.run fns env in - let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.CopyProp.run k)) offline_fns in + (*let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.CopyProp.run k)) offline_fns in *) let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.DeadContextSwitch.run k)) offline_fns in + + let use_rt_copyprop = true in + + let freachable k = + let k = match k with + | FIdent (n, _) -> Ident n + | n -> n in + Bindings.find k decoderst.instrs + in + + let offline_fns = if use_rt_copyprop then (Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.RtCopyProp.run k (freachable k))) offline_fns) else offline_fns in + Transforms.BDDSimp.print_unknown_prims (); + let dsig = fnsig_upd_body (DecoderCleanup.run (unsupported_inst tests offline_fns)) dsig in let dsig = fnsig_upd_body (Transforms.RemoveUnused.remove_unused IdentSet.empty) dsig in Printf.printf "\n"; diff --git a/libASL/transforms.ml b/libASL/transforms.ml index 4089ead6..d003cb88 100644 --- a/libASL/transforms.ml +++ b/libASL/transforms.ml @@ -1814,13 +1814,14 @@ module FixRedefinitions = struct this#add_bind b; DoChildren | Stmt_If (c, t, els, e, loc) -> let c' = visit_expr this c in - this#push_scope () ; + (* Don't push or pop scopes anymore so that variables are also unique across branches *) + (*this#push_scope () ; *) let t' = visit_stmts this t in - this#pop_scope (); this#push_scope () ; + (*this#pop_scope (); this#push_scope () ; *) let els' = mapNoCopy (visit_s_elsif this ) els in - this#pop_scope (); this#push_scope () ; + (*this#pop_scope (); this#push_scope () ; *) let e' = visit_stmts this e in - this#pop_scope (); + (*this#pop_scope (); *) ChangeTo (Stmt_If (c', t', els', e', loc)) | Stmt_For (var, start, dir, stop, body, loc) -> let start' = visit_expr this start in @@ -2083,12 +2084,20 @@ module DecoderChecks = struct (st,prior) ) (st,st.cur_enc) alts in st - let do_transform d = + let do_transform d : st = tf_decoder d init_state end +module type RTAnalysisLattice = sig + type rt (* RT lattice type *) + type olt (* LT lattice type *) + val xfer_stmt : olt -> rt -> stmt -> rt*stmt list + val join: olt -> olt -> olt -> rt -> rt -> rt +end + module BDDSimp = struct + type abs = Top | Val of MLBDD.t list | @@ -2101,6 +2110,17 @@ module BDDSimp = struct stmts: stmt list; } + module type Lattice = RTAnalysisLattice with type olt = state + + module NopAnalysis = struct + type rt = unit + type olt = state + let xfer_stmt o r s = r,[s] + let join o c j r ro = () + let init _ = () + end + + let init_state (ctx : MLBDD.t) = { man = MLBDD.manager ctx; vars = Bindings.empty ; @@ -2144,7 +2164,7 @@ module BDDSimp = struct let get_var v st = match Bindings.find_opt v st.vars with | Some v -> v - | _ -> Top (* logically this should be Bot, but need to init globals *) + | _ -> (Printf.printf "no var %s\n" (pprint_ident v)); Top (* logically this should be Bot, but need to init globals *) let add_var v abs st = { st with vars = Bindings.add v abs st.vars } @@ -2279,10 +2299,116 @@ module BDDSimp = struct let start = List.length v - lo - wd in Val (sublist v start wd) + + let half_add_bit l r = MLBDD.dand l r, MLBDD.xor l r (* carry, sum *) + let full_add_bit l r carry = + let c1,s1 = half_add_bit l r in + let c2,o = half_add_bit s1 carry in + let ocarry = MLBDD.dor c1 c2 in + ocarry,o + + let twos_comp_add (xs : MLBDD.t list) (ys: MLBDD.t list) : MLBDD.t * (MLBDD.t list)= + let xs = List.rev xs in let ys = List.rev ys in + match xs,ys with + | hx::tlx,hy::tly -> + let lscarry,lsb = half_add_bit hx hy in + let bits,carry = List.fold_left2 + (fun (acc,carry) (l:MLBDD.t) (r:MLBDD.t) -> let carry,o = (full_add_bit l r carry) in o::acc , carry) + ([lsb], lscarry) tlx tly + in carry,bits + | _,_ -> failwith "invalid bit strings" + + let signed_add_wrap x y = let _,bits = twos_comp_add x y in bits + + + let addone m xs = let one = MLBDD.dtrue m in + let xs = List.rev xs in + let c,rs = match xs with + | hx::tlx -> + let lscarry,lsb = half_add_bit hx one in + let bits,carry = List.fold_left + (fun (acc,carry) (l:MLBDD.t) -> let carry,o = (half_add_bit l carry) in o::acc, carry) + ([lsb], lscarry) tlx + in carry,bits + | _ -> failwith "no" + in rs + + + let signed_negation m (x:MLBDD.t list) = addone m (List.map MLBDD.dnot x) + + let signed_sub_wrap m x y = let _,bits = twos_comp_add x (signed_negation m y) in bits + +(* + let signed_lt m x y = + + let signed_gt m x y = List.map MLBDD.dnot (signed_lt m x y) + *) + + + + let eq_bvs a b = + let bits = List.map2 MLBDD.eq a b in + match bits with + | x::xs -> List.fold_right MLBDD.dand xs x + | _ -> failwith "bad bits width" + + let sle_bits m x y = + MLBDD.dor + (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y))) + (MLBDD.dnot (MLBDD.xor (List.hd x) (List.hd y)) ) + + (* https://cs.nyu.edu/pipermail/smt-lib/2007/000182.html *) + + let unknown_prims = ref Bindings.empty + let print_unknown_prims (c:unit) = Bindings.to_seq !unknown_prims |> List.of_seq |> List.sort (fun a b -> compare (snd a) (snd b)) + |> List.iter (fun (id,c) -> Printf.printf "%d \t : %s\n" c (pprint_ident id)) + + let eq_bit a b = MLBDD.dnot (MLBDD.xor a b) + + let bvugt m s t : MLBDD.t = let a, b = (List.fold_left2 (fun (gt, bnotsetfirst) a b -> + MLBDD.dor gt (MLBDD.dand (bnotsetfirst) ((MLBDD.dand a (MLBDD.dnot b)))), (* false until a > b*) + MLBDD.dand bnotsetfirst (MLBDD.dnot (MLBDD.dand (MLBDD.dnot gt) (MLBDD.dand b (MLBDD.dnot a)))) (* true until a < b*) + ) + (MLBDD.dfalse m, MLBDD.dtrue m) (s) (t)) + in (MLBDD.dand a b) + + let bvult m x y : MLBDD.t = bvugt m y x + let bvule m x y = MLBDD.dor (bvult m x y) (eq_bvs x y) + let bvuge m x y = MLBDD.dor (bvugt m x y) (eq_bvs x y) + + let bvslt m x y = MLBDD.dor + (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y))) + (MLBDD.dand (eq_bit (List.hd x) (List.hd y)) (bvult m x y)) + + let bvsgt m x y = bvslt m y x + + let bvsle m x y = MLBDD.dor + (MLBDD.dand (List.hd x) (MLBDD.dnot (List.hd y))) + (MLBDD.dand (eq_bit (List.hd x) (List.hd y)) (bvule m x y)) + + let bvsge m x y = bvsle m y x + + let wrap_bv_bool f m x y = match x , y with + | Val x, Val y -> Val [(f m x y)] + | _,_ -> Top + + (* + let signed_gte_bits m x y = [MLBDD.dor (eq_bvs x y) (List.hd (signed_gt m x y))] + *) + + + let twos_comp_sub man (xs : MLBDD.t list) (ys: MLBDD.t list) = () + + let replicate_bits newlen bits = match bits with + | Val bits -> if Int.rem newlen (List.length bits) <> 0 then failwith "indivisible rep length" ; + let repeats = newlen / (List.length bits) in Val (List.concat (List.init repeats (fun i -> bits))) + | _ -> Top + (****************************************************************) (** Expr Walk *) (****************************************************************) + let eval_prim f tes es st = match f, tes, es with | "and_bool", [], [x; y] -> and_bool x y @@ -2298,19 +2424,39 @@ module BDDSimp = struct | "ne_bits", [w], [x; y] -> ne_bits x y | "eor_bits", [w], [x; y] -> eor_bits x y - | "append_bits", [w;w'], [x; y] -> append_bits x y + | "append_bits", [w;w'], [x; y] -> append_bits x y + (*| "replicate_bits", [w;Expr_LitInt nw], [x;times] -> replicate_bits (int_of_string nw) x *) | "ZeroExtend", [w;Expr_LitInt nw], [x; y] -> zero_extend_bits x (int_of_string nw) st | "SignExtend", [w;Expr_LitInt nw], [x; y] -> sign_extend_bits x (int_of_string nw) st - - | "sle_bits", [w], [x; y] -> Top - | "add_bits", [w], [x; y] -> Top - | "lsr_bits", [w;w'], [x; y] -> Top + + | "add_bits", [Expr_LitInt w], [x; y] -> (match x,y with + | Val x, Val y -> let r = (signed_add_wrap x y) in assert (List.length r == (int_of_string w)); Val r + | _,_ -> Top) + | "sub_bits", [w], [x; y] -> (match x,y with + | Val x, Val y -> Val (signed_add_wrap x (signed_negation st.man y)) + | _,_ -> Top) + + | "ule_bits", [w], [x; y] -> wrap_bv_bool bvule st.man x y + | "uge_bits", [w], [x; y] -> wrap_bv_bool bvuge st.man x y + | "sle_bits", [w], [x; y] -> wrap_bv_bool bvsle st.man x y + | "sge_bits", [w], [x; y] -> wrap_bv_bool bvsge st.man x y + | "slt_bits", [w], [x; y] -> wrap_bv_bool bvslt st.man x y + | "sgt_bits", [w], [x; y] -> wrap_bv_bool bvsgt st.man x y + + (* + + | "lsl_bits", [w], [x; y] -> Top + | "lsr_bits", [w], [x; y] -> Top + | "asr_bits", [w], [x; y] -> Top + | "mul_bits", _, [x; y] -> Top + *) | _, _, _ -> - Printf.printf "unknown prim %s\n" f; + unknown_prims := (Bindings.find_opt (Ident f) !unknown_prims) |> (function Some x -> x + 1 | None -> 0) + |> (fun x -> Bindings.add (Ident f) x !unknown_prims) ; Top let rec eval_expr e st = @@ -2328,22 +2474,29 @@ module BDDSimp = struct | Expr_Var id -> get_var id st (* Simply not going to track these *) - | Expr_Field _ -> Top - | Expr_Array _ -> Top + | Expr_Field _ -> Printf.printf "Overapprox field %s\n" (pp_expr e) ; Top + | Expr_Array _ -> Printf.printf "Overapprox array %s\n" (pp_expr e); Top (* Prims *) | Expr_TApply (FIdent (f, 0), tes, es) -> let es = List.map (fun e -> eval_expr e st) es in eval_prim f tes es st - | Expr_Slices(e, [Slice_LoWd(Expr_LitInt lo,Expr_LitInt wd)]) -> + | Expr_Slices(e, [Slice_LoWd(Expr_LitInt lo, Expr_LitInt wd)]) -> let lo = int_of_string lo in let wd = int_of_string wd in let e = eval_expr e st in extract_bits e lo wd - | Expr_Slices(e, [Slice_LoWd(lo,wd)]) -> - Top - - | _ -> failwith @@ "unexpected expr: " ^ (pp_expr e) + | Expr_Slices(e, [Slice_LoWd(lo,wd)]) -> Printf.printf "Overapprox slice\n" ; Top + | Expr_Parens(e) -> eval_expr e st + | Expr_Fields _ -> Printf.printf "unexpected Expr_Fields %s" (pp_expr e); Top + | Expr_In _ -> Printf.printf "unexpected Expr_In %s" (pp_expr e); Top + | Expr_Unop _ -> Printf.printf "unexpected Expr_Unop %s" (pp_expr e); Top + | Expr_Unknown _ -> Printf.printf "unexpected Expr_Unkonwn %s" (pp_expr e); Top + | Expr_ImpDef _ -> Printf.printf "unexpected Expr_ImpDef %s" (pp_expr e); Top + | Expr_LitString _ -> Printf.printf "unexpected Expr_LitString %s" (pp_expr e); Top + | Expr_If _ -> Printf.printf "unexpected Expr_If %s" (pp_expr e); Top + + | _ -> failwith @@ Printf.sprintf "BDDSimp eval_expr: unexpected expr: %s\n" (pp_expr e) (****************************************************************) (** Stmt Walk *) @@ -2365,7 +2518,7 @@ module BDDSimp = struct else true) a - let rebuild_expr e cond st = + let bdd_to_expr cond st = let bd_to_test b = let bv = Value.to_mask Unknown (Value.from_maskLit b) in sym_expr @@ sym_inmask Unknown (Exp (Expr_Var (Ident "enc"))) bv @@ -2373,13 +2526,6 @@ module BDDSimp = struct match cond with | Val [cond] -> let imps = MLBDD.allprime cond in - (* - Does not work; - - let c = ctx_to_mask st.ctx in - let imps = List.map (fun v -> clear_bits v c) imps in - *) - let rebuild = List.fold_right (fun vars -> MLBDD.dor (List.fold_right (fun (b,v) -> @@ -2389,89 +2535,112 @@ module BDDSimp = struct let imps = MLBDD.allprime rebuild in let masks = List.map DecoderChecks.implicant_to_mask imps in (match masks with - | [] -> Printf.printf "Unsat bdd formula\n" ; e - | [b] -> bd_to_test b + | [] -> None + | [b] -> Some (bd_to_test b) | b::bs -> let try2 = MLBDD.dnot cond |> MLBDD.allprime |> List.map DecoderChecks.implicant_to_mask in match try2 with - | [b] -> Expr_TApply (FIdent ("not_bool", 0), [], [bd_to_test b]) + | [b] -> Some (Expr_TApply (FIdent ("not_bool", 0), [], [bd_to_test b])) | _ -> (let r = (let tests = (List.map bd_to_test (b::bs)) in let bool_or x y = Expr_TApply(FIdent("or_bool", 0), [], [x;y]) in List.fold_left bool_or (List.hd tests) (List.tl tests)) in - r) + Some r) ) - | _ -> - Printf.printf "no value %s %s\n" (pp_expr e) (pp_abs cond); - e + | _ -> None + + let rebuild_expr e cond st = match bdd_to_expr cond st with + | Some x -> x + | None -> Printf.printf "Unable to simplify expr" ; e + + + class nopvis = object(self) + method xf_stmt (x:stmt) (st:state) : stmt list = [x] + end + + let nop_transform = new nopvis + + module EvalWithXfer (Xf: Lattice) = struct - let rec eval_stmt s st = + let rec eval_stmt (xs:Xf.rt) (s:stmt) (st:state) = + (* (transfer : xs, s, st -> xs', s' ; eval : st -> s -> st' ; write s' : s' , st' -> st'' ) -> xs' s' st'' *) + let xs,ns = Xf.xfer_stmt st xs s in match s with | Stmt_VarDeclsNoInit(t, [v], loc) -> let st = add_var v Bot st in - write s st + writeall ns st, xs | Stmt_VarDecl(t, v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write s st + writeall ns st, xs | Stmt_ConstDecl(t, v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write s st + writeall ns st,xs | Stmt_Assign(LExpr_Var v, e, loc) -> let abs = eval_expr e st in let st = add_var v abs st in - write s st + writeall ns st,xs (* Eval the assert, attempt to discharge it & strengthen ctx *) | Stmt_Assert(e, loc) -> let abs = eval_expr e st in - if is_false abs st then st + if is_false abs st then st,xs else let e = rebuild_expr e abs st in let st = write (Stmt_Assert(e,loc)) st in - restrict_ctx abs st + restrict_ctx abs st, xs (* State becomes bot - unreachable *) | Stmt_Throw _ -> Printf.printf "%s : %s\n" (pp_stmt s) (pp_state st); - let st = write s st in - halt st + let st = writeall ns st in + halt st,xs (* If we can reduce c to true/false, collapse *) | Stmt_If(c, tstmts, [], fstmts, loc) -> let cond = eval_expr c st in + if is_true cond st then - eval_stmts tstmts st + eval_stmts xs tstmts st else if is_false cond st then - eval_stmts fstmts st + eval_stmts xs fstmts st else let c = rebuild_expr c cond st in let ncond = not_bool cond in - let tst = eval_stmts tstmts (restrict_ctx cond {st with stmts = []}) in - let fst = eval_stmts fstmts (restrict_ctx ncond {st with stmts = []}) in + + let tst,xsa = eval_stmts xs tstmts (restrict_ctx cond {st with stmts = []}) in + let fst,xsb = eval_stmts xs fstmts (restrict_ctx ncond {st with stmts = []}) in let st' = join_state cond tst fst in + let xs = Xf.join tst fst st' xsa xsb in + let st' = writeall st.stmts st' in let st' = write (Stmt_If (c, tst.stmts, [], fst.stmts, loc)) st' in - st' + st',xs (* Can't do anything here *) | Stmt_Assign _ | Stmt_TCall _ -> - write s st + writeall ns st,xs | _ -> failwith "unknown stmt" - and eval_stmts stmts st = - List.fold_left (fun st s -> if MLBDD.is_false st.ctx then st else eval_stmt s st) st stmts + and eval_stmts xs stmts st = + List.fold_left (fun (st,xs) s -> if MLBDD.is_false st.ctx then st,xs else (eval_stmt xs s st)) (st,xs) stmts + + end let set_enc st = let enc = Val (List.rev (List.init 32 (MLBDD.ithvar st.man))) in {st with vars = Bindings.add (Ident "enc") enc st.vars} + module Eval = EvalWithXfer(NopAnalysis) + + let just_eval a b c = fst (Eval.eval_stmts (NopAnalysis.init ()) a b) + let do_transform fn stmts reach = let st = init_state reach in let st = set_enc st in - let st' = eval_stmts stmts st in + let st',xs = Eval.eval_stmts (NopAnalysis.init ()) stmts st in st'.stmts @@ -2509,8 +2678,7 @@ module BDDSimp = struct 1 + (Int.max d1 d2) end - let transform_all instrs decoder = - let st = DecoderChecks.do_transform decoder in + let transform_all instrs (st:DecoderChecks.st)= (* get all prim implicants for each instruction, one list *) let imps = Bindings.fold (fun k e acc -> let imps = MLBDD.allprime e in @@ -2525,7 +2693,9 @@ module BDDSimp = struct Bindings.mapi (fun nm fnsig -> let i = match nm with FIdent(s,_) -> Ident s | s -> s in match Bindings.find_opt i st.instrs with - | Some reach -> fnsig_upd_body (fun b -> do_transform nm b reach) fnsig + | Some reach -> fnsig_upd_body (fun b -> + Printf.printf "transforming %s\n" (pprint_ident nm); + do_transform nm b reach) fnsig | None -> fnsig) instrs end diff --git a/offlineASL-scala/.gitignore b/offlineASL-scala/.gitignore new file mode 100644 index 00000000..cffb8e49 --- /dev/null +++ b/offlineASL-scala/.gitignore @@ -0,0 +1,4 @@ + +lifter/src/generated/* +.metals +out diff --git a/tests/bdd_ops.ml b/tests/bdd_ops.ml new file mode 100644 index 00000000..f59d5ffa --- /dev/null +++ b/tests/bdd_ops.ml @@ -0,0 +1,73 @@ +open LibASL +open Asl_utils +open AST +open LibASL.Primops +open LibASL.Utils + +module TC = Tcheck +module AST = Asl_ast + +let man = MLBDD.init ~cache:1024 () + + +let from_bitsLit x = + let x' = Value.drop_chars x ' ' in + (Primops.mkBits (String.length x') (Z.of_string_base 2 x')) + +let it i = assert (MLBDD.is_true i || MLBDD.is_false i ) ; MLBDD.is_true i + +let bdd_to_bv (b:MLBDD.t list) = let l = List.map (fun i -> + assert (MLBDD.is_true i || MLBDD.is_false i ) ; MLBDD.is_true i) b + in let l = List.map (function + | true -> '1' + | false -> '0') l |> List.to_seq |> String.of_seq in + from_bitsLit l + +let prim_cvt_bits_str (x: bitvector): string = + let n = Z.of_int x.n in + if Z.equal n Z.zero then begin + "''" + end else begin + let s = Z.format "%0b" x.v in + let pad = String.make (Z.to_int n - String.length s) '0' in + pad ^ s + end + + +let bv_to_bdd (bv:bitvector) = + let l = prim_cvt_bits_str bv in + let l = String.to_seq l |> List.of_seq in + List.map (function + | '1' -> MLBDD.dtrue man + | '0' -> MLBDD.dfalse man + | x -> failwith (Printf.sprintf "no %c" x) ) l + +let ppbit = prim_cvt_bits_str + + + +let test_add = + let width = 8 in + let cases = List.init 256 (fun i -> (i - 128)) in + let cases_bits = List.map (fun i -> mkBits width (Z.of_int i)) cases in + let cases_bdd = List.map bv_to_bdd cases_bits in + let compar = List.concat_map (fun i -> List.map (fun j -> i , j) cases_bits) cases_bits in + let to_check = List.concat_map (fun i -> List.map (fun j -> i , j) cases_bdd) cases_bdd in + let res_add = List.map2 (fun (i,j) (i', j') -> (i, j), prim_add_bits i j, bdd_to_bv (LibASL.Transforms.BDDSimp.signed_add_wrap i' j')) compar to_check in + List.iter (fun ((i,j),c,r) -> Alcotest.(check string) (Printf.sprintf "%s + %s = %s" (ppbit i) (ppbit j) (ppbit c)) (prim_cvt_bits_str c) (prim_cvt_bits_str r)) res_add ; + + let res_sub = List.map2 (fun (i,j) (i', j') -> (i, j), prim_sub_bits i j, bdd_to_bv (LibASL.Transforms.BDDSimp.signed_sub_wrap man i' j')) compar to_check in + List.iter (fun ((i,j),c,r) -> Alcotest.(check string) (Printf.sprintf "%s - %s = %s" (ppbit i) (ppbit j) (ppbit c)) (prim_cvt_bits_str c) (prim_cvt_bits_str r)) res_sub ; + + let compare_binop format f1 f2 = + let res = List.map2 (fun (i,j) (i', j') -> (i, j), f1 i j, (f2 i' j')) compar to_check in + List.iter (fun ((i,j),c,r) -> Alcotest.(check bool) (Printf.sprintf format (ppbit i) (ppbit j) (c)) (c) r) res in + compare_binop "%s > %s = %b" (fun x y -> prim_gt_int (Primops.prim_cvt_bits_uint x) (Primops.prim_cvt_bits_uint y)) (fun x y -> it (LibASL.Transforms.BDDSimp.bvugt man x y)) ; + compare_binop "%s < %s = %b" (fun x y -> prim_lt_int (Primops.prim_cvt_bits_sint x) (Primops.prim_cvt_bits_sint y)) (fun x y -> it (LibASL.Transforms.BDDSimp.bvslt man x y)) ; + compare_binop "%s <= %s = %b" (fun x y -> prim_le_int (Primops.prim_cvt_bits_sint x) (Primops.prim_cvt_bits_sint y)) (fun x y -> it (LibASL.Transforms.BDDSimp.bvsle man x y)) ; + + + + + + diff --git a/tests/dune b/tests/dune index 0c1c3027..9ebb56a6 100644 --- a/tests/dune +++ b/tests/dune @@ -1,4 +1,12 @@ (test (name test_asl) (modes exe) (flags (-cclib -lstdc++)) + (modules test_asl) + (libraries alcotest asli.libASL)) + + +(test (name bdd_ops) + (modes exe) + (flags (-cclib -lstdc++)) +(modules bdd_ops) (libraries alcotest asli.libASL))