Skip to content

Commit

Permalink
Reduce partial evaluation state keys to strings
Browse files Browse the repository at this point in the history
  • Loading branch information
@ncough @katrinafyi
ncough authored and katrinafyi committed Jan 16, 2024
1 parent 3fc7aee commit db0ec06
Showing 1 changed file with 53 additions and 40 deletions.
93 changes: 53 additions & 40 deletions libASL/dis.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,13 @@ open Value

open Symbolic

module StringCmp = struct
type t = string
let compare (x: string) (y: string): int = String.compare x y
end
module StringMap = Map.Make(StringCmp)


let debug_level = ref 0
let debug_show_trace = ref false
let no_debug = fun () -> !debug_level = 0
Expand Down Expand Up @@ -101,19 +108,18 @@ let no_inline = [
The "stack level" is how many scopes deep it is.
For example, globals are level 0 and this increases
by 1 for each nested function call. *)
type var = Var of int * ident
let pp_var (Var (i,id)) = Printf.sprintf "Var(%d,%s)" i (pprint_ident id)
type var = Var of int * string
let pp_var (Var (i,id)) = Printf.sprintf "Var(%d,%s)" i (id)
let var_ident (Var (i,id)) =
match i,id with
| 0,Ident s -> Ident s (* special case globals with no suffix. *)
| _,Ident s -> Ident (s ^ "__" ^ string_of_int i)
| _ -> internal_error Unknown "unexpected resolved variable to function identifier"
| 0,s -> Ident s (* special case globals with no suffix. *)
| _,s -> Ident (s ^ "__" ^ string_of_int i)

(** Returns the variable's name without mangling, suitable for
disassembling then resolving again.
WARNING: should only be used when variable is in the inner-most scope. *)
let var_expr_no_suffix_in_local_scope (Var(_,id)) = Expr_Var id
let var_expr_no_suffix_in_local_scope (Var(_,id)) = Expr_Var (Ident id)

(** Returns an expression for the variable with a mangled name,
suitable for emitting in a generated statement. *)
Expand Down Expand Up @@ -141,16 +147,22 @@ module LocalEnv = struct
- VUninitialized itself is only used for scalar types.
thus, uninitialized structures must be expanded into structures of uninitialized scalars.
*)
locals : (ty * sym) Bindings.t list;
locals : (ty * sym) StringMap.t list;
returnSymbols : expr option list;
numSymbols : int;
indent : int;
trace : dis_trace;
}

let force i =
match i with Ident s -> s | _ -> unsupported Unknown ""

let pp_value_bindings = Utils.pp_list (pp_bindings pp_value)

let pp_sym_bindings (bss: (ty * sym) Bindings.t list) =
let pp_bindings (pp: 'a -> string) (bs: 'a StringMap.t): string =
String.concat ", " (List.map (fun (k, v) -> k ^"->"^ pp v) (StringMap.bindings bs))

let pp_sym_bindings (bss: (ty * sym) StringMap.t list) =
Utils.pp_list (pp_bindings (fun (_,e) -> pp_sym e)) bss

