diff --git a/libASL/dis.ml b/libASL/dis.ml index 9514ebca..c5c65ecf 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -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 @@ -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. *) @@ -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) = @@ -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; @@ -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) *) @@ -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 = @@ -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 @@ -247,24 +260,25 @@ 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 = @@ -272,7 +286,7 @@ module LocalEnv = struct 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 } @@ -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 @@ -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 = @@ -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; | _, _ -> () @@ -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; | _ -> ()); @@ -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 @@ -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 @@ -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 @@ -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