diff --git a/CodeHawk/CH/xprlib/xsimplify.ml b/CodeHawk/CH/xprlib/xsimplify.ml index 04f73bec..aafce4b9 100644 --- a/CodeHawk/CH/xprlib/xsimplify.ml +++ b/CodeHawk/CH/xprlib/xsimplify.ml @@ -153,6 +153,7 @@ let rec sim_expr (m:bool) (e:xpr_t):(bool * xpr_t) = | XAsr -> reduce_asr m s1 s2 | XLsl -> reduce_lsl m s1 s2 | XBAnd -> reduce_bitwiseand m s1 s2 + | XLAnd -> reduce_and m s1 s2 | XDisjoint -> reduce_disjoint m s1 s2 | XSubset -> reduce_subset m s1 s2 | XNumJoin -> reduce_binary_numjoin m s1 s2 @@ -1091,9 +1092,14 @@ and reduce_bor m e1 e2 = and reduce_or m e1 e2 = let default = (m, XOp (XLOr, [e1 ; e2])) in - if is_true e1 || is_true e2 then (true, true_constant_expr) - else if is_false e1 then (true, e2) - else if is_false e2 then (true, e1) + if is_true e1 || is_true e2 then + (true, true_constant_expr) + else if is_false e1 then + (true, e2) + else if is_false e2 then + (true, e1) + else if syntactically_equal e1 e2 then + (true, e1) else match (e1,e2) with | (XConst XRandom, XOp (XLOr, [XConst XRandom; b])) | (XConst XRandom, XOp (XLOr, [b; XConst XRandom])) @@ -1145,6 +1151,19 @@ and reduce_bitwiseand m e1 e2 = default end +and reduce_and m e1 e2 = + let default = (m, XOp (XLAnd, [e1; e2])) in + if is_true e1 && is_true e2 then + (true, true_constant_expr) + else if is_true e1 then + (true, e2) + else if is_true e2 then + (true, e1) + else if syntactically_equal e1 e2 then + (true, e1) + else + default + and reduce_shiftleft (m: bool) (e1: xpr_t) (e2: xpr_t): bool * xpr_t = let default = (m, XOp (XShiftlt, [e1; e2])) in diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 8da29235..ea077427 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -1420,6 +1420,7 @@ object (self) let memref_r = self#env#mk_base_variable_reference base in let memoff_r = match offset with + | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " @@ -1497,6 +1498,7 @@ object (self) let memref_r = self#env#mk_base_variable_reference base in let memoff_r = match offset with + | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " @@ -1704,7 +1706,24 @@ object (self) __FILE__ __LINE__ ["x: " ^ (x2s x) ^ "; exp: " ^ (x2s exp)] in Ok exp in - aux x + let result = aux x in + match result with + | Ok okresult -> + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"convert-xpr-offsets:result" + __FILE__ __LINE__ + ["x: " ^ (x2s x) ^ "; exp: " ^ (x2s okresult)] in + result + | Error e -> + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"convert-xpr-offsets:failure" + __FILE__ __LINE__ + ["x: " ^ (x2s x) ^ "; " ^ (String.concat "; " e)] in + result method get_xpr_type (x: xpr_t): btype_t traceresult = match x with @@ -1726,6 +1745,7 @@ object (self) (* let memoff_r = address_memory_offset t_unknown offset in *) let memoff_r = match offset with + | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " @@ -1745,6 +1765,7 @@ object (self) let offset = simplify_xpr (XOp (XMinus, [x; num_constant_expr maxC])) in let gmemoff_r = match offset with + | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | XOp (XMult, [XConst (IntConst n); XVar v]) -> Ok (IndexOffset (v, n#toInt, NoOffset)) @@ -1775,6 +1796,7 @@ object (self) let memref_r = self#env#mk_base_variable_reference base in let memoff_r = match offset with + | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | XOp (XMult, [XConst (IntConst n); XVar v]) -> Ok (IndexOffset (v, n#toInt, NoOffset)) @@ -1805,6 +1827,7 @@ object (self) (fun base -> let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in match offset with + | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | XOp (XMult, [XConst (IntConst n); XVar v]) -> Ok (IndexOffset (v, n#toInt, NoOffset)) @@ -1967,6 +1990,7 @@ object (self) (log_error "decompose_address" "invalid memref") ~ok:(fun memref -> let offset = match xoffset with + | XConst (IntConst n) when n#equal numerical_zero -> NoOffset | XConst (IntConst n) -> ConstantOffset (n, NoOffset) | XOp (XMult, [XConst (IntConst n); XVar v]) -> IndexOffset (v, n#toInt, NoOffset) @@ -1976,6 +2000,7 @@ object (self) (self#env#mk_base_variable_reference v) | Some (XConst (IntConst n), xoffset) -> let offset = match xoffset with + | XConst (IntConst n) when n#equal numerical_zero -> NoOffset | XConst (IntConst n) -> ConstantOffset (n, NoOffset) | XOp (XMult, [XConst (IntConst n); XVar v]) -> IndexOffset (v, n#toInt, NoOffset) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index eb6ad7c7..7c88532e 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -765,7 +765,11 @@ object (self) | BaseVar v when variable_names#has v#getName#getSeqNumber -> Some (variable_names#get v#getName#getSeqNumber) | _ -> None in - let offset = ConstantOffset (offset, NoOffset) in + let offset = + if offset#equal numerical_zero then + NoOffset + else + ConstantOffset (offset, NoOffset) in let avar = varmgr#make_memory_variable ~size memref offset in let v = self#mk_variable avar in let _ = match optName with diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml index 7517afc5..b6ac0258 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml @@ -1133,7 +1133,13 @@ let record_function_interface_type_constraints let fretvar = add_return_capability ftypevar in begin (match mk_btype_constraint fretvar returntype with - | Some tyc -> store#add_constraint tyc + | Some tyc -> + let _ = + log_diagnostics_result + ~tag:("function-interface type constraint") + __FILE__ __LINE__ + [faddr ^ ": " ^ (type_constraint_to_string tyc)] in + store#add_constraint tyc | _ -> ()); (match fargs with | None -> diff --git a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml index 8a133c37..6e19b373 100644 --- a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml +++ b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml @@ -152,6 +152,9 @@ object (self) method is_initialized: bool = grec.gloc_is_initialized + method is_function_address: bool = + BCHFunctionData.functions_data#is_function_entry_point self#address + method contains_address (addr: doubleword_int): bool = (self#address#equal addr) || (match self#size with diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 83148d7a..c2e4c4ad 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -4332,6 +4332,7 @@ class type global_location_int = method is_typed: bool method is_struct: bool method is_array: bool + method is_function_address: bool method initialvalue: globalvalue_t option method desc: string option method contains_address: doubleword_int -> bool diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintGraph.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintGraph.ml index a236281b..438efc49 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintGraph.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintGraph.ml @@ -56,7 +56,7 @@ object (self: 'a) Update for constraint of type (v, c) or (c, w), v in V, c in C: tvars'(w) = tvars(w) u {c}, tvreps' = tvreps if w = tvreps(v) - tvars'(w) = tvars(w), tvreps' = tvresp otherwise + tvars'(w) = tvars(w), tvreps' = tvreps otherwise Update for constraint of type (v1, v2), v1, v2 in V: diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml index 290457db..de873e80 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml @@ -437,7 +437,6 @@ object (self) method resolve_reglhs_type (reg: register_t) (faddr: string) (iaddr: string): btype_t option = let evaluation = self#evaluate_reglhs_type reg faddr iaddr in - let logresults = iaddr = "0xffffffff" in let log_evaluation () = log_diagnostics_result ~tag:("reglhs resolution not successfull for " ^ faddr) @@ -463,9 +462,17 @@ object (self) List.iter (fun (vars, consts) -> let jointy = type_constant_join consts in let _ = - if logresults then - log_result __FILE__ __LINE__ - ["jointy: " ^ (type_constant_to_string jointy)] in + log_diagnostics_result + ~tag:("result of type_constant_join for " ^ faddr) + __FILE__ __LINE__ + [iaddr + ^ ": jointy: " + ^ (type_constant_to_string jointy) + ^ " from " + ^ (p2s (pretty_print_list + consts + (fun c -> STR (type_constant_to_string c)) + "[" ", " "]"))] in List.iter (fun v -> let optty = match jointy with diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml index 189486fd..46cf7bfb 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml @@ -277,11 +277,6 @@ let mk_global_variable_typevar (gaddr: string): type_variable_t = mk_type_basevar (GlobalVariableType gaddr) -let mk_reglhs_typevar (reg: register_t) (faddr: string) (iaddr: string) - : type_variable_t = - mk_type_basevar (RegisterLhsType (reg, faddr, iaddr)) - - let mk_localstack_lhs_typevar (off: int) (faddr: string) (iaddr: string) : type_variable_t = mk_type_basevar (LocalStackLhsType (off, faddr, iaddr)) @@ -356,6 +351,15 @@ let add_stack_address_capability (offset: int) (tv: type_variable_t) add_capability [FLocStackAddress offset] tv +let mk_reglhs_typevar (reg: register_t) (faddr: string) (iaddr: string) + : type_variable_t = + if iaddr = "init" then + let ftypevar = mk_function_typevar faddr in + add_freg_param_capability reg ftypevar + else + mk_type_basevar (RegisterLhsType (reg, faddr, iaddr)) + + let mk_cty_term (c: type_constant_t): type_term_t = TyConstant c diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 427a45c8..bce8e1cd 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_20250702" - ~date:"2025-07-02" + ~version:"0.6.0_20250714" + ~date:"2025-07-14" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index 287bc44a..50393138 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml @@ -76,6 +76,7 @@ object (self) instr#has_opcode_condition && (match instr#get_opcode with | Branch _ | BranchExchange _ -> false + | Compare _ | CompareNegative _ -> false | _ -> true) && (Option.is_none instr#is_in_aggregate) in begin diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml index e34627eb..66aada1e 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - 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 @@ -211,9 +211,9 @@ let cc_expr (* ---------------------------------------------------------- Compare --- *) - | (Compare (ACCAlways, x, y, _), ACCEqual) -> + | (Compare (_, x, y, _), ACCEqual) -> (XOp (XEq, [v x; v y]), [x; y]) - | (Compare (ACCAlways, x, y, _), ACCNotEqual) -> + | (Compare (_, x, y, _), ACCNotEqual) -> (XOp (XNe, [v x; v y]), [x; y]) (* Occasionally the compiler will generate a a carryset condition for @@ -292,19 +292,19 @@ let cc_expr (XOp (XLAnd, [XOp (XLt, [vu x; vu y]); XOp (XGe, [vu x; zero_constant_expr])]), [x; y]) - | (Compare (ACCAlways, x, y, _), ACCUnsignedHigher) -> + | (Compare (_, x, y, _), ACCUnsignedHigher) -> (XOp (XGt, [vu x; vu y]), [x; y]) - | (Compare (ACCAlways, x, y, _), ACCNotUnsignedHigher) -> + | (Compare (_, x, y, _), ACCNotUnsignedHigher) -> (XOp (XLe, [vu x; vu y]), [x; y]) - | (Compare (ACCAlways, x, y, _), ACCSignedGE) -> + | (Compare (_, x, y, _), ACCSignedGE) -> (XOp (XGe, [v x; v y]), [x; y]) - | (Compare (ACCAlways, x, y, _), ACCSignedLT) -> + | (Compare (_, x, y, _), ACCSignedLT) -> (XOp (XLt, [v x; v y]), [x; y]) - | (Compare (ACCAlways, x, y, _), ACCSignedLE) -> + | (Compare (_, x, y, _), ACCSignedLE) -> (XOp (XLe, [v x; v y]), [x; y]) - | (Compare (ACCAlways, x, y, _), ACCSignedGT) -> + | (Compare (_, x, y, _), ACCSignedGT) -> (XOp (XGt, [v x; v y]), [x; y]) | (LogicalShiftLeft (true, ACCAlways, _, x, y, _), ACCNonNegative) -> @@ -315,7 +315,7 @@ let cc_expr | (CompareNegative (ACCAlways, x, y), ACCEqual) -> (XOp (XEq, [XOp (XPlus, [v x; v y]); zero_constant_expr]), [x; y]) - | (CompareNegative (ACCAlways, x, y), ACCNotEqual) -> + | (CompareNegative (_, x, y), ACCNotEqual) -> (XOp (XNe, [XOp (XPlus, [v x; v y]); zero_constant_expr]), [x; y]) | (CompareNegative (ACCAlways, x, y), ACCCarrySet) -> @@ -516,4 +516,16 @@ let arm_conditional_conditional_expr condfloc#set_test_expr xpr; (frozenVars#toList, Some xpr, opsused) end - | _ -> (frozenVars#toList, None, opsused) + | _ -> + let _ = + if collect_diagnostics () then + ch_diagnostics_log#add + "unused conditional condition expression" + (LBLOCK [ + STR (arm_opcode_to_string condopc); + STR "; "; + STR (arm_opcode_to_string testopc); + STR "; "; + STR (arm_opcode_to_string testtestopc) + ]) in + (frozenVars#toList, None, opsused) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 209d76f7..1eb32fe4 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -1128,8 +1128,10 @@ object (self) let txpr = floc#get_test_expr in let fxpr = simplify_xpr (XOp (XLNot, [txpr])) in let csetter = floc#f#get_associated_cc_setter floc#cia in - let tcond = rewrite_test_expr csetter txpr in - let fcond = rewrite_test_expr csetter fxpr in + (* we can rewrite with invariants at this address, since the expression + should have been made position independent for local variables.*) + let tcond = rewrite_expr txpr in + let fcond = rewrite_expr fxpr in let ctcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) tcond in let cfcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) fcond in let csetter_addr_r = string_to_doubleword csetter in @@ -2193,6 +2195,7 @@ object (self) let vrd_r = rd#to_variable floc in let xrm_r = rm#to_expr floc in let result_r = TR.tmap (rewrite_expr ?restrict:(Some 4)) xrm_r in + let result_r = TR.tmap (rewrite_in_cc_context floc c) result_r in let cresult_r = TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) result_r in let rdefs = (get_rdef_r xrm_r) :: (get_all_rdefs_r result_r) in diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index dfabde71..ea2d71c1 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -36,6 +36,7 @@ open CHTraceResult (* xprlib *) open XprTypes +open XprUtil open Xsimplify (* bchlib *) @@ -255,6 +256,43 @@ object (self) linenumber [(p2s floc#l#toPretty) ^ ": " ^ (btype_to_string ty)] in + let operand_is_zero (op: arm_operand_int): bool = + (* Returns true if the value of the operand is known to be zero at + this location. This result is primarily intended to avoid spurious + typing relationships in cases where the compiler 'knows' that the value + is zero, and may use it as an alternate for the the immediate value zero + in certain instructions, like ADD, MOV, or SUB. *) + TR.tfold_default + (fun v -> + match v with + | XConst (IntConst n) -> n#equal numerical_zero + | _ -> false) + false + (TR.tmap rewrite_expr (op#to_expr floc)) in + + let operand_is_zero_in_cc_context + (cc: arm_opcode_cc_t) (op: arm_operand_int): bool = + match cc with + | ACCAlways -> operand_is_zero op + | _ when instr#is_condition_covered -> operand_is_zero op + | _ when is_cond_conditional cc && floc#has_test_expr -> + TR.tfold_default + (fun xx -> + let txpr = floc#get_test_expr in + let tcond = rewrite_expr txpr in + (match tcond with + | XOp (XEq, [XVar vr; XConst (IntConst n)]) -> + let subst v = + if v#equal vr then XConst (IntConst n) else XVar vr in + let result = simplify_xpr (substitute_expr subst xx) in + (match result with + | XConst (IntConst n) -> n#equal numerical_zero + | _ -> operand_is_zero op) + | _ -> operand_is_zero op)) + (operand_is_zero op) + (TR.tmap rewrite_expr (op#to_expr floc)) + | _ -> operand_is_zero op in + match instr#get_opcode with | Add (_, _, rd, rn, rm, _) -> @@ -275,7 +313,26 @@ object (self) | _ -> ()) | _ -> ()); - (if rm#is_immediate && (rm#to_numerical#toInt < 256) then + (* Heuristic: if a small number (taken here as < 256) is added to + a register value it is assumed that the value in the destination + register has the same type as the value in the source register. + + The case where the value of the source register is known to be zero + is excluded, because this construct, rd = rn (=0) + imm, is often + used as an alternate for MOV rd, #imm, in which case the type of + the source value may be entirely related to the type of the type of + the destination value (giving rise to very hard to diagnose typing + errors) + + This heuristic also fails when applied to pointers to access + different fields in a struct. Although this case is not so common, + (ARM allows offsets to be specified as part of memory accesses), + it does happen (it has been observed), and hence this heuristic + is disabled for now, until we have a way to explicitly exclude + this case. + (if rm#is_immediate + && (rm#to_numerical#toInt < 256) + && (not (operand_is_zero rn)) then let rdreg = rd#to_register in let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let rndefs = get_variable_rdefs_r (rn#to_variable floc) in @@ -288,7 +345,7 @@ object (self) begin log_subtype_constraint __LINE__ "ADD-imm" rntypeterm lhstypeterm; store#add_subtype_constraint rntypeterm lhstypeterm - end) rndefs); + end) rndefs); *) (match getopt_global_address_r (rn#to_expr floc) with | Some gaddr -> @@ -389,7 +446,19 @@ object (self) begin log_subtype_constraint __LINE__ "MVN" tctypeterm lhstypeterm; store#add_subtype_constraint tctypeterm lhstypeterm - end) + end); + + (* propagate function return type *) + (if rd#get_register = AR0 && (has_exit_use_r (rd#to_variable floc)) then + let regvar = mk_reglhs_typevar rdreg faddr iaddr in + let fvar = mk_function_typevar faddr in + let fvar = add_return_capability fvar in + let regterm = mk_vty_term regvar in + let fterm = mk_vty_term fvar in + begin + log_subtype_constraint __LINE__ "MVN-freturn" regterm fterm; + store#add_subtype_constraint regterm fterm + end); end @@ -399,15 +468,28 @@ object (self) let rmdefs = get_variable_rdefs_r (rm#to_variable floc) in let rmreg = rm#to_register in begin - List.iter (fun rmsym -> - let rmaddr = rmsym#getBaseName in - let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in - let rmtypeterm = mk_vty_term rmtypevar in - let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint __LINE__ "MVN-rdef" rmtypeterm lhstypeterm; - store#add_subtype_constraint rmtypeterm lhstypeterm - end) rmdefs + (List.iter (fun rmsym -> + let rmaddr = rmsym#getBaseName in + let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in + let rmtypeterm = mk_vty_term rmtypevar in + let lhstypeterm = mk_vty_term lhstypevar in + begin + log_subtype_constraint __LINE__ "MVN-rdef" rmtypeterm lhstypeterm; + store#add_subtype_constraint rmtypeterm lhstypeterm + end) rmdefs); + + (* propagate function return type *) + (if rd#get_register = AR0 && (has_exit_use_r (rd#to_variable floc)) then + let regvar = mk_reglhs_typevar rdreg faddr iaddr in + let fvar = mk_function_typevar faddr in + let fvar = add_return_capability fvar in + let regterm = mk_vty_term regvar in + let fterm = mk_vty_term fvar in + begin + log_subtype_constraint __LINE__ "MVN-freturn" regterm fterm; + store#add_subtype_constraint regterm fterm + end); + end | BitwiseOr (_, _, rd, rn, _, _) -> @@ -962,6 +1044,7 @@ object (self) store#add_subtype_constraint tctypeterm rntypeterm end) rndefs) + (* | LogicalShiftRight (_, _, rd, rn, rm, _) when rm#is_immediate -> let rdreg = rd#to_register in let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in @@ -988,29 +1071,45 @@ object (self) log_subtype_constraint __LINE__ "LSR-rhs" tctypeterm rntypeterm; store#add_subtype_constraint tctypeterm rntypeterm end) rndefs) - + *) | Move (_, _, rd, rm, _, _) when rm#is_immediate -> - let rmval = rm#to_numerical#toInt in - (* 0 provides no information about the type *) - if rmval = 0 then - () - else - let rdreg = rd#to_register in - let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in - let tyc = get_intvalue_type_constant rmval in - let lhstypeterm = mk_vty_term lhstypevar in - let tctypeterm = mk_cty_term tyc in - begin - log_subtype_constraint __LINE__ "MOV-imm" tctypeterm lhstypeterm; - store#add_subtype_constraint tctypeterm lhstypeterm - end + let rdreg = rd#to_register in + let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in + begin + + (* variable introduction for lhs with type *) + (match get_regvar_type_annotation () with + | Some t -> + let opttc = mk_btype_constraint lhstypevar t in + (match opttc with + | Some tc -> + begin + log_type_constraint __LINE__ "MOV-rvintro" tc; + store#add_constraint tc + end + | _ -> ()) + | _ -> ()); + + (let rmval = rm#to_numerical#toInt in + (* 0 provides no information about the type *) + if rmval = 0 then + () + else + let tyc = get_intvalue_type_constant rmval in + let lhstypeterm = mk_vty_term lhstypevar in + let tctypeterm = mk_cty_term tyc in + begin + log_subtype_constraint __LINE__ "MOV-imm" tctypeterm lhstypeterm; + store#add_subtype_constraint tctypeterm lhstypeterm + end) + end | Move (_, _, rd, rm, _, _) when rd#get_register = rm#get_register -> (* exclude to avoid spurious rdefs to get involved *) () (* Move x, y --- x := y --- Y <: X *) - | Move (_, _, rd, rm, _, _) when rm#is_register -> + | Move (_, c, rd, rm, _, _) when rm#is_register -> let xrm_r = rm#to_expr floc in let rdreg = rd#to_register in let rdtypevar = mk_reglhs_typevar rdreg faddr iaddr in @@ -1058,19 +1157,28 @@ object (self) (* use reaching defs *) (let rmreg = rm#to_register in - let rmvar_r = rm#to_variable floc in - let rmrdefs = get_variable_rdefs_r rmvar_r in - let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in - List.iter (fun rmrdef -> - let rmaddr = rmrdef#getBaseName in - if rmaddr != "init" then - let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in - let rmtypeterm = mk_vty_term rmtypevar in - let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint __LINE__ "MOV-reg" rmtypeterm lhstypeterm; - store#add_subtype_constraint rmtypeterm lhstypeterm - end) rmrdefs) + if operand_is_zero_in_cc_context c rm then + (* This case is excluded, because the move from a register + that contains zero can be done as a substitute for the + move of an immediate value, without any relationships in + types between the source and destination register. It is + often used by compilers as a convenience, if the register + is known to have the value zero at this point. *) + () + else + let rmvar_r = rm#to_variable floc in + let rmrdefs = get_variable_rdefs_r rmvar_r in + let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in + List.iter (fun rmrdef -> + let rmaddr = rmrdef#getBaseName in + if rmaddr != "init" then + let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in + let rmtypeterm = mk_vty_term rmtypevar in + let lhstypeterm = mk_vty_term lhstypevar in + begin + log_subtype_constraint __LINE__ "MOV-reg" rmtypeterm lhstypeterm; + store#add_subtype_constraint rmtypeterm lhstypeterm + end) rmrdefs) end | Pop (_, _, rl, _) when rl#includes_pc -> @@ -1283,7 +1391,7 @@ object (self) end - | Subtract (_, _, rd, rn, _, _, _) -> + | Subtract (_, _, rd, rn, rm, _, _) -> let rdreg = rd#to_register in let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let rndefs = get_variable_rdefs_r (rn#to_variable floc) in @@ -1292,15 +1400,19 @@ object (self) (* Note: Does not take into consideration the possibility of the subtraction of two pointers *) - List.iter (fun rnsym -> - let rnaddr = rnsym#getBaseName in - let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in - let rntypeterm = mk_vty_term rntypevar in - let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint __LINE__ "SUB-rdef-1" rntypeterm lhstypeterm; - store#add_subtype_constraint rntypeterm lhstypeterm - end) rndefs; + (if rm#is_immediate && (rm#to_numerical#toInt = 0) then + () + else + List.iter (fun rnsym -> + let rnaddr = rnsym#getBaseName in + let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in + let rntypeterm = mk_vty_term rntypevar in + let lhstypeterm = mk_vty_term lhstypevar in + begin + log_subtype_constraint + __LINE__ "SUB-rdef-1" rntypeterm lhstypeterm; + store#add_subtype_constraint rntypeterm lhstypeterm + end) rndefs); (* propagate function return type *) (if rd#get_register = AR0 && (has_exit_use_r (rd#to_variable floc)) then diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 43eafc82..52465e0e 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -4626,8 +4626,13 @@ object (self) (["defusehigh"], {op_name = new symbol_t ~atts:["exit"] "use_high"; op_args = [("dst", v, WRITE)]})) symvars in + let exitname = new symbol_t ~atts:["exit"] "invariant" in + let cmdinvop = OPERATION {op_name = exitname; op_args = []} in let constantAssigns = env#end_transaction in - let cmds = constantAssigns @ cmds @ cmdshigh in + let cmds = constantAssigns @ [cmdinvop] @ cmds @ cmdshigh in + let returnvar = finfo#env#mk_arm_register_variable AR0 in + let _ = finfo#add_use_loc returnvar "exit" in + let _ = finfo#add_use_high_loc returnvar "exit" in TRANSACTION (new symbol_t "exit", LF.mkCode cmds, None) method translate = diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml index df0fcc82..5b6766f2 100644 --- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml @@ -73,7 +73,7 @@ let codemax = make_dw "0x400000" let translate_store () = let tests = [ ("PUSHLR", "0x1b960", "04e02de500", - [("var_0004", "LR_in"); ("SP", "sv__5__sv")]); + [("var_0004", "LR_in"); ("SP", "sv__3__sv")]); ("PUSHR0_3", "0x19470", "0f002de900", [("var_0016", "R0_in"); ("var_0012", "R1_in");