let init (env: Eval.Env.t) =
Expand All @@ -174,10 +186,10 @@ module LocalEnv = struct
in
let globals = Bindings.mapi
(fun id v -> (get_global_type id, Val v))
globalsAndConsts
in
globalsAndConsts in
let globals = StringMap.of_seq @@ Seq.map ( fun (k,v) -> (force k,v)) @@ Bindings.to_seq globals in
{
locals = [Bindings.empty ; globals];
locals = [StringMap.empty ; globals];
returnSymbols = [];
numSymbols = 0;
indent = 0;
Expand All @@ -192,7 +204,7 @@ module LocalEnv = struct
let pp_locals (env: t): string =
let last = List.length env.locals - 1 in
let withoutGlobals = List.mapi
(fun i x -> if i = last then Bindings.empty else x) env.locals in
(fun i x -> if i = last then StringMap.empty else x) env.locals in
Printf.sprintf "locals = %s" (pp_sym_bindings withoutGlobals)
(* Printf.sprintf "locals = %s" (pp_sym_bindings env.locals) *)

Expand Down Expand Up @@ -225,7 +237,7 @@ module LocalEnv = struct

(** Adds a local scoping level within the current level. *)
let addLevel (env: t): t =
{env with locals = (Bindings.empty)::env.locals}
{env with locals = (StringMap.empty)::env.locals}

(** Pops the innermost scoping level. *)
let popLevel (env: t): t =
Expand All @@ -235,10 +247,11 @@ module LocalEnv = struct

(** Adds a new local variable to the innermost scope. *)
let addLocalVar (loc: l) (k: ident) (v: sym) (t: ty) (env: t): var * t =
if !Eval.trace_write then Printf.printf "TRACE: fresh %s = %s\n" (pprint_ident k) (pp_sym v);
let k = force k in
if !Eval.trace_write then Printf.printf "TRACE: fresh %s = %s\n" (k) (pp_sym v);
let var = Var (List.length env.locals - 1, k) in
match env.locals with
| (bs :: rest) -> var, {env with locals = (Bindings.add k (t,v) bs :: rest)}
| (bs :: rest) -> var, {env with locals = (StringMap.add k (t,v) bs :: rest)}
| [] -> internal_error Unknown "attempt to add local var but no local scopes exist"

let addLocalConst = addLocalVar
Expand All @@ -247,32 +260,33 @@ module LocalEnv = struct
let getVar (loc: l) (x: var) (env: t): (ty * sym) =
let Var (i,id) = x in
let n = List.length env.locals - i - 1 in
match Bindings.find_opt id (List.nth env.locals n) with
match StringMap.find_opt id (List.nth env.locals n) with
| Some x -> x
| None -> internal_error loc @@ "failed to get resolved variable: " ^ pp_var x

(** Resolves then gets the type and value of a resolved variable. *)
let rec go loc x env i (bs: (ty * sym) Bindings.t list) =
let rec go loc x env i (bs: (ty * sym) StringMap.t list) =
(match bs with
| [] -> internal_error loc @@ "cannot resolve undeclared variable: " ^ pprint_ident x ^ "\n\n" ^ pp_locals env
| b::rest -> match Bindings.find_opt x b with
| [] -> internal_error loc @@ "cannot resolve undeclared variable: " ^ x ^ "\n\n" ^ pp_locals env
| b::rest -> match StringMap.find_opt x b with
| Some v -> (Var (i,x),v)
| _ -> go loc x env (i - 1) rest)
let resolveGetVar (loc: l) (x: ident) = fun env ->
let x = force x in
let l = List.length env.locals - 1 in
match env.locals with
| b::rest -> (match Bindings.find_opt x b with
| b::rest -> (match StringMap.find_opt x b with
| Some v -> (Var (l,x),v)
| _ -> go loc x env (l - 1) rest)
| _ -> internal_error loc @@ "cannot resolve undeclared variable: " ^ pprint_ident x ^ "\n\n" ^ pp_locals env
| _ -> internal_error loc @@ "cannot resolve undeclared variable: " ^ x ^ "\n\n" ^ pp_locals env

(** Sets a resolved variable to the given value. *)
let setVar (loc: l) (x: var) (v: sym) (env: t): t =
if !Eval.trace_write then Printf.printf "TRACE: write %s = %s\n" (pp_var x) (pp_sym v);
let Var (i,id) = x in
let n = List.length env.locals - i - 1 in
let locals = Utils.nth_modify (
Bindings.update id (fun e -> match e with
StringMap.update id (fun e -> match e with
| Some (t,_) -> Some (t,v)
| None -> internal_error loc @@ "failed to set resolved variable: " ^ pp_var x)) n env.locals in
{ env with locals }
Expand Down Expand Up @@ -325,13 +339,13 @@ module DisEnv = struct
let mkUninit (t: ty): value rws =
reads (uninit t)

let merge_bindings env l r: (ty * sym) Bindings.t =
let merge_bindings env l r: (ty * sym) StringMap.t =
if l == r then l else
Bindings.union (fun k (t1,v1) (t2,v2) ->
StringMap.union (fun k (t1,v1) (t2,v2) ->
if !debug_level > 0 && t2 <> t1 then
unsupported Unknown @@
Printf.sprintf "cannot merge locals with different types: %s, %s <> %s."
(pprint_ident k) (pp_type t1) (pp_type t2);
(k) (pp_type t1) (pp_type t2);
let out = Some (t1,match v1 = v2 with
| false -> Val (uninit t1 env)
| true -> v1) in
Expand Down Expand Up @@ -639,7 +653,7 @@ and type_of_load (loc: l) (x: expr): ty rws =

and type_access_chain (loc: l) (var: var) (ref: access_chain list): ty rws =
let Var (_,id) = var in
type_of_load loc (expr_access_chain (Expr_Var id) ref)
type_of_load loc (expr_access_chain (Expr_Var (Ident id)) ref)

(** Disassemble type *)
and dis_type (loc: l) (t: ty): ty rws =
Expand Down Expand Up @@ -1038,7 +1052,7 @@ and dis_lexpr_chain (loc: l) (x: lexpr) (ref: access_chain list) (r: sym): unit
fun fact - the only instructions i'm aware of that can actually do this don't
work anyway *)
let () = (match var, ref with
| Var(0, Ident("PSTATE")), ([Field(Ident("EL" | "SP" | "nRW"))]) ->
| Var(0, ("PSTATE")), ([Field(Ident("EL" | "SP" | "nRW"))]) ->
unsupported loc @@ "Update to PSTATE EL/SP/nRW while disassembling" ^ pp_lexpr x;
| _, _ ->
()
Expand All @@ -1047,11 +1061,11 @@ and dis_lexpr_chain (loc: l) (x: lexpr) (ref: access_chain list) (r: sym): unit
DisEnv.modify (LocalEnv.setVar loc var (Val vv'))
| [] ->
(match var with
| Var(0, Ident("InGuardedPage")) ->
| Var(0, ("InGuardedPage")) ->
unsupported loc @@ "Update to InGuardedPage while disassembling" ^ pp_lexpr x;
| Var(0, Ident("SCR_EL3")) ->
| Var(0, ("SCR_EL3")) ->
unsupported loc @@ "Update to SCR_EL3 while disassembling" ^ pp_lexpr x;
| Var(0, Ident("SCTLR_EL1")) ->
| Var(0, ("SCTLR_EL1")) ->
unsupported loc @@ "Update to SCTLR_EL1 while disassembling" ^ pp_lexpr x;

| _ -> ());
Expand All @@ -1067,8 +1081,8 @@ and dis_lexpr_chain (loc: l) (x: lexpr) (ref: access_chain list) (r: sym): unit
| _::_ ->
(* variable contains a symbolic expression. read, modify, then write. *)
let@ Var(_,tmp) = capture_expr_mutable loc t e in
let@ () = dis_lexpr_chain loc (LExpr_Var tmp) ref r in
let@ e' = dis_expr loc (Expr_Var tmp) in
let@ () = dis_lexpr_chain loc (LExpr_Var (Ident tmp)) ref r in
let@ e' = dis_expr loc (Expr_Var (Ident tmp)) in
assign_var loc var e'
| [] ->
assign_var loc var r
Expand Down Expand Up @@ -1455,7 +1469,7 @@ let build_env (env: Eval.Env.t): env =
let loc = Unknown in

(* get the pstate, then construct a new pstate where nRW=0, EL=0 & SP=0, then set the pstate *)
let (_, pstate) = LocalEnv.getVar loc (Var(0, Ident("PSTATE"))) lenv in
let (_, pstate) = LocalEnv.getVar loc (Var(0, ("PSTATE"))) lenv in
let pstate = (match pstate with
| Val(pstate_v) ->
let pstate_v = set_access_chain loc pstate_v [Field(Ident("EL"))] (VBits({n=2; v=Z.zero;})) in
Expand All @@ -1465,12 +1479,11 @@ let build_env (env: Eval.Env.t): env =
| _ ->
unsupported loc @@ "Initial env value of PSTATE is not a Value";
) in
let lenv = LocalEnv.setVar loc (Var(0, Ident("PSTATE"))) (Val(pstate)) lenv in
let lenv = LocalEnv.setVar loc (Var(0, Ident("SCR_EL3"))) (Val(VBits({n=64; v=Z.zero;}))) lenv in
let lenv = LocalEnv.setVar loc (Var(0, Ident("SCTLR_EL1"))) (Val(VBits({n=64; v=Z.zero;}))) lenv in

let lenv = LocalEnv.setVar loc (Var(0, ("PSTATE"))) (Val(pstate)) lenv in
let lenv = LocalEnv.setVar loc (Var(0, ("SCR_EL3"))) (Val(VBits({n=64; v=Z.zero;}))) lenv in
let lenv = LocalEnv.setVar loc (Var(0, ("SCTLR_EL1"))) (Val(VBits({n=64; v=Z.zero;}))) lenv in
(* set InGuardedPage to false *)
let lenv = LocalEnv.setVar loc (Var(0, Ident("InGuardedPage"))) (Val (VBool false)) lenv in
let lenv = LocalEnv.setVar loc (Var(0, ("InGuardedPage"))) (Val (VBool false)) lenv in
let globals = IdentSet.of_list @@ List.map fst @@ Bindings.bindings (Eval.Env.readGlobals env) in
lenv, globals

Expand All @@ -1479,8 +1492,8 @@ let build_env (env: Eval.Env.t): env =
Assumes variable is named _PC and its represented as a bitvector. *)
let setPC (env: Eval.Env.t) (lenv,g: env) (address: Z.t): env =
let loc = Unknown in
let pc = Ident "_PC" in
let width = (match Eval.Env.getVar loc env pc with
let pc = "_PC" in
let width = (match Eval.Env.getVar loc env (Ident pc) with
| VUninitialized ty -> width_of_type loc ty
| VBits b -> b.n
| _ -> unsupported loc @@ "Initial env contains PC with unexpected type") in
Expand Down

0 comments on commit db0ec06

Please sign in to comment.