diff --git a/CodeHawk/CH/xprlib/xsimplify.ml b/CodeHawk/CH/xprlib/xsimplify.ml index aafce4b9..af1b4830 100644 --- a/CodeHawk/CH/xprlib/xsimplify.ml +++ b/CodeHawk/CH/xprlib/xsimplify.ml @@ -1040,6 +1040,10 @@ and reduce_ne m e1 e2 = (* (a - b) != 0 ===> a != b *) | (XOp (XMinus, [x; y]), SConst a) when zero_num a -> (true, XOp (XNe, [x; y])) + (* (a + b) != 0 ====> a != -b *) + | (XOp (XPlus, [x; y]), SConst a) when zero_num a -> + (true, XOp (XNe, [x; (XOp (XNeg, [y]))])) + | _ -> default diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index ea077427..c11a85e1 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -1259,6 +1259,10 @@ object (self) memref_r memoff_r method private get_variable_type (v: variable_t): btype_t traceresult = + let is_zero (x: xpr_t) = + match x with + | XConst (IntConst n) -> n#equal numerical_zero + | _ -> false in if self#f#env#is_initial_register_value v then let reg_r = self#f#env#get_initial_register_value_register v in TR.tbind @@ -1348,6 +1352,43 @@ object (self) let cinfo = get_compinfo_by_key ckey in let finfo = get_compinfo_field cinfo fname in Ok finfo.bftype + | IndexOffset (v, i, memsuboff) -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "index offset: " + ^ (memory_offset_to_string memoff) + ^ " with " + ^ (p2s v#toPretty) + ^ ", index: " + ^ (string_of_int i) + ^ "; and " + ^ (memory_offset_to_string memsuboff)] + | ArrayIndexOffset (x, memsuboff) -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "array index offset: " + ^ (memory_offset_to_string memoff) + ^ " with " + ^ (x2s x) + ^ "; and " + ^ (memory_offset_to_string memsuboff)] + | BasePtrArrayIndexOffset (x, _) when is_zero x -> + (match basevartype with + | TPtr (t, _) -> Ok t + | _ -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "array index offset: " + ^ (memory_offset_to_string memoff) + ^ " with basevar type: " + ^ (btype_to_string basevartype) + ^ " not yet handled"]) + | BasePtrArrayIndexOffset (x, memsuboff) -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "base-ptr array index offset: " + ^ (memory_offset_to_string memoff) + ^ " with " + ^ (x2s x) + ^ "; and " + ^ (memory_offset_to_string memsuboff)] + | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "memoff: " ^ (memory_offset_to_string memoff) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionData.ml b/CodeHawk/CHB/bchlib/bCHFunctionData.ml index 44b0cf74..ba771042 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionData.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionData.ml @@ -280,6 +280,32 @@ object (self) __FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "No stackvar annotation found at offset " ^ (string_of_int offset)] + method is_typing_rule_enabled (loc: string) (name: string): bool = + match self#get_function_annotation with + | None -> false + | Some a -> + List.fold_left + (fun acc tra -> + acc || + (if tra.tra_action = "enable" && tra.tra_name = name then + (List.mem "all" tra.tra_locations) + || (List.mem loc tra.tra_locations) + else + false)) false a.typingrules + + method is_typing_rule_disabled (loc: string) (name: string): bool = + match self#get_function_annotation with + | None -> false + | Some a -> + List.fold_left + (fun acc tra -> + acc || + (if tra.tra_action = "disable" && tra.tra_name = name then + (List.mem "all" tra.tra_locations) + || (List.mem loc tra.tra_locations) + else + false)) false a.typingrules + method add_inlined_block (baddr:doubleword_int) = inlined_blocks <- baddr :: inlined_blocks @@ -592,6 +618,25 @@ let read_xml_stackvar_intro (node: xml_element_int): stackvar_intro_t traceresul svi_cast = svi_cast} +let read_xml_typing_rule (node: xml_element_int): typing_rule_t traceresult = + let get = node#getAttribute in + let has = node#hasNamedAttribute in + if not (has "name") then + Error ["typingrule without name"] + else if not (has "locs") then + Error ["typingrule without location"] + else if not (has "action") then + Error ["typingrule without action"] + else + let name = get "name" in + let action = get "action" in + let locs = get "locs" in + let locs = String.split_on_char ',' locs in + Ok {tra_name = name; + tra_action = action; + tra_locations = locs} + + let read_xml_function_annotation (node: xml_element_int) = let get = node#getAttribute in let getc = node#getTaggedChild in @@ -635,8 +680,27 @@ let read_xml_function_annotation (node: xml_element_int) = (rvintros#getTaggedChildren "vintro") else [] in + let typingrules = + if hasc "typing-rules" then + let trules = getc "typing-rules" in + List.fold_left + (fun acc n -> + TR.tfold + ~ok:(fun tr -> tr :: acc) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ e; + acc + end) + (read_xml_typing_rule n)) + [] + (trules#getTaggedChildren "typingrule") + else + [] in fndata#set_function_annotation - {regvarintros = regvintros; stackvarintros = stackvintros} + {regvarintros = regvintros; + stackvarintros = stackvintros; + typingrules = typingrules} else log_error_result ~tag:"function annotation faddr not found" diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml index b6ac0258..181c523a 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml @@ -1139,7 +1139,7 @@ let record_function_interface_type_constraints ~tag:("function-interface type constraint") __FILE__ __LINE__ [faddr ^ ": " ^ (type_constraint_to_string tyc)] in - store#add_constraint tyc + store#add_constraint faddr "exit" "INTF-freturn" tyc | _ -> ()); (match fargs with | None -> @@ -1160,7 +1160,7 @@ let record_function_interface_type_constraints ~tag:("function-interface type constraint") __FILE__ __LINE__ [faddr ^ ": " ^ (type_constraint_to_string tyc)] in - store#add_constraint tyc + store#add_constraint faddr "init" "INTF-fparam" tyc | _ -> chlog#add "function interface type constraints" diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index c2e4c4ad..45a4d6b9 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1511,10 +1511,17 @@ type stackvar_intro_t = { svi_cast: bool } +type typing_rule_t = { + tra_action: string; + tra_name: string; + tra_locations: string list + } + type function_annotation_t = { regvarintros: regvar_intro_t list; - stackvarintros: stackvar_intro_t list + stackvarintros: stackvar_intro_t list; + typingrules: typing_rule_t list } class type function_data_int = @@ -1567,6 +1574,8 @@ class type function_data_int = method has_regvar_type_cast: doubleword_int -> bool method has_stackvar_type_annotation: int -> bool method has_stackvar_type_cast: int -> bool + method is_typing_rule_enabled: string -> string -> bool + method is_typing_rule_disabled: string -> string -> bool method has_class_info: bool method has_callsites: bool method has_path_contexts: bool @@ -3188,6 +3197,14 @@ type type_constraint_t = | TyZeroCheck of type_term_t +type type_inference_rule_application_t = { + tir_faddr: string; + tir_loc: string; + tir_rule: string; + tir_constraint_ix: int + } + + class type type_constraint_dictionary_int = object @@ -3246,17 +3263,21 @@ class type type_constraint_store_int = method reset: unit - method add_constraint: type_constraint_t -> unit + method add_constraint: + string -> string -> string -> type_constraint_t -> unit - method add_var_constraint: type_variable_t -> unit + method add_var_constraint: + string -> string -> string -> type_variable_t -> unit - method add_term_constraint: type_term_t -> unit + method add_term_constraint: + string -> string -> string -> type_term_t -> unit - method add_zerocheck_constraint: type_variable_t -> unit + (* method add_zerocheck_constraint: type_variable_t -> unit *) - method add_subtype_constraint: type_term_t -> type_term_t -> unit + method add_subtype_constraint: + string -> string -> string -> type_term_t -> type_term_t -> unit - method add_ground_constraint: type_term_t -> type_term_t -> unit + (* method add_ground_constraint: type_term_t -> type_term_t -> unit *) method get_function_type_constraints: string -> type_constraint_t list @@ -3287,6 +3308,8 @@ class type type_constraint_store_int = method resolve_local_stack_lhs_types: string -> (int * btype_t option) list + method write_xml: xml_element_int -> unit + method toPretty: pretty_t end diff --git a/CodeHawk/CHB/bchlib/bCHPreFileIO.ml b/CodeHawk/CHB/bchlib/bCHPreFileIO.ml index 92529093..9d15ef26 100644 --- a/CodeHawk/CHB/bchlib/bCHPreFileIO.ml +++ b/CodeHawk/CHB/bchlib/bCHPreFileIO.ml @@ -439,6 +439,13 @@ let get_resultdata_filename () = Filename.concat fdir (exename ^ "_data.xml") +let get_typeconstraintstore_filename () = + let exename = get_filename () in + let fdir = get_results_dir () in + let _ = create_directory fdir in + Filename.concat fdir (exename ^ "_tcstore.xml") + + let get_x86dictionary_filename () = let exename = get_filename () in let fdir = get_results_dir () in @@ -657,6 +664,18 @@ let save_resultdata_file (node:xml_element_int) = file_output#saveFile filename doc#toPretty end + +let save_typeconstraintstore (node: xml_element_int) = + let filename = get_typeconstraintstore_filename () in + let doc = xmlDocument () in + let root = get_bch_root "type-constraint-store" in + begin + doc#setNode root; + root#appendChildren [node]; + file_output#saveFile filename doc#toPretty + end + + let save_cfgs (node:xml_element_int) = let filename = get_cfgs_filename () in let doc = xmlDocument () in diff --git a/CodeHawk/CHB/bchlib/bCHPreFileIO.mli b/CodeHawk/CHB/bchlib/bCHPreFileIO.mli index 5ea8b236..5a7eb3f0 100644 --- a/CodeHawk/CHB/bchlib/bCHPreFileIO.mli +++ b/CodeHawk/CHB/bchlib/bCHPreFileIO.mli @@ -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 @@ -117,7 +117,8 @@ val save_userdata_function_summary_file: string -> xml_element_int -> unit val save_userdata_function_summaries_file: xml_element_int -> unit val load_export_ordinal_table: string -> xml_element_int option -val save_resultdata_file : xml_element_int -> unit +val save_resultdata_file: xml_element_int -> unit +val save_typeconstraintstore: xml_element_int -> unit val save_cfgs: xml_element_int -> unit val save_executable_dump: xml_element_int -> unit diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml index de873e80..e8e1f252 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml @@ -31,6 +31,7 @@ open CHUtils (* chutil *) open CHLogger +open CHXmlDocument (* bchlib *) open BCHBCTypePretty @@ -72,6 +73,8 @@ object (self) (* constraints that involve a global variable *) val gvartypes = H.create 5 + val rules_applied = H.create 5 + method reset = begin H.clear store; @@ -81,9 +84,28 @@ object (self) H.clear gvartypes end - method add_constraint (c: type_constraint_t) = + method private add_rule_applied + (faddr: string) + (loc: string) + (rule: string) + (ix: int) = + let tir = { + tir_faddr = faddr; + tir_loc = loc; + tir_rule = rule; + tir_constraint_ix = ix + } in + let entry = + if H.mem rules_applied faddr then + H.find rules_applied faddr + else + [] in + H.replace rules_applied faddr (tir :: entry) + + method add_constraint + (faddr: string) (loc: string) (rule: string) (c: type_constraint_t) = let index = tcd#index_type_constraint c in - (* index the constraint *) + let _ = self#add_rule_applied faddr loc rule index in if H.mem store index then () else @@ -188,33 +210,50 @@ object (self) if H.mem iaddrentry iaddr then H.find iaddrentry iaddr else [] in H.replace iaddrentry iaddr (c :: entry) - method add_var_constraint (tyvar: type_variable_t) = - self#add_constraint (TyVar (TyVariable tyvar)) + method add_var_constraint + (faddr: string) + (loc: string) + (rule: string) + (tyvar: type_variable_t) = + self#add_constraint faddr loc rule (TyVar (TyVariable tyvar)) - method add_term_constraint (t: type_term_t) = + method add_term_constraint + (faddr: string) + (loc: string) + (rule: string) + (t: type_term_t) = match t with - | TyVariable tv -> self#add_var_constraint tv + | TyVariable tv -> self#add_var_constraint faddr loc rule tv | _ -> () + (* method add_zerocheck_constraint (tyvar: type_variable_t) = begin self#add_var_constraint tyvar; self#add_constraint (TyZeroCheck (TyVariable tyvar)) end + *) - method add_subtype_constraint (t1: type_term_t) (t2: type_term_t) = + method add_subtype_constraint + (faddr: string) + (loc: string) + (rule: string) + (t1: type_term_t) + (t2: type_term_t) = begin - self#add_term_constraint t1; - self#add_term_constraint t2; - self#add_constraint (TySub (t1, t2)) + self#add_term_constraint faddr loc rule t1; + self#add_term_constraint faddr loc rule t2; + self#add_constraint faddr loc rule (TySub (t1, t2)) end + (* method add_ground_constraint (t1: type_term_t) (t2: type_term_t) = begin self#add_term_constraint t1; self#add_term_constraint t2; self#add_constraint (TyGround (t1, t2)) end + *) method get_function_type_constraints (faddr: string): type_constraint_t list = if H.mem functiontypes faddr then @@ -704,6 +743,31 @@ object (self) () in !result + method private write_xml_rules_applied (node: xml_element_int) = + let ranode = xmlElement "rules-applied" in + begin + H.iter (fun faddr rules -> + let fnode = xmlElement "function" in + let _ = fnode#setAttribute "faddr" faddr in + begin + List.iter (fun rule -> + let rnode = xmlElement "rule" in + begin + rnode#setAttribute "loc" rule.tir_loc; + rnode#setAttribute "rule" rule.tir_rule; + rnode#setIntAttribute "tc-ix" rule.tir_constraint_ix; + fnode#appendChildren [rnode] + end) rules; + ranode#appendChildren [fnode] + end) rules_applied; + node#appendChildren [ranode] + end + + method write_xml (node: xml_element_int) = + begin + self#write_xml_rules_applied (node) + end + method toPretty = let constraints = ref [] in let _ = diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index bce8e1cd..9fdb09da 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_20250714" - ~date:"2025-07-14" + ~version:"0.6.0_20250722" + ~date:"2025-07-22" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index 50393138..cb8504f8 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml @@ -304,8 +304,7 @@ object (self) save_vars faddr vard end ); (* (if save then fndata#save); *) - H.add table fn#get_address#to_hex_string fn; - typeconstraints#record_type_constraints; + H.add table fn#get_address#to_hex_string fn end method write_xml (node:xml_element_int) = @@ -325,9 +324,12 @@ object (self) method save = let node = xmlElement "application-results" in + let tcnode = xmlElement "type-constraint-store" in begin self#write_xml node; - save_resultdata_file node + save_resultdata_file node; + typeconstraintstore#write_xml tcnode; + save_typeconstraintstore tcnode end end diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml index 352c77c0..89627ef5 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml @@ -735,6 +735,9 @@ object (self:'a) method is_pc_register = match kind with ARMReg ARPC -> true | _ -> false + method is_sp_register = + match kind with ARMReg ARSP -> true | _ -> false + method is_double_register = match kind with ARMDoubleReg _ -> true | _ -> false diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli b/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli index 6a0d4330..e6bd0452 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli @@ -202,6 +202,7 @@ class type arm_operand_int = method is_register: bool method is_shifted_register: bool method is_pc_register: bool + method is_sp_register: bool method is_double_register: bool method is_extension_register: bool method is_double_extension_register: bool diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 1eb32fe4..28ba89a6 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -2385,6 +2385,7 @@ object (self) let r0_op = arm_register_op AR0 RD in let xr0_r = r0_op#to_expr floc in let xxr0_r = TR.tmap rewrite_expr xr0_r in + let xxr0_r = TR.tmap (rewrite_in_cc_context floc c) xxr0_r in let cxr0_r = TR.tbind floc#convert_xpr_to_c_expr xxr0_r in add_return_value tags args xr0_r xxr0_r cxr0_r else diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index ea2d71c1..64f69a91 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -256,6 +256,24 @@ object (self) linenumber [(p2s floc#l#toPretty) ^ ": " ^ (btype_to_string ty)] in + let log_subtype_rule_disabled + (linenumber: int) (name: string) (ty1: type_term_t) (ty2: type_term_t) = + log_diagnostics_result + ~tag:("typing rule " ^ name ^ " disabled") + __FILE__ + linenumber + [(p2s floc#l#toPretty) ^ ": " + ^ (type_term_to_string ty1) + ^ " <: " + ^ (type_term_to_string ty2)] in + + let _log_rule_enabled (linenumber: int) (name: string) = + log_diagnostics_result + ~tag:("typing rule " ^ name ^ " enabled") + __FILE__ + linenumber + [(p2s floc#l#toPretty)] 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 @@ -293,25 +311,51 @@ object (self) (TR.tmap rewrite_expr (op#to_expr floc)) | _ -> operand_is_zero op in - match instr#get_opcode with - - | Add (_, _, rd, rn, rm, _) -> - let xrn_r = rn#to_expr floc in - begin - - (match get_regvar_type_annotation () with - | Some t -> - let rdreg = rd#to_register in - let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in - let opttc = mk_btype_constraint lhstypevar t in + let regvar_type_introduction (mnem: string) (op: arm_operand_int) = + if op#is_register then + (match get_regvar_type_annotation () with + | Some t -> + let reg = op#to_register in + let tv_z = mk_reglhs_typevar reg faddr iaddr in + let opttc = mk_btype_constraint tv_z t in + let rule = mnem ^ "-rvintro" in (match opttc with | Some tc -> begin - log_type_constraint __LINE__ "ADD-rvintro" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> ()) - | _ -> ()); + | _ -> ()) + else + ch_error_log#add + "regvar-type-introduction" + (LBLOCK [STR faddr; STR ":"; STR iaddr; STR ": "; + op#toPretty; STR " is not a register"]) in + + let regvar_linked_to_exit (mnem: string) (op: arm_operand_int) = + if op#is_register then + (if op#get_register = AR0 && (has_exit_use_r (op#to_variable floc)) then + let reg = op#to_register in + let tv_z = mk_reglhs_typevar reg faddr iaddr in + let fvar = add_return_capability (mk_function_typevar faddr) in + let tt_z = mk_vty_term tv_z in + let fterm = mk_vty_term fvar in + let rule = mnem ^ "-freturn" in + begin + log_subtype_constraint __LINE__ rule tt_z fterm; + store#add_subtype_constraint faddr iaddr rule tt_z fterm + end) + else + () in + + match instr#get_opcode with + + | Add (_, _, rd, rn, rm, _) -> + let xrn_r = rn#to_expr floc in + begin + (regvar_type_introduction "ADD" rd); + (regvar_linked_to_exit "ADD" rd); (* Heuristic: if a small number (taken here as < 256) is added to a register value it is assumed that the value in the destination @@ -320,7 +364,7 @@ object (self) 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 source value may be entirely unrelated to the type of the destination value (giving rise to very hard to diagnose typing errors) @@ -329,7 +373,7 @@ object (self) (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. + this case.*) (if rm#is_immediate && (rm#to_numerical#toInt < 256) && (not (operand_is_zero rn)) then @@ -342,14 +386,19 @@ object (self) 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__ "ADD-imm" rntypeterm lhstypeterm; - store#add_subtype_constraint rntypeterm lhstypeterm - end) rndefs); *) + let rule = "ADD-c" in + if fndata#is_typing_rule_disabled iaddr rule then + log_subtype_rule_disabled __LINE__ rule rntypeterm lhstypeterm + else + begin + log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule rntypeterm lhstypeterm + end) rndefs); (match getopt_global_address_r (rn#to_expr floc) with | Some gaddr -> - if BCHConstantDefinitions.is_in_global_arrayvar gaddr then + if rm#is_register + && BCHConstantDefinitions.is_in_global_arrayvar gaddr then (match (BCHConstantDefinitions.get_arrayvar_base_offset gaddr) with | Some _ -> let rmdefs = get_variable_rdefs_r (rm#to_variable floc) in @@ -360,10 +409,12 @@ object (self) let tyc = mk_int_type_constant Unsigned 32 in let rmtypeterm = mk_vty_term rmtypevar in let ctypeterm = mk_cty_term tyc in + let rule = "ADD-global" in begin log_subtype_constraint - __LINE__ "ADD-global" rmtypeterm ctypeterm; - store#add_subtype_constraint rmtypeterm ctypeterm + __LINE__ rule rmtypeterm ctypeterm; + store#add_subtype_constraint + faddr iaddr rule rmtypeterm ctypeterm end) rmdefs | _ -> ()) else @@ -378,10 +429,10 @@ object (self) let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let fttypeterm = mk_vty_term ftvar in let lhstypeterm = mk_vty_term lhstypevar in + let rule = "ADD-initv" in begin - log_subtype_constraint - __LINE__ "ADD-lhs-init" fttypeterm lhstypeterm; - store#add_subtype_constraint fttypeterm lhstypeterm + log_subtype_constraint __LINE__ rule fttypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule fttypeterm lhstypeterm end | _ -> ()) end @@ -392,14 +443,17 @@ object (self) let rnreg = rn#to_register in let rndefs = get_variable_rdefs_r (rn#to_variable floc) in begin + (regvar_type_introduction "ASR" rd); + (regvar_linked_to_exit "ASR" rd); (* ASR results in a signed integer *) (let tc = mk_int_type_constant Signed 32 in let tctypeterm = mk_cty_term tc in let lhstypeterm = mk_vty_term lhstypevar in + let rule = "ASR-lhs-default" in begin - log_subtype_constraint __LINE__ "ASR-lhs" tctypeterm lhstypeterm; - store#add_subtype_constraint tctypeterm lhstypeterm + log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm end); (* ASR is applied to a signed integer *) @@ -409,9 +463,10 @@ object (self) let tyc = mk_int_type_constant Signed 32 in let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in + let rule = "ASR-rdef" in begin - log_subtype_constraint __LINE__ "ASR-rhs" tctypeterm rntypeterm; - store#add_subtype_constraint tctypeterm rntypeterm + log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rntypeterm end) rndefs) end @@ -421,15 +476,18 @@ object (self) let rndefs = get_variable_rdefs_r (rn#to_variable floc) in let rnreg = rn#to_register in begin + (regvar_type_introduction "AND" rd); + (regvar_linked_to_exit "AND" rd); 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 + let rule = "AND-rdef" in begin - log_subtype_constraint __LINE__ "AND-rdef-1" rntypeterm lhstypeterm; - store#add_subtype_constraint rntypeterm lhstypeterm + log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule rntypeterm lhstypeterm end) rndefs end @@ -439,27 +497,17 @@ object (self) let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let tyc = get_intvalue_type_constant rmval in begin + (regvar_type_introduction "MVN" rd); + (regvar_linked_to_exit "MVN" rd); (* destination is an integer type *) (let tctypeterm = mk_cty_term tyc in let lhstypeterm = mk_vty_term lhstypevar in + let rule = "MVN-default" in begin - log_subtype_constraint __LINE__ "MVN" tctypeterm lhstypeterm; - store#add_subtype_constraint tctypeterm lhstypeterm + log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm 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 | BitwiseNot (_, _, rd, rm, _) -> @@ -468,28 +516,20 @@ object (self) let rmdefs = get_variable_rdefs_r (rm#to_variable floc) in let rmreg = rm#to_register in begin + (regvar_type_introduction "MVN" rd); + (regvar_linked_to_exit "MVN" rd); + (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 + let rule = "MVN-rdef" in begin - log_subtype_constraint __LINE__ "MVN-rdef" rmtypeterm lhstypeterm; - store#add_subtype_constraint rmtypeterm lhstypeterm + log_subtype_constraint __LINE__ rule rmtypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule 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, _, _) -> @@ -498,15 +538,18 @@ object (self) let rndefs = get_variable_rdefs_r (rn#to_variable floc) in let rnreg = rn#to_register in begin + (regvar_type_introduction "ORR" rd); + (regvar_linked_to_exit "ORR" rd); 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 + let rule = "ORR-rdef" in begin - log_subtype_constraint __LINE__ "AND-rdef-1" rntypeterm lhstypeterm; - store#add_subtype_constraint rntypeterm lhstypeterm + log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule rntypeterm lhstypeterm end) rndefs end @@ -545,28 +588,30 @@ object (self) match get_regvar_type_annotation () with | Some t -> let opttc = mk_btype_constraint typevar t in + let rule = "BL-rvintro" in (match opttc with | Some tc -> begin - log_type_constraint __LINE__ "BL-rv-intro" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> begin - log_no_type_constraint __LINE__ "BL-rv-intro" t; + log_no_type_constraint __LINE__ rule t; () end) | _ -> let opttc = mk_btype_constraint typevar rtype in + let rule = "BL-rv" in match opttc with | Some tc -> begin - log_type_constraint __LINE__ "BL-rv" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> begin - log_no_type_constraint __LINE__ "BL-rv" rtype; + log_no_type_constraint __LINE__ rule rtype; () end); @@ -583,21 +628,23 @@ object (self) let typevar = mk_reglhs_typevar regarg faddr rdsym#getBaseName in let opttc = mk_btype_constraint typevar ptype in + let rule = "BL-regarg" in match opttc with | Some tc -> begin - log_type_constraint __LINE__ "BL-reg-arg" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> begin - log_no_type_constraint __LINE__ "BL-reg-arg" ptype; + log_no_type_constraint __LINE__ rule ptype; () end) rdefs else () else if is_stack_parameter p then + let rule = "BL-stackarg" in (log_tfold_default (log_error ("Unable to retrieve stack offset from " @@ -615,8 +662,8 @@ object (self) match opttc with | Some tc -> begin - log_type_constraint __LINE__ "BL-stack-arg" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> ()) () @@ -635,11 +682,12 @@ object (self) match get_stackvar_type_annotation offset with | Some t -> let opttc = mk_btype_constraint lhstypevar t in + let rule = "BL-svintro" in (match opttc with | Some tc -> begin - log_type_constraint __LINE__ "BL-stack-vintro" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> ()) | _ -> @@ -647,11 +695,12 @@ object (self) let eltype = ptr_deref ptype in let atype = t_array eltype 1 in let opttc = mk_btype_constraint lhstypevar atype in + let rule = "BL-stackarg" in match opttc with | Some tc -> begin - log_type_constraint __LINE__ "BL-reg-arg" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> ()) end @@ -672,9 +721,10 @@ object (self) let immtypeconst = get_intvalue_type_constant immval in let rntypeterm = mk_vty_term rntypevar in let immtypeterm = mk_cty_term immtypeconst in + let rule = "CMP-rdef" in begin - log_subtype_constraint __LINE__ "CMP-imm" rntypeterm immtypeterm; - store#add_subtype_constraint rntypeterm immtypeterm + log_subtype_constraint __LINE__ rule rntypeterm immtypeterm; + store#add_subtype_constraint faddr iaddr rule rntypeterm immtypeterm end) rndefs | Compare (_, rn, rm, _) when rm#is_register -> @@ -695,9 +745,10 @@ object (self) let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in let rntypeterm = mk_vty_term rntypevar in let rmtypeterm = mk_vty_term rmtypevar in + let rule = "CMP-rdef" in begin - log_subtype_constraint __LINE__ "CMP-reg" rntypeterm rmtypeterm; - store#add_subtype_constraint rntypeterm rmtypeterm + log_subtype_constraint __LINE__ rule rntypeterm rmtypeterm; + store#add_subtype_constraint faddr iaddr rule rntypeterm rmtypeterm end) pairs); (let xrn_r = rn#to_expr floc in @@ -710,9 +761,10 @@ object (self) let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in let ftterm = mk_vty_term ftvar in let rmtypeterm = mk_vty_term rmtypevar in + let rule = "CMP-init" in begin - log_subtype_constraint __LINE__ "CMP-reg-init" ftterm rmtypeterm; - store#add_subtype_constraint ftterm rmtypeterm + log_subtype_constraint __LINE__ rule ftterm rmtypeterm; + store#add_subtype_constraint faddr iaddr rule ftterm rmtypeterm end) rmdefs | _ -> ()); @@ -726,9 +778,10 @@ object (self) let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in let ftterm = mk_vty_term ftvar in let rntypeterm = mk_vty_term rntypevar in + let rule = "CMP-init" in begin - log_subtype_constraint __LINE__ "CMP-reg-init" ftterm rntypeterm; - store#add_subtype_constraint ftterm rntypeterm + log_subtype_constraint __LINE__ rule ftterm rntypeterm; + store#add_subtype_constraint faddr iaddr rule ftterm rntypeterm end) rndefs | _ -> ()) end @@ -737,33 +790,23 @@ object (self) let rtreg = rt#to_register in 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 - (match opttc with - | Some tc -> - begin - log_type_constraint __LINE__ "LDR-rvintro" tc; - store#add_constraint tc - end - | _ -> ()) - | _ -> ()); + (regvar_type_introduction "LDR" rt); + (regvar_linked_to_exit "LDR" rt); (* 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.tbind floc#get_xpr_type xrmem_r in + let rule = "LDR-memop-tc" in TR.titer ~ok:(fun t -> let opttc = mk_btype_constraint rttypevar t in (match opttc with | Some tc -> begin - log_type_constraint __LINE__ "LDR-var" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> ())) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) @@ -773,152 +816,134 @@ object (self) (let xrdef = get_variable_rdefs_r (rn#to_variable floc) in let rnreg = rn#to_register in let offset = rm#to_numerical#toInt in - List.iter (fun rdsym -> - let ldaddr = rdsym#getBaseName in - let rdtypevar = mk_reglhs_typevar rnreg faddr ldaddr in - let rdtypevar = add_load_capability ~offset rdtypevar in - let rdtypeterm = mk_vty_term rdtypevar in - let rttypeterm = mk_vty_term rttypevar in - begin - log_subtype_constraint __LINE__ "LDR-imm-off" rdtypeterm rttypeterm; - store#add_subtype_constraint rdtypeterm rttypeterm - end) xrdef); - - (match TR.tmap rewrite_expr (memop#to_expr floc) with - | Error _ -> () - | Ok (XVar v) -> - (match floc#f#env#get_variable_type v with - | Some ty -> - let opttc = mk_btype_constraint rttypevar ty in - (match opttc with - | Some tc -> - begin - log_type_constraint __LINE__ "LDR-memop" tc; - store#add_constraint tc - end - | _ -> ()) - | _ -> ()) - | _ -> ()); + begin - (* if the address to load from is the address of a global struct field, - assign the type of that field to the destination register. *) - (match getopt_global_address_r (memop#to_address floc) with - | Some gaddr -> - if BCHConstantDefinitions.is_in_global_structvar gaddr then - match (BCHConstantDefinitions.get_structvar_base_offset gaddr) with - | Some (_, Field ((fname, fckey), NoOffset)) -> - let compinfo = bcfiles#get_compinfo fckey in - let finfo = get_compinfo_field compinfo fname in - let finfotype = resolve_type finfo.bftype in - (match finfotype with - | Error _ -> () - | Ok finfotype -> - let lhstype = - if is_struct_type finfotype then - let subcinfo = - get_struct_type_compinfo finfotype in - get_compinfo_scalar_type_at_offset subcinfo 0 - else - Some finfotype in - (match lhstype with - | Some ty -> - let opttc = mk_btype_constraint rttypevar ty in - (match opttc with - | Some tc -> - begin - log_type_constraint __LINE__ "LDR-struct-field" tc; - store#add_constraint tc - end - | _ -> ()) - | _ -> - chlog#add - "global struct var type constraint" - (LBLOCK [ - STR iaddr; - STR ": "; - STR compinfo.bcname; - STR ": unable to obtain field type"]))) - | Some (dw, boffset) -> - let _ = - chlog#add - "global struct var type constraint" - (LBLOCK [ - STR iaddr; - STR ": "; - dw#toPretty; - STR " with offset "; - offset_to_pretty boffset]) in - () - | _ -> () - else + (if rn#is_pc_register then () - | _ -> ()); + else + List.iter (fun rdsym -> + let ldaddr = rdsym#getBaseName in + let rdtypevar = mk_reglhs_typevar rnreg faddr ldaddr in + let rdtypevar = add_load_capability ~offset rdtypevar in + let rdtypeterm = mk_vty_term rdtypevar in + let rttypeterm = mk_vty_term rttypevar in + let rule = "LDR-load" in + begin + log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule rdtypeterm rttypeterm + end) xrdef); - (* if the value loaded is the start address of a global array, - assign that array type to the destination register. *) - (match getopt_global_address_r (memop#to_expr floc) with - | Some gaddr -> - if BCHConstantDefinitions.is_in_global_arrayvar gaddr then - (match (BCHConstantDefinitions.get_arrayvar_base_offset gaddr) with - | Some (_, offset, bty) -> - (match offset with - | Index (Const (CInt (i64, _, _)), NoOffset) -> - let cindex = mkNumericalFromInt64 i64 in - if cindex#equal numerical_zero then - let opttc = mk_btype_constraint rttypevar bty in - (match opttc with - | Some tc -> - begin - log_type_constraint __LINE__ "LDR-array" tc; - store#add_constraint tc - end - | _ -> ()) - else - () - | _ -> + (* if the address to load from is the address of a global struct field, + assign the type of that field to the destination register. *) + (match getopt_global_address_r (memop#to_address floc) with + | Some gaddr -> + if BCHConstantDefinitions.is_in_global_structvar gaddr then + match (BCHConstantDefinitions.get_structvar_base_offset gaddr) with + | Some (_, Field ((fname, fckey), NoOffset)) -> + let compinfo = bcfiles#get_compinfo fckey in + let finfo = get_compinfo_field compinfo fname in + let finfotype = resolve_type finfo.bftype in + (match finfotype with + | Error _ -> () + | Ok finfotype -> + let lhstype = + if is_struct_type finfotype then + let subcinfo = + get_struct_type_compinfo finfotype in + get_compinfo_scalar_type_at_offset subcinfo 0 + else + Some finfotype in + (match lhstype with + | Some ty -> + let opttc = mk_btype_constraint rttypevar ty in + let rule = "LDR-struct-field" in + (match opttc with + | Some tc -> + begin + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc + end + | _ -> ()) + | _ -> + chlog#add + "global struct var type constraint" + (LBLOCK [ + STR iaddr; + STR ": "; + STR compinfo.bcname; + STR ": unable to obtain field type"]))) + | Some (dw, boffset) -> + let _ = chlog#add - "global array var" + "global struct var type constraint" (LBLOCK [ STR iaddr; STR ": "; - gaddr#toPretty; - STR ", "; - offset_to_pretty offset - ])) - | _ -> ()) - | _ -> ()); + dw#toPretty; + STR " with offset "; + offset_to_pretty boffset]) in + () + | _ -> () + else + () + | _ -> ()); - (match getopt_stackaddress_r (memop#to_address floc) with - | None -> () - | Some offset -> - let rhstypevar = mk_localstack_lhs_typevar offset faddr iaddr in - let rhstypeterm = mk_vty_term rhstypevar in - let rttypeterm = mk_vty_term rttypevar in - begin - log_subtype_constraint - __LINE__ "LDR-stack-addr" rhstypeterm rttypeterm; - store#add_subtype_constraint rhstypeterm rttypeterm - end) + (* if the value loaded is the start address of a global array, + assign that array type to the destination register. *) + (match getopt_global_address_r (memop#to_expr floc) with + | Some gaddr -> + if BCHConstantDefinitions.is_in_global_arrayvar gaddr then + (match (BCHConstantDefinitions.get_arrayvar_base_offset gaddr) with + | Some (_, offset, bty) -> + (match offset with + | Index (Const (CInt (i64, _, _)), NoOffset) -> + let cindex = mkNumericalFromInt64 i64 in + if cindex#equal numerical_zero then + let opttc = mk_btype_constraint rttypevar bty in + let rule = "LDR-array" in + (match opttc with + | Some tc -> + begin + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc + end + | _ -> ()) + else + () + | _ -> + chlog#add + "global array var" + (LBLOCK [ + STR iaddr; + STR ": "; + gaddr#toPretty; + STR ", "; + offset_to_pretty offset + ])) + | _ -> ()) + | _ -> ()); + + (match getopt_stackaddress_r (memop#to_address floc) with + | None -> () + | Some offset -> + let rhstypevar = mk_localstack_lhs_typevar offset faddr iaddr in + let rhstypeterm = mk_vty_term rhstypevar in + let rttypeterm = mk_vty_term rttypevar in + let rule = "LDR-stack-addr" in + begin + log_subtype_constraint + __LINE__ rule rhstypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule rhstypeterm rttypeterm + end) + end) end | LoadRegisterByte (_, rt, rn, rm, _, _) when rm#is_immediate -> let rtreg = rt#to_register in let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in begin - - (match get_regvar_type_annotation () with - | Some t -> - let rtreg = rt#to_register in - let lhstypevar = mk_reglhs_typevar rtreg faddr iaddr in - let opttc = mk_btype_constraint lhstypevar t in - (match opttc with - | Some tc -> - begin - log_type_constraint __LINE__ "LDRB-rvintro" tc; - store#add_constraint tc - end - | _ -> ()) - | _ -> ()); + (regvar_type_introduction "LDRB" rt); + (regvar_linked_to_exit "LDRB" rt); (* LDRB rt, [rn, rm] : X_rndef.load <: X_rt *) (let xrdefs = get_variable_rdefs_r (rn#to_variable floc) in @@ -930,18 +955,20 @@ object (self) let rdtypevar = add_load_capability ~offset ~size:1 rdtypevar in let rdtypeterm = mk_vty_term rdtypevar in let rttypeterm = mk_vty_term rttypevar in + let rule = "LDRB-load" in begin - log_subtype_constraint __LINE__ "LDRB-imm-off" rdtypeterm rttypeterm; - store#add_subtype_constraint rdtypeterm rttypeterm + log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule rdtypeterm rttypeterm end) xrdefs); (* LDRB rt, ... : X_rt <: integer type *) (let tc = mk_int_type_constant Unsigned 8 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in + let rule = "LDRB-default" in begin - log_subtype_constraint __LINE__ "LDRB-lhs-byte" tctypeterm rttypeterm; - store#add_subtype_constraint tctypeterm rttypeterm + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm end) end @@ -950,14 +977,17 @@ object (self) let rtreg = rt#to_register in let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in begin + (regvar_type_introduction "LDRB" rt); + (regvar_linked_to_exit "LDRB" rt); (* LDRB rt, ... : X_rt <: integer type *) (let tc = mk_int_type_constant SignedNeutral 8 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in + let rule = "LDRB-default" in begin - log_subtype_constraint __LINE__ "LDRB-lhs-byte" tctypeterm rttypeterm; - store#add_subtype_constraint tctypeterm rttypeterm + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm end) end @@ -966,6 +996,8 @@ object (self) let rtreg = rt#to_register in let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in begin + (regvar_type_introduction "LDRH" rt); + (regvar_linked_to_exit "LDRH" rt); (* loaded type may be known *) (let xmem_r = memop#to_expr floc in @@ -975,11 +1007,12 @@ object (self) TR.titer ~ok:(fun t -> let opttc = mk_btype_constraint rttypevar t in + let rule = "LDRH-memop-tc" in (match opttc with | Some tc -> begin - log_type_constraint __LINE__ "LDRH-var" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> ())) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) @@ -995,9 +1028,10 @@ object (self) let rdtypevar = add_load_capability ~offset ~size:2 rdtypevar in let rdtypeterm = mk_vty_term rdtypevar in let rttypeterm = mk_vty_term rttypevar in + let rule = "LDRH-load" in begin - log_subtype_constraint __LINE__ "LDRH-imm-off" rdtypeterm rttypeterm; - store#add_subtype_constraint rdtypeterm rttypeterm + log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule rdtypeterm rttypeterm end) xrdef) end @@ -1005,14 +1039,17 @@ object (self) let rtreg = rt#to_register in let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in begin + (regvar_type_introduction "LDRH" rt); + (regvar_linked_to_exit "LDRH" rt); (* LDRH rt, ... : X_rt <: integer type *) (let tc = mk_int_type_constant SignedNeutral 16 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in + let rule = "LDRH-default" in begin - log_subtype_constraint __LINE__ "LDRB-lhs-byte" tctypeterm rttypeterm; - store#add_subtype_constraint tctypeterm rttypeterm + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm end) end @@ -1022,73 +1059,75 @@ object (self) let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let rnreg = rn#to_register in let rndefs = get_variable_rdefs_r (rn#to_variable floc) in + begin + (regvar_type_introduction "LSL" rd); + (regvar_linked_to_exit "LSL" rd); - (* LSL results in an unsigned integer *) - (let tc = mk_int_type_constant Unsigned 32 in - let tcterm = mk_cty_term tc in - let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint __LINE__ "LSL-lhs" tcterm lhstypeterm; - store#add_subtype_constraint tcterm lhstypeterm - end); - - (* LSL is applied to an unsigned integer *) - (List.iter (fun rnrdef -> - let rnaddr = rnrdef#getBaseName in - let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in - let tyc = mk_int_type_constant Unsigned 32 in - let tctypeterm = mk_cty_term tyc in - let rntypeterm = mk_vty_term rntypevar in - begin - log_subtype_constraint __LINE__ "LSL-rhs" tctypeterm rntypeterm; - store#add_subtype_constraint tctypeterm rntypeterm - end) rndefs) + (* LSL results in an unsigned integer *) + (let tc = mk_int_type_constant Unsigned 32 in + let tcterm = mk_cty_term tc in + let lhstypeterm = mk_vty_term lhstypevar in + let rule = "LSL-default" in + begin + log_subtype_constraint __LINE__ rule tcterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tcterm lhstypeterm + end); + (* LSL is applied to an unsigned integer *) + (let rule = "LSL-default" in + List.iter (fun rnrdef -> + let rnaddr = rnrdef#getBaseName in + let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in + let tyc = mk_int_type_constant Unsigned 32 in + let tctypeterm = mk_cty_term tyc in + let rntypeterm = mk_vty_term rntypevar in + begin + log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rntypeterm + end) rndefs) + end + + + | LogicalShiftRight (_, _, rd, _rn, rm, _) when rm#is_immediate -> (* - | LogicalShiftRight (_, _, rd, rn, rm, _) when rm#is_immediate -> let rdreg = rd#to_register in let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let rnreg = rn#to_register in let rndefs = get_variable_rdefs_r (rn#to_variable floc) in - - (* LSR results in an unsigned integer *) - (let tc = mk_int_type_constant Unsigned 32 in - let tcterm = mk_cty_term tc in - let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint __LINE__ "LSR-lhs" tcterm lhstypeterm; - store#add_subtype_constraint tcterm lhstypeterm - end); - - (* LSR is applied to an unsigned integer *) - (List.iter (fun rnrdef -> - let rnaddr = rnrdef#getBaseName in - let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in - let tyc = mk_int_type_constant Unsigned 32 in - let tctypeterm = mk_cty_term tyc in - let rntypeterm = mk_vty_term rntypevar in - begin - log_subtype_constraint __LINE__ "LSR-rhs" tctypeterm rntypeterm; - store#add_subtype_constraint tctypeterm rntypeterm - end) rndefs) *) + begin + (regvar_type_introduction "LSR" rd); + (regvar_linked_to_exit "LSR" rd); + (* + (* LSR results in an unsigned integer *) + (let tc = mk_int_type_constant Unsigned 32 in + let tcterm = mk_cty_term tc in + let lhstypeterm = mk_vty_term lhstypevar in + begin + log_subtype_constraint __LINE__ "LSR-lhs" tcterm lhstypeterm; + store#add_subtype_constraint tcterm lhstypeterm + end); + + (* LSR is applied to an unsigned integer *) + (List.iter (fun rnrdef -> + let rnaddr = rnrdef#getBaseName in + let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in + let tyc = mk_int_type_constant Unsigned 32 in + let tctypeterm = mk_cty_term tyc in + let rntypeterm = mk_vty_term rntypevar in + begin + log_subtype_constraint __LINE__ "LSR-rhs" tctypeterm rntypeterm; + store#add_subtype_constraint tctypeterm rntypeterm + end) rndefs) + *) + end + | Move (_, _, rd, rm, _, _) when rm#is_immediate -> 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 - | _ -> ()) - | _ -> ()); + (regvar_type_introduction "MOV" rd); + (regvar_linked_to_exit "MOV" rd); (let rmval = rm#to_numerical#toInt in (* 0 provides no information about the type *) @@ -1098,9 +1137,10 @@ object (self) let tyc = get_intvalue_type_constant rmval in let lhstypeterm = mk_vty_term lhstypevar in let tctypeterm = mk_cty_term tyc in + let rule = "MOV-c" in begin - log_subtype_constraint __LINE__ "MOV-imm" tctypeterm lhstypeterm; - store#add_subtype_constraint tctypeterm lhstypeterm + log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm end) end @@ -1110,50 +1150,11 @@ object (self) (* Move x, y --- x := y --- Y <: X *) | Move (_, c, rd, rm, _, _) when rm#is_register -> - let xrm_r = rm#to_expr floc in + let _xrm_r = rm#to_expr floc in let rdreg = rd#to_register in - let rdtypevar = 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 rdtypevar t in - (match opttc with - | Some tc -> - begin - log_type_constraint __LINE__ "MOV-rvintro" tc; - store#add_constraint tc - end - | _ -> ()) - | _ -> ()); - - (* propagate function argument type *) - (match getopt_initial_argument_value_r xrm_r with - | Some (rmreg, off) when off = 0 -> - let rhstypevar = mk_function_typevar faddr in - let rhstypevar = add_freg_param_capability rmreg rhstypevar in - let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in - let rhstypeterm = mk_vty_term rhstypevar in - let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint - __LINE__ "MOV-reg-init" rhstypeterm lhstypeterm; - store#add_subtype_constraint rhstypeterm lhstypeterm - 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__ "MOV-freturn" regterm fterm; - store#add_subtype_constraint regterm fterm - end); + (regvar_type_introduction "MOV" rd); + (regvar_linked_to_exit "MOV" rd); (* use reaching defs *) (let rmreg = rm#to_register in @@ -1169,6 +1170,7 @@ object (self) 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 + let rule = "MOV-rdef" in List.iter (fun rmrdef -> let rmaddr = rmrdef#getBaseName in if rmaddr != "init" then @@ -1176,8 +1178,9 @@ object (self) 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 + log_subtype_constraint __LINE__ rule rmtypeterm lhstypeterm; + store#add_subtype_constraint + faddr iaddr rule rmtypeterm lhstypeterm end) rmrdefs) end @@ -1197,21 +1200,23 @@ object (self) begin (* use function return type *) (let opttc = mk_btype_constraint typevar rtype in + let rule = "POP-rv" in match opttc with | Some tc -> begin - log_type_constraint __LINE__ "POP-rv" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> begin - log_no_type_constraint __LINE__ "POP-rv" rtype; + log_no_type_constraint __LINE__ rule rtype; () end); (* propagate via reaching defs *) (let r0var = floc#env#mk_arm_register_variable AR0 in let r0defs = get_variable_rdefs r0var in + let rule = "POP-rdef" in List.iter (fun r0def -> let r0addr = r0def#getBaseName in if r0addr != "init" then @@ -1219,9 +1224,9 @@ object (self) let r0typeterm = mk_vty_term r0typevar in let lhstypeterm = mk_vty_term typevar in begin - log_subtype_constraint - __LINE__ "POP-R0-rdef" r0typeterm lhstypeterm; - store#add_subtype_constraint r0typeterm lhstypeterm + log_subtype_constraint __LINE__ rule r0typeterm lhstypeterm; + store#add_subtype_constraint + faddr iaddr rule r0typeterm lhstypeterm end) r0defs) end) @@ -1230,6 +1235,27 @@ object (self) (* no type information gained *) () + | ReverseSubtract (_, _, rd, _, rm, _) -> + let rdreg = rd#to_register in + let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in + let rmdefs = get_variable_rdefs_r (rm#to_variable floc) in + let rmreg = rm#to_register in + begin + (regvar_type_introduction "RSB" rd); + (regvar_linked_to_exit "RSB" rd); + + (let rule = "RSB-rdef" in + 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__ rule rmtypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule rmtypeterm lhstypeterm + end) rmdefs); + end + | SignedMultiplyLong (_, _, rdlo, rdhi, rn, rm) -> let rdloreg = rdlo#to_register in let lhslotypevar = mk_reglhs_typevar rdloreg faddr iaddr in @@ -1244,21 +1270,31 @@ object (self) let tctypeterm = mk_cty_term tc in let lhslotypeterm = mk_vty_term lhslotypevar in let lhshitypeterm = mk_vty_term lhshitypevar in + let rule1 = "SMULL-default" in + let rule2 = "SMULL-rdef" in begin - store#add_subtype_constraint tctypeterm lhslotypeterm; - store#add_subtype_constraint tctypeterm lhshitypeterm; + log_subtype_constraint __LINE__ rule1 tctypeterm lhslotypeterm; + log_subtype_constraint __LINE__ rule1 tctypeterm lhshitypeterm; + store#add_subtype_constraint faddr iaddr rule1 tctypeterm lhslotypeterm; + store#add_subtype_constraint faddr iaddr rule1 tctypeterm lhshitypeterm; (List.iter (fun rnrdef -> let rnaddr = rnrdef#getBaseName in let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in let rntypeterm = mk_vty_term rntypevar in - store#add_subtype_constraint tctypeterm rntypeterm) rndefs); + begin + log_subtype_constraint __LINE__ rule2 tctypeterm rntypeterm; + store#add_subtype_constraint faddr iaddr rule2 tctypeterm rntypeterm + end) rndefs); (List.iter (fun rmrdef -> let rmaddr = rmrdef#getBaseName in let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in let rmtypeterm = mk_vty_term rmtypevar in - store#add_subtype_constraint tctypeterm rmtypeterm) rmdefs) + begin + log_subtype_constraint __LINE__ rule2 tctypeterm rmtypeterm; + store#add_subtype_constraint faddr iaddr rule2 tctypeterm rmtypeterm + end) rmdefs) end (* Store x in y --- *y := x --- X <: Y.store *) @@ -1284,10 +1320,11 @@ object (self) let rhstypevar = add_freg_param_capability rtreg rhstypevar in let rhstypeterm = mk_vty_term rhstypevar in let lhstypeterm = mk_vty_term lhstypevar in + let rule = "STR-init" in begin - log_subtype_constraint - __LINE__ "STR-funarg" rhstypeterm lhstypeterm; - store#add_subtype_constraint rhstypeterm lhstypeterm + log_subtype_constraint __LINE__ rule rhstypeterm lhstypeterm; + store#add_subtype_constraint + faddr iaddr rule rhstypeterm lhstypeterm end | _ -> ()); @@ -1295,6 +1332,7 @@ object (self) (let rtreg = rt#to_register in let rtvar_r = rt#to_variable floc in let rtrdefs = get_variable_rdefs_r rtvar_r in + let rule = "STR-rdef" in List.iter (fun rtrdef -> let rtaddr = rtrdef#getBaseName in if rtaddr != "init" then @@ -1303,8 +1341,9 @@ object (self) let lhstypeterm = mk_vty_term lhstypevar in begin log_subtype_constraint - __LINE__ "STR-imm-off" rttypeterm lhstypeterm; - store#add_subtype_constraint rttypeterm lhstypeterm + __LINE__ rule rttypeterm lhstypeterm; + store#add_subtype_constraint + faddr iaddr rule rttypeterm lhstypeterm end) rtrdefs); (* import type from stackvar-introductions *) @@ -1316,26 +1355,28 @@ object (self) let opttc = mk_btype_constraint lhstypevar t in (match opttc with | Some tc -> + let rule = "STR-svintro" in begin - log_type_constraint __LINE__ "STR-stack-vintro" tc; - store#add_constraint tc + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc end | _ -> ())) end); - (List.iter (fun rndsym -> + (let rule = "STR-store" in + 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 + let rntypevar = add_store_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 - __LINE__ "STR-imm-off" rttypeterm rntypeterm; - store#add_subtype_constraint rttypeterm rntypeterm + log_subtype_constraint __LINE__ rule rttypeterm rntypeterm; + store#add_subtype_constraint + faddr iaddr rule rttypeterm rntypeterm end) rtrdefs) rnrdefs) end @@ -1353,12 +1394,14 @@ object (self) let tc = mk_int_type_constant SignedNeutral 8 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in + let rule = "STRB-default" in begin - log_subtype_constraint __LINE__ "STRB-rhs-byte" tctypeterm rttypeterm; - store#add_subtype_constraint tctypeterm rttypeterm + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm end); - (List.iter (fun rndsym -> + (let rule = "STRB-rdef" in + List.iter (fun rndsym -> let straddr = rndsym#getBaseName in let rntypevar = mk_reglhs_typevar rnreg faddr straddr in let rntypevar = add_load_capability ~size:1 ~offset rntypevar in @@ -1368,9 +1411,9 @@ object (self) let rttypeterm = mk_vty_term rttypevar in let rntypeterm = mk_vty_term rntypevar in begin - log_subtype_constraint - __LINE__"STRB-imm-off" rttypeterm rntypeterm; - store#add_subtype_constraint rttypeterm rntypeterm + log_subtype_constraint __LINE__ rule rttypeterm rntypeterm; + store#add_subtype_constraint + faddr iaddr rule rttypeterm rntypeterm end) rtrdefs) rnrdefs) end @@ -1384,9 +1427,10 @@ object (self) (let tc = mk_int_type_constant SignedNeutral 8 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in + let rule = "STRB-default" in begin - log_subtype_constraint __LINE__ "STRB-rhs-byte" tctypeterm rttypeterm; - store#add_subtype_constraint tctypeterm rttypeterm + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm end) end @@ -1397,80 +1441,73 @@ object (self) let rndefs = get_variable_rdefs_r (rn#to_variable floc) in let rnreg = rn#to_register in begin + (regvar_type_introduction "SUB" rd); + (regvar_linked_to_exit "SUB" rd); (* Note: Does not take into consideration the possibility of the subtraction of two pointers *) (if rm#is_immediate && (rm#to_numerical#toInt = 0) then () + else if rd#is_sp_register && rn#is_sp_register then + (* no type information to be gained from stackpointer manipulations *) + () else + let rule = "SUB-rdef" in 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 + log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; + store#add_subtype_constraint + faddr iaddr rule rntypeterm lhstypeterm end) rndefs); - (* 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__ "SUB-freturn" regterm fterm; - store#add_subtype_constraint regterm fterm - end); - end - | UnsignedBitFieldExtract (_, _, rn) -> - (match rn#get_kind with - | ARMRegBitSequence (r, _, _) -> - let rnreg = register_of_arm_register r in - let rndefs = get_variable_rdefs_r (rn#to_variable floc) in - begin - (List.iter (fun rnrdef -> - let rnaddr = rnrdef#getBaseName in - let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in - let tyc = mk_int_type_constant Unsigned 32 in - let tctypeterm = mk_cty_term tyc in - let rntypeterm = mk_vty_term rntypevar in - begin - log_subtype_constraint __LINE__ "UBFX-rhs" tctypeterm rntypeterm; - store#add_subtype_constraint tctypeterm rntypeterm - end) rndefs) - end - | _ -> ()) + | UnsignedBitFieldExtract (_, rd, rn) -> + begin + (regvar_type_introduction "UBFX" rd); + (regvar_linked_to_exit "UBFX" rd); + + (match rn#get_kind with + | ARMRegBitSequence (r, _, _) -> + let rnreg = register_of_arm_register r in + let rndefs = get_variable_rdefs_r (rn#to_variable floc) in + begin + (List.iter (fun rnrdef -> + let rnaddr = rnrdef#getBaseName in + let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in + let tyc = mk_int_type_constant Unsigned 32 in + let tctypeterm = mk_cty_term tyc in + let rntypeterm = mk_vty_term rntypevar in + let rule = "UBFX-default" in + begin + log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; + store#add_subtype_constraint + faddr iaddr rule tctypeterm rntypeterm + end) rndefs) + end + | _ -> ()) + end | UnsignedExtendHalfword (_, rd, _, _) -> let rdreg = rd#to_register in let rdtypevar = mk_reglhs_typevar rdreg faddr iaddr in begin - (match get_regvar_type_annotation () with - | Some t -> - let opttc = mk_btype_constraint rdtypevar t in - (match opttc with - | Some tc -> - begin - log_type_constraint __LINE__ "UXTH-rvintro" tc; - store#add_constraint tc - end - | _ -> - let opttc = mk_btype_constraint rdtypevar t_short in - (match opttc with - | Some tc -> store#add_constraint tc - | _ -> ()) - ) - | _ -> - let opttc = mk_btype_constraint rdtypevar t_short in - (match opttc with - | Some tc -> store#add_constraint tc - | _ -> ())); + (regvar_type_introduction "UXTH" rd); + (regvar_linked_to_exit "UXTH" rd); + + (let opttc = mk_btype_constraint rdtypevar t_short in + let rule = "UBFX-default" in + (match opttc with + | Some tc -> + begin + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc + end + | _ -> ())); end | opc -> diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHARMConditionalExprTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHARMConditionalExprTest.ml index 7d48a36e..b8d658d3 100644 --- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHARMConditionalExprTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHARMConditionalExprTest.ml @@ -149,7 +149,7 @@ let compare_negative_tests () = ("cmn-bcs", "0x18620", "0x18624", "010572e30100002a", 3, "(R2 >= 4290772992)"); ("cmn-beq", "0x170d0", "0x170d4", "010073e30100000a", 3, "(R3 = -1)"); ("cmn-bhi", "0x1f9b0", "0x1f9b4", "1f0270e30100008a", 3, "(R0 > 268435455)"); - ("cmn-bne", "0x10a0c", "0x10a10", "010072e30100001a", 3, "((R2 + 1) != 0)") + ("cmn-bne", "0x10a0c", "0x10a10", "010072e30100001a", 3, "(R2 != (-1))") ] in begin TS.new_testsuite (testname ^ "_compare_negative_tests") lastupdated;