diff --git a/CodeHawk/CH/xprlib/xprUtil.ml b/CodeHawk/CH/xprlib/xprUtil.ml index aa0bc644..124ceeeb 100644 --- a/CodeHawk/CH/xprlib/xprUtil.ml +++ b/CodeHawk/CH/xprlib/xprUtil.ml @@ -267,6 +267,7 @@ let substitute_expr (subst:substitution_t) (expr:xpr_t) = let rec aux exp = match exp with | XVar v -> subst v + | XOp ((Xf "addressofvar"), _) -> exp | XOp (op,l) -> XOp (op, List.map (fun e -> aux e) l) | XAttr (s, e) -> XAttr (s, aux e) | _ -> exp diff --git a/CodeHawk/CH/xprlib/xprt.ml b/CodeHawk/CH/xprlib/xprt.ml index 0c4c9084..410b7add 100644 --- a/CodeHawk/CH/xprlib/xprt.ml +++ b/CodeHawk/CH/xprlib/xprt.ml @@ -3,10 +3,10 @@ Author: Henny Sipma ------------------------------------------------------------------------------ The MIT License (MIT) - + Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2022 Aarno Labs LLC + Copyright (c) 2021-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -14,10 +14,10 @@ to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: - + The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. - + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE @@ -32,7 +32,7 @@ open CHBounds open CHCommon open CHLanguage open CHNumerical -open CHPretty +open CHPretty open CHSymbolicSets open CHUtils @@ -44,135 +44,165 @@ open XprTypes exception XprFailure of string * pretty_t -let sym_constant s = SymSet [s] -let sym_constant_expr s = XConst (sym_constant s) +let sym_constant (s: symbol_t) = SymSet [s] + +let sym_constant_expr (s: symbol_t) = XConst (sym_constant s) -let sym_set_constant l = SymSet l -let _sym_set_constant_expr l = XConst (sym_set_constant l) +let sym_set_constant (l: symbol_t list) = SymSet l + +let _sym_set_constant_expr (l: symbol_t list) = XConst (sym_set_constant l) let zero_constant = IntConst (numerical_zero) + let zero_constant_expr = XConst (zero_constant) let one_constant = IntConst (mkNumerical 1) + let one_constant_expr = XConst (one_constant) let int_constant i = IntConst (mkNumerical i) + let int_constant_expr i = XConst (int_constant i) + let num_constant_expr n = XConst (IntConst n) let random_constant_expr = XConst XRandom + let unknown_int_constant_expr = XConst XUnknownInt -let _interval_expr i = - match i#singleton with - Some num -> num_constant_expr num +let _interval_expr (i: CHIntervals.interval_t) = + match i#singleton with + | Some num -> num_constant_expr num | _ -> let minb = i#getMin#getBound in let maxb = i#getMax#getBound in match (minb, maxb) with - | (NUMBER minv, NUMBER maxv) -> + | (NUMBER minv, NUMBER maxv) -> XOp (XNumRange, [ num_constant_expr minv ; num_constant_expr maxv ]) | (NUMBER minv, _) -> XOp (XNumRange, [ num_constant_expr minv ; unknown_int_constant_expr]) | (_, NUMBER maxv) -> XOp (XNumRange, [ unknown_int_constant_expr ; num_constant_expr maxv]) - | _ -> + | _ -> random_constant_expr - + let _unknown_set_constant_expr = XConst XUnknownSet - + let true_constant = BoolConst true + let true_constant_expr = XConst true_constant - + let false_constant = BoolConst false + let false_constant_expr = XConst false_constant - -let is_random = function XConst XRandom -> true | _ -> false - -let is_true = function + +let is_random (x: xpr_t) = + match x with | XConst XRandom -> true | _ -> false + +let is_true (x: xpr_t) = + match x with | XConst (BoolConst b) -> b | _ -> false - -let is_false = function + +let is_false (x: xpr_t) = + match x with | XConst (BoolConst b) -> not b | _ -> false - -let _get_bool expr = - match expr with + +let _get_bool (x: xpr_t) = + match x with | XConst (BoolConst b) -> b | _ -> raise (XprFailure ("CExpr.get_bool", LBLOCK [STR "not a boolean constant in get_bool: " ])) -let is_zero = function +let is_zero (x: xpr_t) = + match x with | XConst (IntConst num) -> num#equal numerical_zero | _ -> false -let is_one = function +let is_one (x: xpr_t) = + match x with | XConst (IntConst num) -> num#equal numerical_one | _ -> false -let _is_non_zero_int = function +let _is_non_zero_int (x: xpr_t) = + match x with | XConst (IntConst num) -> not (num#equal numerical_zero) | _ -> false -let is_intconst = function +let is_intconst (x: xpr_t) = + match x with | XConst (IntConst _ ) -> true | _ -> false -let is_conjunction = function - XOp (XLAnd, _) -> true +let is_conjunction (x: xpr_t) = + match x with + | XOp (XLAnd, _) -> true | _ -> false -let is_disjunction = function +let is_disjunction (x: xpr_t) = + match x with | XOp (XLOr, _) -> true | _ -> false -let get_conjuncts = function +let get_conjuncts (x: xpr_t) = + match x with | XOp (XLAnd, c) -> c - | _ -> raise (XprFailure - ("Xprt.get_conjuncts", - LBLOCK [ STR "not a conjunction in get_conjuncts: "])) + | _ -> + raise + (XprFailure + ("Xprt.get_conjuncts", + LBLOCK [STR "not a conjunction in get_conjuncts: "])) -let get_disjuncts = function +let get_disjuncts (x: xpr_t) = + match x with | XOp (XLOr, d) -> d - | _ -> raise (XprFailure - ("Xprt.get_disjuncts", - LBLOCK [ STR "not a disjunction in get_disjuncts: "])) + | _ -> + raise + (XprFailure + ("Xprt.get_disjuncts", + LBLOCK [STR "not a disjunction in get_disjuncts: "])) -let get_const = function +let get_const (x: xpr_t) = + match x with | XConst (IntConst num) -> Some num - | XConst (BoolConst b) -> + | XConst (BoolConst b) -> if b then Some numerical_one else Some numerical_zero | _ -> None -let _get_sym_const = function +let _get_sym_const (x: xpr_t) = + match x with | XConst (SymSet [s]) -> Some s | _ -> None -let _get_sym_set = function +let _get_sym_set (x: xpr_t) = + match x with | XConst (SymSet l) -> Some l | _ -> None -let _make_ch_symbolic_set = function +let _make_ch_symbolic_set (x: xpr_t) = + match x with | XConst (SymSet l) -> new symbolic_set_t l | _ -> topSymbolicSet -let _is_bool_op = function +let _is_bool_op (xop: xop_t) = + match xop with | XLt | XGt | XLe | XGe | XEq - | XNe + | XNe | XSubset | XDisjoint | XLAnd | XLOr -> true | _ -> false -let _is_numeric_bool_op = function +let _is_numeric_bool_op (xop: xop_t) = + match xop with | XLt | XGt | XLe @@ -181,33 +211,38 @@ let _is_numeric_bool_op = function | XEq -> true | _ -> false -let _is_symbolic_bool_op = function +let _is_symbolic_bool_op (xop: xop_t) = + match xop with | XSubset | XDisjoint -> true | _ -> false + type engine_expr_type_t = | NumericType | SymbolicType | BoolType -let _engine_type_of_var v = +let _engine_type_of_var (v: variable_t) = if is_numerical_type v#getType then NumericType else SymbolicType -let _engine_type_of_const = function +let _engine_type_of_const (x: xcst_t) = + match x with | SymSet _ | XUnknownSet -> SymbolicType | XUnknownInt | IntConst _ -> NumericType - | BoolConst _ + | BoolConst _ | XRandom -> BoolType + let vars_in_expr (expr:xpr_t):VariableCollections.set_t = let s = new VariableCollections.set_t in let rec vs e = match e with | XVar v -> s#add v | XConst _ -> () + | XOp ((Xf "addressofvar"), _) -> () | XOp (_, l) -> List.iter vs l | XAttr (_,e) -> vs e in begin @@ -215,16 +250,19 @@ let vars_in_expr (expr:xpr_t):VariableCollections.set_t = s end + let variables_in_expr (x:xpr_t):variable_t list = (vars_in_expr x)#toList + let vars_in_expr_list (exprs:xpr_t list) = let s = new VariableCollections.set_t in - begin + begin List.iter (fun e -> s#addSet (vars_in_expr e)) exprs; s#toList end -let syntactically_equal expr1 expr2 = + +let syntactically_equal (expr1: xpr_t) (expr2: xpr_t) = let c_equal c1 c2 = match (c1,c2) with | (SymSet s1, SymSet s2) -> List.for_all2 (fun x1 x2 -> x1#equal x2) s1 s2 @@ -252,6 +290,7 @@ let op_strings = (XMult, "XMult"); (XDiv, "XDiv"); (XMod, "XMod"); + (XPow, "XPow"); (XShiftlt, "XShiftlt"); (XShiftrt, "XShiftrt"); (XLsr, "XLsr"); @@ -276,27 +315,31 @@ let op_strings = (XXlsb, "XXlsb"); (XXlsh, "XXlsh"); (XXbyte, "XXbyte"); - (Xf "","Xf")] + ((Xf "addressofvar"),"Xf")] -let get_op_string op = +let get_op_string (op: xop_t) = try let (_,s) = List.find (fun (o,_s) -> op = o) op_strings in s with | Not_found -> - raise (CHFailure (LBLOCK [STR "Operator not found in get_op_string"])) + raise + (CHFailure + (LBLOCK [ + STR __FILE__; STR ":"; INT __LINE__; STR ": "; + STR "Operator not found in get_op_string"])) -let compare_op op1 op2 = +let compare_op (op1: xop_t) (op2: xop_t) = let op1_string = get_op_string op1 in let op2_string = get_op_string op2 in Stdlib.compare op1_string op2_string -let syntactic_comparison expr1 expr2 = +let syntactic_comparison (expr1: xpr_t) (expr2: xpr_t) = let c_compare c1 c2 = match (c1,c2) with - | (SymSet s1, SymSet s2) -> + | (SymSet s1, SymSet s2) -> let l = Stdlib.compare (List.length s1) (List.length s2) in if l = 0 then list_compare s1 s2 (fun x y -> x#compare y) @@ -306,7 +349,7 @@ let syntactic_comparison expr1 expr2 = | (BoolConst b1, BoolConst b2) -> begin match (b1,b2) with - | (false, false) + | (false, false) | (true, true) -> 0 | (false, true) -> -1 | (true, false) -> 1 @@ -328,7 +371,7 @@ let syntactic_comparison expr1 expr2 = match (e1,e2) with (XConst c1, XConst c2) -> c_compare c1 c2 | (XVar v1, XVar v2) -> v1#compare v2 - | (XOp (op1, l1), XOp (op2, l2)) -> + | (XOp (op1, l1), XOp (op2, l2)) -> let l = compare_op op1 op2 in if l = 0 then list_compare l1 l2 e_compare else l | (XAttr (s1,ee1), XAttr (s2,ee2)) -> @@ -340,12 +383,13 @@ let syntactic_comparison expr1 expr2 = | (XOp _, _) -> -1 | (_, XOp _) -> 1 in e_compare expr1 expr2 - - -let rec _num_terms e = - match e with - XVar _ | XConst _ | XAttr _ -> 1 - | XOp (XPlus, l) | XOp (XMinus, l) -> - List.fold_left (fun a x -> a + (_num_terms x)) 0 l - | _ -> 1 - + + +let rec _num_terms (x: xpr_t) = + match x with + | XVar _ + | XConst _ + | XAttr _ -> 1 + | XOp (XPlus, l) | XOp (XMinus, l) -> + List.fold_left (fun a x -> a + (_num_terms x)) 0 l + | _ -> 1 diff --git a/CodeHawk/CH/xprlib/xprt.mli b/CodeHawk/CH/xprlib/xprt.mli index 43500a54..03a2f321 100644 --- a/CodeHawk/CH/xprlib/xprt.mli +++ b/CodeHawk/CH/xprlib/xprt.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2023 Aarno Labs LLC + Copyright (c) 2021-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal diff --git a/CodeHawk/CH/xprlib/xsimplify.ml b/CodeHawk/CH/xprlib/xsimplify.ml index c680ad62..8a88ecd9 100644 --- a/CodeHawk/CH/xprlib/xsimplify.ml +++ b/CodeHawk/CH/xprlib/xsimplify.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -45,6 +45,7 @@ exception XSimplificationProblem of CHPretty.pretty_t let xpr_to_pretty e = xpr_printer#pr_expr e +let x2p = xpr_to_pretty type e_struct_t = @@ -237,6 +238,18 @@ and reduce_plus (m: bool) (e1: xpr_t) (e2: xpr_t): (bool * xpr_t) = else match (e1, e2) with + (* (&y + x) ==> no further simplification *) + | (XOp ((Xf "addressofvar"), [_]), _) -> + (false, XOp (XPlus, [e1; e2])) + + (* (x + &y) ==> (&y + x) *) + | (_, XOp ((Xf "addressofvar"), [_])) -> + (true, XOp (XPlus, [e2; e1])) + + (* ((&x + y) + z) ==> (&x + (y + z)) *) + | (XOp (XPlus, [XOp ((Xf "addressofvar"), [x]); y]), z) -> + (true, XOp (XPlus, [XOp ((Xf "addressofvar"), [x]); XOp (XPlus, [y; z])])) + (* x + (y-x) ~> y *) | (x, XOp (XMinus, [y; z])) when syntactically_equal x z -> (true, y) @@ -263,7 +276,6 @@ and reduce_plus (m: bool) (e1: xpr_t) (e2: xpr_t): (bool * xpr_t) = XOp (XLsl, [y; XConst (IntConst b)])) when syntactically_equal x y -> rs XMult [x; XOp (XPlus, [pwr2 a; pwr2 b])] - | _ -> match (get_struct e1, get_struct e2) with @@ -363,6 +375,13 @@ and reduce_minus (m: bool) (e1: xpr_t) (e2: xpr_t) = (true, random_constant_expr) else match (e1, e2) with + + (* ((&x + y) - z) ==> (&x + (y - z)) *) + | (XOp (XPlus, [XOp ((Xf "addressofvar"), [x]); y]), _) -> + let _ = pr_debug [STR " DEBUG: reduce_minus: "; + STR "e1: "; x2p e1; STR "; e2: "; x2p e2; NL] in + rs XPlus [XOp ((Xf "addressofvar"), [x]); XOp (XMinus, [y; e2])] + (* (x << 3) - x) --> (7 * x) *) | (XOp (XLsl, [ee1; XConst (IntConst n)]), ee3) when syntactically_equal ee1 ee3 && n#equal (mkNumerical 3) -> @@ -412,6 +431,7 @@ and reduce_minus (m: bool) (e1: xpr_t) (e2: xpr_t) = | _ -> match (get_struct e1, get_struct e2) with + | (SConst a, SConst b) -> (* a - b *) (true, ne (a#sub b)) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 552aff60..3f94ab67 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -651,7 +651,7 @@ object (self) TR.tbind ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) self#env#mk_global_variable - (get_total_constant_offset memoff)) + (get_total_constant_offset memoff)) memoffset_r else TR.tmap @@ -661,7 +661,36 @@ object (self) memoffset_r) memref_r in - if inv#is_base_offset_constant var then + if self#f#env#is_addressof_symbolic_value var then + let xaofv_r = self#f#env#get_addressof_symbolic_expr var in + let memvar_r = + TR.tbind + (fun xaofv -> + match xaofv with + | XOp ((Xf "addressofvar"), [XVar v]) -> Ok v + | _ -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Expression is not an addressofvar expression: " + ^ (x2s xaofv)]) + xaofv_r in + let memoff_r = + TR.tbind + (fun memvar -> + let memtype = self#get_variable_type memvar in + let memtype = + match memtype with + | Some t -> t + | _ -> t_unknown in + address_memory_offset memtype (num_constant_expr numoffset)) + memvar_r in + TR.tbind + (fun memvar -> + TR.tbind + (fun memoff -> self#f#env#add_memory_offset memvar memoff) + memoff_r) + memvar_r + + else if inv#is_base_offset_constant var then let (base, offset) = inv#get_base_offset_constant var in let memoffset = numoffset#add offset in let memref_r = self#env#mk_base_sym_reference base in @@ -686,7 +715,7 @@ object (self) else XVar var in let addr = XOp (XPlus, [varx; num_constant_expr numoffset]) in - let address = inv#rewrite_expr addr in + let address = simplify_xpr (inv#rewrite_expr addr) in match address with | XConst (IntConst n) -> let dw = numerical_mod_to_doubleword n in @@ -701,8 +730,7 @@ object (self) ^ system_info#get_image_base#to_hex_string ^ ")"] | _ -> - let (memref_r, memoffset_r) = self#decompose_memaddr address in - mk_memvar memref_r memoffset_r + self#get_var_at_address ~size:(Some size) address method get_memory_variable_1 ?(align=1) (* alignment of var value *) @@ -1246,22 +1274,72 @@ object (self) method get_fts_parameter_expr (_p: fts_parameter_t) = None + method private normalize_addrvalue (x: xpr_t): xpr_t = + simplify_xpr x + method get_var_at_address ?(size=None) ?(btype=t_unknown) (addrvalue: xpr_t): variable_t traceresult = - match memmap#xpr_containing_location addrvalue with - | Some gloc -> - (TR.tmap - (fun offset -> self#f#env#mk_gloc_variable gloc offset) - (gloc#address_memory_offset ~tgtsize:size ~tgtbtype:btype addrvalue)) + match self#normalize_addrvalue addrvalue with + | XOp ((Xf "addressofvar"), [XVar v]) -> Ok v + | XOp (XPlus, [XOp ((Xf "addressofvar"), [XVar v]); xoff]) + when self#f#env#is_global_variable v -> + let gvaddr_r = self#f#env#get_global_variable_address v in + TR.tbind + (fun gvaddr -> + if memmap#has_location gvaddr then + let gloc = memmap#get_location gvaddr in + TR.tmap + (fun offset -> self#f#env#mk_gloc_variable gloc offset) + (gloc#address_offset_memory_offset + ~tgtsize:size ~tgtbtype:btype xoff) + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ (p2s self#l#toPretty) + ^ ": " + ^ "Global location at address " + ^ gvaddr#to_hex_string + ^ " not found"]) + gvaddr_r | _ -> - let (memref_r, memoff_r) = self#decompose_memaddr addrvalue in - TR.tmap2 - ~msg1:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun memref memoff -> - self#f#env#mk_offset_memory_variable memref memoff) - memref_r memoff_r + match memmap#xpr_containing_location addrvalue with + | Some gloc -> + (TR.tmap + (fun offset -> self#f#env#mk_gloc_variable gloc offset) + (gloc#address_memory_offset ~tgtsize:size ~tgtbtype:btype addrvalue)) + | _ -> + let (memref_r, memoff_r) = self#decompose_memaddr addrvalue in + TR.tmap2 + ~msg1:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (fun memref memoff -> + self#f#env#mk_offset_memory_variable memref memoff) + memref_r memoff_r + + method private get_variable_type (v: variable_t): btype_t option = + if self#f#env#is_initial_register_value v then + let reg_r = self#f#env#get_initial_register_value_register v in + let param_r = + TR.tbind + (fun reg -> + if self#f#get_summary#has_parameter_for_register reg then + Ok (self#f#get_summary#get_parameter_for_register reg) + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ (p2s v#toPretty) + ^ " does not have an associated parameter"]) + reg_r in + TR.tfold_default + (fun param -> Some param.apar_type) + (self#env#get_variable_type v) + param_r + else + self#env#get_variable_type v + + method get_xpr_type (x: xpr_t): btype_t option = + match x with + | XVar v -> self#get_variable_type v + | _ -> None method decompose_memaddr (x: xpr_t): (memory_reference_int traceresult * memory_offset_t traceresult) = @@ -1273,7 +1351,7 @@ object (self) | [base] -> let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in let memref_r = self#env#mk_base_variable_reference base in - let vartype = self#f#env#get_variable_type base in + let vartype = self#get_variable_type base in let vartype = match vartype with None -> t_unknown | Some t -> t in let memoff_r = address_memory_offset vartype offset in (* @@ -1310,6 +1388,7 @@ object (self) | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s self#l#toPretty) ^ ": " + ^ "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "Offset from global base " ^ maxC#toString ^ " not recognized: " ^ (x2s offset)] in @@ -1335,6 +1414,7 @@ object (self) | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s self#l#toPretty) ^ ": " + ^ "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "Offset from base " ^ (x2s (XVar base)) ^ " not recognized: " ^ (x2s offset)] in @@ -1364,6 +1444,7 @@ object (self) | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s self#l#toPretty) ^ ": " + ^ "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "Offset from base " ^ (x2s (XVar base)) ^ " not recognized: " ^ (x2s offset)]) @@ -1384,6 +1465,7 @@ object (self) let memref_r = Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s self#l#toPretty) ^ ": " + ^ "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "No candidate pointers. Left with maxC: " ^ maxC#toString] in let memoff_r = @@ -1395,6 +1477,7 @@ object (self) let memref_r = Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s self#l#toPretty) ^ ": " + ^ "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "Multiple variables: " ^ (String.concat "; " (List.map (fun v -> p2s v#toPretty) vars))] in @@ -1407,6 +1490,7 @@ object (self) let memref_r = Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s self#l#toPretty) ^ ": " + ^ "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "Multiple known pointers: " ^ (String.concat "; " (List.map (fun v -> p2s v#toPretty) knownpointers))] in @@ -1638,13 +1722,16 @@ object (self) [BRANCH [LF.mkCode truecmds; LF.mkCode falsecmds]] method private is_composite_symbolic_value (x: xpr_t): bool = - let is_external v = self#f#env#is_function_initial_value v in - let is_fixed_type v = - (is_external v) - || (self#f#env#is_symbolic_value v) in - let vars = variables_in_expr x in - (List.length vars) > 0 - && List.for_all is_fixed_type (variables_in_expr x) + match x with + | XOp ((Xf "addressofvar"), [XVar _]) -> true + | _ -> + let is_external v = self#f#env#is_function_initial_value v in + let is_fixed_type v = + (is_external v) + || (self#f#env#is_symbolic_value v) in + let vars = variables_in_expr x in + (List.length vars) > 0 + && List.for_all is_fixed_type (variables_in_expr x) method get_assign_commands_r ?(signed=false) @@ -1693,6 +1780,26 @@ object (self) else rhs in + let rhs = + (* if rhs is the address of a global variable create an address-of + expression for that global variable. *) + match rhs with + | XConst (IntConst n) -> + let dw = numerical_mod_to_doubleword n in + if memmap#has_location dw then + TR.tfold + ~ok:(fun gv -> XOp ((Xf "addressofvar"), [XVar gv])) + ~error:(fun e -> + begin + log_result + ~tag:"assign global variable address" __FILE__ __LINE__ e; + rhs + end) + (self#f#env#mk_global_variable n) + else + rhs + | _ -> rhs in + let rhs = (* if rhs is a composite symbolic expression, create a new variable for it *) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index da626ee7..aafe5c33 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1536,6 +1536,37 @@ object (self) method is_signed_symbolic_value = varmgr#is_signed_symbolic_value + method is_addressof_symbolic_value (v: variable_t) = + if self#is_symbolic_value v then + let symx_r = self#get_symbolic_value_expr v in + TR.tfold_default + (fun symx -> + match symx with + | XOp ((Xf "addressofvar"), _) -> true + | _ -> false) + false + symx_r + else + false + + method get_addressof_symbolic_expr (v: variable_t): xpr_t traceresult = + if self#is_addressof_symbolic_value v then + let symx_r = self#get_symbolic_value_expr v in + TR.tbind + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (fun symx -> + match symx with + | XOp ((Xf "addressofvar"), [x]) -> Ok x + | _ -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Not an addressofvar symbolic expression: " + ^ (x2s symx)]) + symx_r + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Not a symbolic-value expression: " + ^ (p2s v#toPretty)] + method get_symbolic_value_expr (v: variable_t): xpr_t traceresult = if self#is_symbolic_value v then varmgr#get_symbolic_value_expr v diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml index b93d2f2d..9e4cc725 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml @@ -146,6 +146,10 @@ object (self:'a) (BCH_failure (LBLOCK [STR "Internal error: get_parameter_for_register"])) + method has_parameter_for_register (reg: register_t): bool = + Option.is_some + (get_register_parameter_for_register self#get_function_interface reg) + method get_parameter_at_stack_offset (offset: int): fts_parameter_t = let spar = get_stack_parameter_at_offset self#get_function_interface offset in match spar with diff --git a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml index a294ce51..b6e9470d 100644 --- a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml +++ b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024 Aarno Labs LLC + Copyright (c) 2024-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -370,37 +370,41 @@ object (self) ^ "xoffset: " ^ (x2s xoffset) ^ "; btype: " ^ (btype_to_string btype)] + method address_offset_memory_offset + ?(tgtsize=None) + ?(tgtbtype=t_unknown) + (xoffset: xpr_t): memory_offset_t traceresult = + match xoffset with + | XConst (IntConst n) + when n#equal CHNumerical.numerical_zero + && Option.is_none tgtsize + && is_unknown_type tgtbtype -> + Ok NoOffset + | XConst (IntConst n) + when n#equal CHNumerical.numerical_zero && (not self#is_typed) -> + Ok NoOffset + | XConst (IntConst n) when not self#is_typed -> + Ok (ConstantOffset (n, NoOffset)) + | _ -> + let tgtbtype = + if is_unknown_type tgtbtype then None else Some tgtbtype in + if self#is_struct then + let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in + self#structvar_memory_offset ~tgtsize ~tgtbtype btype xoffset + else if self#is_array then + let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in + self#arrayvar_memory_offset ~tgtsize ~tgtbtype btype xoffset + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" + ^ (btype_to_string self#btype) + ^ " is not known to be a struct or array"] + method address_memory_offset ?(tgtsize=None) ?(tgtbtype=t_unknown) (xpr: xpr_t): memory_offset_t traceresult = - tbind - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun xoffset -> - match xoffset with - | XConst (IntConst n) - when n#equal CHNumerical.numerical_zero - && Option.is_none tgtsize - && is_unknown_type tgtbtype -> - Ok NoOffset - | XConst (IntConst n) - when n#equal CHNumerical.numerical_zero && (not self#is_typed) -> - Ok NoOffset - | XConst (IntConst n) when not self#is_typed -> - Ok (ConstantOffset (n, NoOffset)) - | _ -> - let tgtbtype = - if is_unknown_type tgtbtype then None else Some tgtbtype in - if self#is_struct then - let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in - self#structvar_memory_offset ~tgtsize ~tgtbtype btype xoffset - else if self#is_array then - let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in - self#arrayvar_memory_offset ~tgtsize ~tgtbtype btype xoffset - else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" - ^ (btype_to_string self#btype) - ^ " is not known to be a struct or array"]) + TR.tbind + (self#address_offset_memory_offset ~tgtsize ~tgtbtype) (self#address_offset xpr) method initialvalue: globalvalue_t option = grec.gloc_initialvalue diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 46fc7c53..d5eb51f9 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -2385,6 +2385,8 @@ object ('a) method get_parameter_for_register: register_t -> fts_parameter_t + method has_parameter_for_register: register_t -> bool + method get_parameter_at_stack_offset: int -> fts_parameter_t method get_returntype: btype_t @@ -4231,6 +4233,7 @@ object [var] cannot be found. *) method get_symbolic_value_expr: variable_t -> xpr_t traceresult + (** {3 Other} *) method is_function_initial_value: variable_t -> bool @@ -4358,6 +4361,12 @@ class type global_location_int = -> xpr_t -> memory_offset_t traceresult + method address_offset_memory_offset: + ?tgtsize:int option + -> ?tgtbtype:btype_t + -> xpr_t + -> memory_offset_t traceresult + method has_elf_symbol: bool method write_xml: xml_element_int -> unit @@ -4946,6 +4955,11 @@ class type function_environment_int = Returns [Error] if [var] is not a symbolic expression variable.*) method get_symbolic_value_expr: variable_t -> xpr_t traceresult + method is_addressof_symbolic_value: variable_t -> bool + + method get_addressof_symbolic_expr: variable_t -> xpr_t traceresult + + (** {3 Other} *) method is_function_initial_value: variable_t -> bool @@ -5925,6 +5939,8 @@ class type floc_int = -> xpr_t (** address value *) -> variable_t traceresult + method get_xpr_type: xpr_t -> btype_t option + (** {2 Predicates on variables}*) (* returns true if the given variable evaluates to a constant at this diff --git a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml index 2bf469ff..0433c681 100644 --- a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml +++ b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -58,6 +58,7 @@ module H = Hashtbl module TR = CHTraceResult +(* let x2p = XprToPretty.xpr_formatter#pr_expr *) let tracked_locations = [] let track_location loc p = diff --git a/CodeHawk/CHB/bchlib/bCHMemoryReference.mli b/CodeHawk/CHB/bchlib/bCHMemoryReference.mli index d9389359..04042dee 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryReference.mli +++ b/CodeHawk/CHB/bchlib/bCHMemoryReference.mli @@ -69,6 +69,14 @@ val mk_maximal_memory_offset: numerical_t -> btype_t -> memory_offset_t val add_offset: memory_offset_t -> memory_offset_t -> memory_offset_t + +(** [address_memory_offset tgtsize tgttype ty offset] returns the symbolic offset + that corresponds with the numerical offset [offset] for a base variable with + type [ty]. The optional arguments [tgtsize] and [tgttype] can be used to + disambiguate between for example an entire struct or only its first field. + + An error is returned if the the symbolic offset cannot be constructed. + *) val address_memory_offset: ?tgtsize: int option -> ?tgtbtype: btype_t diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml index 7bc460a0..e4db3e9a 100644 --- a/CodeHawk/CHB/bchlib/bCHVariable.ml +++ b/CodeHawk/CHB/bchlib/bCHVariable.ml @@ -174,7 +174,10 @@ object (self:'a) self#get_memref_type i size | MemoryVariable (_, size, (FieldOffset _ as offset)) -> self#get_memref_field_type size offset - | MemoryVariable _ -> None + | MemoryVariable (_, size, (ConstantOffset (_, (FieldOffset _ as offset)))) -> + self#get_memref_field_type size offset + | MemoryVariable _ -> + None | RegisterVariable _ -> None | CPUFlagVariable _ -> None | AuxiliaryVariable a -> diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 4a7a828f..d015baaa 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20250203" - ~date:"2025-02-03" + ~version:"0.6.0_20250210" + ~date:"2025-02-10" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlib/bCHXprUtil.ml b/CodeHawk/CHB/bchlib/bCHXprUtil.ml index e6593be2..237b3640 100644 --- a/CodeHawk/CHB/bchlib/bCHXprUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHXprUtil.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2022 Henny B. Sipma - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -30,7 +30,9 @@ (* chlib *) open CHLanguage open CHNumerical -open CHPretty + +(* chutil *) +open CHLogger (* xprlib *) open Xprt @@ -40,6 +42,8 @@ open Xsimplify let x2p = xpr_formatter#pr_expr +let p2s = CHPrettyUtil.pretty_to_string +let x2s (x: xpr_t) = p2s (x2p x) (* returns the largest constant term in the given expression, taking sign @@ -87,7 +91,10 @@ let normalize_scaled_ivar_expr (xpr: xpr_t) (ivar: variable_t): xpr_t option = Some x | _ -> let _ = - pr_debug [STR "DEBUG: expression not rewritten: "; x2p x; NL] in + log_error_result + ~tag:"normalize-scaled-ivar-expr" + __FILE__ __LINE__ + [(x2s x) ^ " with ivar " ^ (p2s ivar#toPretty)] in None in aux xpr @@ -97,7 +104,8 @@ let normalize_scaled_ivar_expr (xpr: xpr_t) (ivar: variable_t): xpr_t option = let rec vars_as_positive_terms (x:xpr_t) = match x with XVar v -> [ v ] - | XOp (XPlus, [ x1 ; x2 ]) -> (vars_as_positive_terms x1) @ (vars_as_positive_terms x2) + | XOp (XPlus, [ x1 ; x2 ]) -> + (vars_as_positive_terms x1) @ (vars_as_positive_terms x2) | XOp (XMinus, [ x1 ; _ ]) -> vars_as_positive_terms x1 | _ -> [] diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 3d535ca6..99a3887d 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -605,7 +605,7 @@ object (self) Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "Parameter type not recognized in call instruction"] in let xx = rewrite_expr ?restrict:(Some 4) x in - (* + let ptype = get_parameter_type p in let xx = if is_pointer ptype then let _ = floc#memrecorder#record_argument xx index in @@ -618,10 +618,9 @@ object (self) TR.tfold_default (fun v -> XOp ((Xf "addressofvar"), [(XVar v)])) xx - (floc#get_var_at_address ~btype:ptype xx) + (floc#get_var_at_address ~btype:(ptr_deref ptype) xx) else xx in - *) let rdef = get_rdef_r xvar_r in (xx :: xprs, xvar_r :: xvars, rdef :: rdefs, index + 1)) ([], [], [], 1) callargs in @@ -2530,7 +2529,7 @@ object (self) let xxdst_r = TR.tmap (fun v -> XOp ((Xf "addressofvar"), [(XVar v)])) - (TR.tbind (fun x -> floc#get_var_at_address x) xxdst_r) in + (TR.tbind floc#get_var_at_address xxdst_r) in let rdefs = [(get_rdef_r xsrc_r); (get_rdef_r xdst_r)] in let _ = TR.tfold_default @@ -2636,6 +2635,7 @@ object (self) let xrm_r = rm#to_expr floc in let xxrt_r = TR.tmap rewrite_expr xrt_r in let xxaddr_r = TR.tmap rewrite_expr xaddr_r in + let lhsvar_r = TR.tbind floc#get_var_at_address xxaddr_r in let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r; @@ -2644,7 +2644,7 @@ object (self) let uses = [get_def_use_r vmem_r] in let useshigh = [get_def_use_high_r vmem_r] in let xprs_r = [xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r] in - let vars_r = [vmem_r] in + let vars_r = [vmem_r; lhsvar_r] in let _ = floc#memrecorder#record_store_r ~addr_r:xxaddr_r @@ -2679,6 +2679,8 @@ object (self) let xrm_r = rm#to_expr floc in let xxrt_r = TR.tmap rewrite_expr xrt_r in let xxaddr_r = TR.tmap rewrite_expr xaddr_r in + let lhsvar_r = + TR.tbind (floc#get_var_at_address ~size:(Some 1)) xxaddr_r in let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r; @@ -2695,7 +2697,7 @@ object (self) ~xpr_r:xxrt_r in let (tagstring, args) = mk_instrx_data_r - ~vars_r:[vmem_r] + ~vars_r:[vmem_r; lhsvar_r] ~xprs_r:[xrn_r; xrm_r; xrt_r; xxrt_r; xaddr_r] ~rdefs ~uses diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 4f3b2651..f1fe2528 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -424,12 +424,12 @@ object (self) (* add constraints for argument values *) List.iter (fun (p, x) -> let ptype = get_parameter_type p in - if is_register_parameter p then - let regarg = TR.tget_ok (get_register_parameter_register p) in - let pvar = floc#f#env#mk_register_variable regarg in - let rdefs = get_variable_rdefs pvar in - begin - (if not (is_unknown_type ptype) then + begin + (if is_register_parameter p then + let regarg = TR.tget_ok (get_register_parameter_register p) in + let pvar = floc#f#env#mk_register_variable regarg in + let rdefs = get_variable_rdefs pvar in + if not (is_unknown_type ptype) then List.iter (fun rdsym -> let typevar = mk_reglhs_typevar regarg faddr rdsym#getBaseName in @@ -444,53 +444,57 @@ object (self) begin log_no_type_constraint "BL-reg-arg" ptype; () - end) rdefs); - - (match getopt_stackaddress x with - | None -> () - | Some offset -> - let lhstypevar = - mk_localstack_lhs_typevar offset faddr iaddr in - if is_pointer ptype then - let eltype = ptr_deref ptype in - let atype = t_array eltype 1 in - let opttc = mk_btype_constraint lhstypevar atype in - match opttc with - | Some tc -> - begin - log_type_constraint "BL-reg-arg" tc; - store#add_constraint tc - end - | _ -> ()) - end - - else if is_stack_parameter p then - (log_tfold_default - (log_error - ("Unable to retrieve stack offset from " - ^ (fts_parameter_to_string p))) - (fun p_offset -> - (log_tfold_default - (log_error "Unable to get current stack pointer offset") - (fun sp_offset -> - let arg_offset = - (sp_offset#add (mkNumerical p_offset))#neg in - let typevar = - mk_localstack_lhs_typevar - arg_offset#toInt faddr iaddr in - let opttc = mk_btype_constraint typevar ptype in - match opttc with - | Some tc -> - begin - log_type_constraint "BL-reg-arg" tc; - store#add_constraint tc - end - | _ -> ()) - () - (floc#get_singleton_stackpointer_offset))) - () - (get_stack_parameter_offset p)) - + end) rdefs + else + () + + else if is_stack_parameter p then + (log_tfold_default + (log_error + ("Unable to retrieve stack offset from " + ^ (fts_parameter_to_string p))) + (fun p_offset -> + (log_tfold_default + (log_error "Unable to get current stack pointer offset") + (fun sp_offset -> + let arg_offset = + (sp_offset#add (mkNumerical p_offset))#neg in + let typevar = + mk_localstack_lhs_typevar + arg_offset#toInt faddr iaddr in + let opttc = mk_btype_constraint typevar ptype in + match opttc with + | Some tc -> + begin + log_type_constraint "BL-stack-arg" tc; + store#add_constraint tc + end + | _ -> ()) + () + (floc#get_singleton_stackpointer_offset))) + () + (get_stack_parameter_offset p)) + + else + ()); + + (match getopt_stackaddress x with + | None -> () + | Some offset -> + let lhstypevar = + mk_localstack_lhs_typevar offset faddr iaddr in + if is_pointer ptype then + let eltype = ptr_deref ptype in + let atype = t_array eltype 1 in + let opttc = mk_btype_constraint lhstypevar atype in + match opttc with + | Some tc -> + begin + log_type_constraint "BL-reg-arg" tc; + store#add_constraint tc + end + | _ -> ()) + end ) callargs end @@ -574,6 +578,7 @@ object (self) let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in begin + (* variable introduction for lhs with type *) (match get_regvar_type_annotation () with | Some t -> let opttc = mk_btype_constraint rttypevar t in @@ -586,6 +591,24 @@ object (self) | _ -> ()) | _ -> ()); + (* loaded type may be known *) + (let xmem_r = memop#to_expr floc in + let xrmem_r = + TR.tmap (fun x -> simplify_xpr (floc#inv#rewrite_expr x)) xmem_r in + let xtype_r = TR.tmap floc#get_xpr_type xrmem_r in + let xtype_opt = TR.tvalue xtype_r ~default:None in + match xtype_opt with + | Some t -> + let opttc = mk_btype_constraint rttypevar t in + (match opttc with + | Some tc -> + begin + log_type_constraint "LDR-var" tc; + store#add_constraint tc + end + | _ -> ()) + | _ -> ()); + (* LDR rt, [rn, rm] : X_rndef.load <: X_rt *) (let xrdef = get_variable_rdefs_r (rn#to_variable floc) in let rnreg = rn#to_register in @@ -985,43 +1008,64 @@ object (self) end (* Store x in y --- *y := x --- X <: Y.store *) - | StoreRegister (_, rt, _rn, rm, memvarop, _) when rm#is_immediate -> + | StoreRegister (_, rt, rn, rm, memvarop, _) when rm#is_immediate -> + let rnrdefs = get_variable_rdefs_r (rn#to_variable floc) in + let rnreg = rn#to_register in + let offset = rm#to_numerical#toInt in + let rtrdefs = get_variable_rdefs_r (rt#to_variable floc) in + let rtreg = rt#to_register in let xaddr_r = memvarop#to_address floc in let xrt_r = rt#to_expr floc in - (match getopt_stackaddress_r xaddr_r with - | None -> () - | Some offset -> - let lhstypevar = mk_localstack_lhs_typevar offset faddr iaddr in - begin - (* propagate function argument type *) - (match getopt_initial_argument_value_r xrt_r with - | Some (rtreg, off) when off = 0 -> - let rhstypevar = mk_function_typevar faddr in - let rhstypevar = add_freg_param_capability rtreg rhstypevar in - let rhstypeterm = mk_vty_term rhstypevar in - let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint "STR-funarg" rhstypeterm lhstypeterm; - store#add_subtype_constraint rhstypeterm lhstypeterm - end - | _ -> ()); - - (* propagate src register type from rdefs *) - (let rtreg = rt#to_register in - let rtvar_r = rt#to_variable floc in - let rtrdefs = get_variable_rdefs_r rtvar_r in - List.iter (fun rtrdef -> - let rtaddr = rtrdef#getBaseName in - if rtaddr != "init" then - let rttypevar = mk_reglhs_typevar rtreg faddr rtaddr in - let rttypeterm = mk_vty_term rttypevar in - let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint "STR-imm-off" rttypeterm lhstypeterm; - store#add_subtype_constraint rttypeterm lhstypeterm - end) rtrdefs) - end - ) + begin + + (match getopt_stackaddress_r xaddr_r with + | None -> () + | Some offset -> + let lhstypevar = mk_localstack_lhs_typevar offset faddr iaddr in + begin + (* propagate function argument type *) + (match getopt_initial_argument_value_r xrt_r with + | Some (rtreg, off) when off = 0 -> + let rhstypevar = mk_function_typevar faddr in + let rhstypevar = add_freg_param_capability rtreg rhstypevar in + let rhstypeterm = mk_vty_term rhstypevar in + let lhstypeterm = mk_vty_term lhstypevar in + begin + log_subtype_constraint "STR-funarg" rhstypeterm lhstypeterm; + store#add_subtype_constraint rhstypeterm lhstypeterm + end + | _ -> ()); + + (* propagate src register type from rdefs *) + (let rtreg = rt#to_register in + let rtvar_r = rt#to_variable floc in + let rtrdefs = get_variable_rdefs_r rtvar_r in + List.iter (fun rtrdef -> + let rtaddr = rtrdef#getBaseName in + if rtaddr != "init" then + let rttypevar = mk_reglhs_typevar rtreg faddr rtaddr in + let rttypeterm = mk_vty_term rttypevar in + let lhstypeterm = mk_vty_term lhstypevar in + begin + log_subtype_constraint "STR-imm-off" rttypeterm lhstypeterm; + store#add_subtype_constraint rttypeterm lhstypeterm + end) rtrdefs) + end); + + (List.iter (fun rndsym -> + let straddr = rndsym#getBaseName in + let rntypevar = mk_reglhs_typevar rnreg faddr straddr in + let rntypevar = add_load_capability ~size:4 ~offset rntypevar in + List.iter (fun rtdsym -> + let rtdloc = rtdsym#getBaseName in + let rttypevar = mk_reglhs_typevar rtreg faddr rtdloc in + let rttypeterm = mk_vty_term rttypevar in + let rntypeterm = mk_vty_term rntypevar in + begin + log_subtype_constraint "STR-imm-off" rttypeterm rntypeterm; + store#add_subtype_constraint rttypeterm rntypeterm + end) rtrdefs) rnrdefs) + end | StoreRegisterByte (_, rt, rn, rm, _memvarop, _) when rm#is_immediate -> let rnrdefs = get_variable_rdefs_r (rn#to_variable floc) in diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index c215ad06..965e6322 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -1648,6 +1648,7 @@ let translate_arm_instruction | LoadRegister (c, rt, rn, rm, mem, _) -> let lhs_r = TR.tmap fst (rt#to_lhs floc) in let rhs_r = mem#to_expr floc in + let rhs_r = TR.tmap floc#inv#rewrite_expr rhs_r in let vrd = floc#env#mk_register_variable rt#to_register in let updatecmds = if mem#is_offset_address_writeback then diff --git a/CodeHawk/CHT/CH_tests/xprlib_tests/txprlib/tCHXprlibGenerator.ml b/CodeHawk/CHT/CH_tests/xprlib_tests/txprlib/tCHXprlibGenerator.ml index d6b7ed42..8e10136f 100644 --- a/CodeHawk/CHT/CH_tests/xprlib_tests/txprlib/tCHXprlibGenerator.ml +++ b/CodeHawk/CHT/CH_tests/xprlib_tests/txprlib/tCHXprlibGenerator.ml @@ -1,13 +1,13 @@ (* ============================================================================= - CodeHawk Unit Testing Framework + CodeHawk Unit Testing Framework Author: Henny Sipma Adapted from: Kaputt (https://kaputt.x9c.fr/index.html) ------------------------------------------------------------------------------ The MIT License (MIT) - + Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2022-2023 Aarno Labs LLC + Copyright (c) 2022-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -15,10 +15,10 @@ to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: - + The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. - + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE @@ -61,6 +61,11 @@ let mk_neg (x: xpr_t) = XOp (XNeg, [x]) let mk_var (name: string) = new variable_t (new symbol_t name) NUM_VAR_TYPE +let mk_addressof (name: string) = + let v = mk_var name in + XOp ((Xf "addressofvar"), [XVar v]) + + let mk_vars (name: string) (n: int) = let rec aux nn result = if nn = 0 then diff --git a/CodeHawk/CHT/CH_tests/xprlib_tests/txprlib/tCHXprlibGenerator.mli b/CodeHawk/CHT/CH_tests/xprlib_tests/txprlib/tCHXprlibGenerator.mli index 619d4573..9ecc336c 100644 --- a/CodeHawk/CHT/CH_tests/xprlib_tests/txprlib/tCHXprlibGenerator.mli +++ b/CodeHawk/CHT/CH_tests/xprlib_tests/txprlib/tCHXprlibGenerator.mli @@ -7,7 +7,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny B. Sipma - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -53,3 +53,5 @@ val mk_neg: xpr_t -> xpr_t val mk_var: string -> variable_t val mk_vars: string -> int -> variable_t list + +val mk_addressof: string -> xpr_t diff --git a/CodeHawk/CHT/CH_tests/xprlib_tests/txxprlib/xsimplifyTest.ml b/CodeHawk/CHT/CH_tests/xprlib_tests/txxprlib/xsimplifyTest.ml index e5731c50..d7dbb9b0 100644 --- a/CodeHawk/CHT/CH_tests/xprlib_tests/txxprlib/xsimplifyTest.ml +++ b/CodeHawk/CHT/CH_tests/xprlib_tests/txxprlib/xsimplifyTest.ml @@ -7,7 +7,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -42,7 +42,7 @@ let simplify = S.simplify_xpr let testname = "xsimplifyTest" -let lastupdated = "2024-06-19" +let lastupdated = "2025-02-07" let basic () = @@ -562,6 +562,61 @@ let reduce_plus () = r (simplify (XOp (XPlus, [XOp (XShiftlt, [x; a]); XOp (XShiftlt, [x; b])])))); + (* (xbase + a) ==> (xbase + a) *) + TS.add_simple_test + ~title: "base_no_move" + (fun () -> + let a = XG.mk_ix 2 in + let v = XG.mk_var "x" in + let x = XOp (XPlus, [XOp ((Xf "addressofvar"), [XVar v]); a]) in + XA.equal_xpr x (simplify x)); + + (* (a + xbase) -> (xbase + a) *) + TS.add_simple_test + ~title: "base_move" + (fun () -> + let a = XG.mk_ix 2 in + let aofv = XG.mk_addressof "v" in + let r = XOp (XPlus, [aofv; a]) in + let x = XOp (XPlus, [a; aofv]) in + XA.equal_xpr r (simplify x)); + + (* (a + xbase) - b ==> xbase + (a - b) *) + TS.add_simple_test + ~title: "base_move_out" + (fun () -> + let a = XVar (XG.mk_var "x") in + let b = XVar (XG.mk_var "y") in + let aofv = XG.mk_addressof "v" in + let x = XOp (XMinus, [XOp (XPlus, [a; aofv]); b]) in + let r = XOp (XPlus, [aofv; XOp (XMinus, [a; b])]) in + XA.equal_xpr r (simplify x)); + + (* (xbase + ((x * y) - z)) => unchanged *) + TS.add_simple_test + ~title: "base_index_expr" + (fun () -> + let x = XVar (XG.mk_var "x") in + let y = XVar (XG.mk_var "y") in + let z = XG.mk_ix 2 in + let aofv = XG.mk_addressof "v" in + let p = XOp (XMult, [x; y]) in + let xx = XOp (XPlus, [aofv; XOp (XMinus, [p; z])]) in + XA.equal_xpr xx (simplify xx)); + + (* ((xbase + y) + z) ==> (xbase + (y + z)) *) + TS.add_simple_test + ~title:"base_p_move_out" + (fun () -> + let aofv = XG.mk_addressof "v" in + let y = XVar (XG.mk_var "y") in + let z = XVar (XG.mk_var "z") in + let x = XOp (XPlus, [XOp (XPlus, [aofv; y]); z]) in + let r = XOp (XPlus, [aofv; XOp (XPlus, [y; z])]) in + XA.equal_xpr r (simplify x)); + + (* ((addressofvar (gv_0x5e1e1c) + ((68 * R0_in[4]_in) - 68)) + 40) *) + TS.launch_tests () end