From 8089231716b609502a99415533c53cf82ca37647 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 22 Aug 2026 00:05:58 -0700 Subject: [PATCH 01/22] CHB: add peek capability to stream wrapper --- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 5 +++++ CodeHawk/CHB/bchlib/bCHStreamWrapper.ml | 11 ++++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index e58847de4..2d052bd3e 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -982,6 +982,11 @@ object method pushback: int -> unit + (** [peek_doubleword offset] returns the doubleword at offset [offset] from + the current position in the stream without consuming the bytes (the + position of the stream is unaffected). *) + method peek_doubleword: int -> doubleword_int + (* accessors *) method pos: int method sub: int -> int -> string diff --git a/CodeHawk/CHB/bchlib/bCHStreamWrapper.ml b/CodeHawk/CHB/bchlib/bCHStreamWrapper.ml index 47868cbf6..c62447938 100644 --- a/CodeHawk/CHB/bchlib/bCHStreamWrapper.ml +++ b/CodeHawk/CHB/bchlib/bCHStreamWrapper.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2022-2023 Aarno Labs LLC + Copyright (c) 2022-2026 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 @@ -354,6 +354,15 @@ object (self) ch <- new big_endian_stream_wrapper_t input end + method peek_doubleword (n: int) = + let input = IO.input_string (string_suffix s (pos + n)) in + let tmpch = + if little_endian then + (new little_endian_stream_wrapper_t input) + else + (new big_endian_stream_wrapper_t input) in + tmpch#read_doubleword + end From ddb9d36991b60357bb8777271c5f44d54a766f4d Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 22 Aug 2026 00:07:42 -0700 Subject: [PATCH 02/22] CHB:ARM: block predicated aggregates when part of larger predicate sequence --- .../bchlibarm32/bCHARMInstructionAggregate.ml | 39 ++++++++++++++++--- 1 file changed, 33 insertions(+), 6 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml index e7844d56c..dcf94195b 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml @@ -568,6 +568,23 @@ let identify_pseudo_ldrsb | _ -> None +let has_predicated_neighbor + (ch: pushback_stream_int) + (first: arm_assembly_instruction_int) + (last: arm_assembly_instruction_int): bool = + (match TR.to_option + (get_arm_assembly_instruction (first#get_address#add_int (-4))) with + | Some instr -> instr#has_opcode_condition + | _ -> false) + || (let iaddr = last#get_address#add_int 4 in + let bytes = ch#peek_doubleword 0 in + let opcode = + try + disassemble_arm_instruction ch iaddr bytes + with _ -> OpInvalid in + BCHARMOpcodeRecords.is_opcode_conditional opcode) + + (* format of predicate assignment (in ARM): assigns the result of a test as a 0/1 value to a register @@ -575,7 +592,7 @@ let identify_pseudo_ldrsb MOVEQ Rx, #1 *) let identify_predicate_assignment - (_ch: pushback_stream_int) + (ch: pushback_stream_int) (instr: arm_assembly_instruction_int): (bool * arm_assembly_instruction_int @@ -600,8 +617,11 @@ let identify_predicate_assignment && (not (imm1#to_numerical#equal imm2#to_numerical)) && (has_inverse_cc c1) && ((Option.get (get_inverse_cc c1)) = c2) -> - let inverse = is_zero imm2 in - Some (inverse, movinstr, instr, rd) + if has_predicated_neighbor ch movinstr instr then + None + else + let inverse = is_zero imm2 in + Some (inverse, movinstr, instr, rd) | _ -> None) | _ -> None) | _ -> None @@ -619,7 +639,7 @@ or MOVNE Rx, imm2 *) let identify_ternary_assignment - (_ch: pushback_stream_int) + (ch: pushback_stream_int) (instr: arm_assembly_instruction_int): (arm_assembly_instruction_int * arm_assembly_instruction_int @@ -653,14 +673,21 @@ let identify_ternary_assignment && (rd#get_register = rdreg) && (has_inverse_cc c1) && ((Option.get (get_inverse_cc c1)) = c2) -> - Some (movinstr, instr, rd, imm1#to_numerical, n2) + if has_predicated_neighbor ch movinstr instr then + None + else + Some (movinstr, instr, rd, imm1#to_numerical, n2) | BitwiseNot (false, c1, rd, imm1, _) when imm1#is_immediate && (rd#get_register = rdreg) && (has_inverse_cc c1) && ((Option.get (get_inverse_cc c1)) = c2) -> (match (negval imm1#to_numerical) with - | Some n1 -> Some (movinstr, instr, rd, n1, n2) + | Some n1 -> + if has_predicated_neighbor ch movinstr instr then + None + else + Some (movinstr, instr, rd, n1, n2) | _ -> None) | _ -> None) | _ -> None) From ed1560cd380714cce97cb175bf22b5c0d03981cb Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 22 Aug 2026 00:45:15 -0700 Subject: [PATCH 03/22] CHB:ARM: add support for predicated tests --- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 0e8b5857e..2c9a53c86 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -130,13 +130,28 @@ let make_conditional_predicate ~(testinstr: arm_assembly_instruction_int) ~(condloc: location_int) ~(testloc: location_int) = - let (frozenvars, optxpr, opsused) = + let testfloc = get_floc testloc in + let get_default_conditional_expr () = arm_conditional_expr ~condopc:condinstr#get_opcode ~testopc:testinstr#get_opcode ~condloc:condloc ~testloc:testloc in - (frozenvars, optxpr, opsused) + if is_opcode_conditional testinstr#get_opcode then + let finfo = testfloc#f in + match get_associated_test_instr finfo testloc#ci with + | Some (testtestloc , testtestinstr) -> + arm_conditional_conditional_expr + ~condopc:condinstr#get_opcode + ~testopc:testinstr#get_opcode + ~testtestopc: testtestinstr#get_opcode + ~condloc + ~testloc + ~testtestloc + | _ -> + get_default_conditional_expr () + else + get_default_conditional_expr () let make_instr_local_tests From 4c7528bf13fc7e849e3d19946fb7076e9747f6d8 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 23 Aug 2026 17:52:13 -0700 Subject: [PATCH 04/22] CHB:ARM: replace cmd list with threaded cmdstate to support predicated instructions --- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 263 ++++++++++++++---- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.mli | 32 ++- 3 files changed, 236 insertions(+), 63 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index c6e66e7ac..7f5f9e114 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_20260816" - ~date:"2026-0816" + ~version:"0.6.0_20260823" + ~date:"2026-0823" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 2c9a53c86..6c1ca2baf 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -62,6 +62,7 @@ open BCHARMAssemblyInstructions open BCHARMCHIFSystem open BCHARMCodePC open BCHARMConditionalExpr +open BCHARMDisassemblyUtils open BCHARMOpcodeRecords open BCHARMOperand open BCHARMTestSupport @@ -117,6 +118,129 @@ let package_transaction TRANSACTION (label, LF.mkCode (cnstAssigns @ cmds), None) +(* ------------------------------------------------------------------ cmdstate_t + Data structure and associated functions for the collection of commands inside + a basic block. The data structure allows for a refinement of the otherwise + linear sequence of commands, to enable a representation of predicated + instructions that result in increased precision of analysis results, due to + the collection of instructions with equal predicate in separate branches, + rather than having a single branch instruction per predicated instruction + with intervening joins. + *) + +type setter_key_t = { + sk_testloc: ctxt_iaddress_t; + sk_testtestloc: ctxt_iaddress_t option + } + +type fragment_t = { + fr_key: setter_key_t; + fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) + fr_thenbucket: cmd_t list; (* starts with thentest, grows by append *) + fr_elsebucket: cmd_t list (* starts with elsetest *) + } + +type cmdstate_t = { + cs_flat: cmd_t list; (* closed-out cmds, in order *) + cs_open: fragment_t option (* at most one open fragement *) + } + + +let get_setter_key + (finfo: function_info_int) + (testloc: location_int) + (testinstr: arm_assembly_instruction_int): setter_key_t = + let sk_testtestloc = + if is_opcode_conditional testinstr#get_opcode then + match get_associated_test_instr finfo testloc#ci with + | Some (testtestloc, _) -> Some testtestloc#ci + | None -> + let _ = + log_error_result + ~tag:"get_setter_key:Unable to get test-test-loc" + ~msg:testloc#ci + __FILE__ __LINE__ + [testinstr#toString] in + None + else + None in + {sk_testloc = testloc#ci; sk_testtestloc} + +let get_setter_key_at + (finfo: function_info_int) + (ctxtiaddr: ctxt_iaddress_t) + : (setter_key_t * arm_assembly_instruction_int * location_int) option = + match get_associated_test_instr finfo ctxtiaddr with + | None -> None + | Some (testloc, testinstr) -> + Some (get_setter_key finfo testloc testinstr, testinstr, testloc) + + +let cmdstate_start: cmdstate_t = {cs_flat = []; cs_open = None} + +(* Close cs_open (if any) into one BRANCH appended to cs_flat *) +let cmdstate_flush (cs: cmdstate_t): cmdstate_t = + match cs.cs_open with + | None -> cs + | Some fr -> + let branch = + BRANCH [LF.mkCode fr.fr_thenbucket; LF.mkCode fr.fr_elsebucket] in + {cs_flat = cs.cs_flat @ [branch]; cs_open = None} + +(* Extend cmdstate with the cmds for an unconditional / condition-covered + instruction: closes any open fragment, and appends the already wrapped + unit cmds *) +let cmdstate_append_linear + (cs: cmdstate_t) (unit_cmds: cmd_t list): cmdstate_t = + let cs = cmdstate_flush cs in + {cs with cs_flat = cs.cs_flat @ unit_cmds} + + +let cmdstate_append_predicated + (cs: cmdstate_t) + ~(key: setter_key_t) + ~(cc: arm_opcode_cc_t) + ~(thentest: cmd_t list) + ~(elsetest: cmd_t list) + ~(unit_cmds: cmd_t list): cmdstate_t = + match cs.cs_open with + | Some fr when fr.fr_key = key && cc = fr.fr_opencc -> + {cs with cs_open = + Some {fr with fr_thenbucket = fr.fr_thenbucket @ unit_cmds}} + | Some fr when fr.fr_key = key && Some cc = get_inverse_cc fr.fr_opencc -> + {cs with cs_open = + Some {fr with fr_elsebucket = fr.fr_elsebucket @ unit_cmds}} + | _ -> + let cs = cmdstate_flush cs in + {cs with + cs_open = + Some {fr_key = key; fr_opencc = cc; + fr_thenbucket = thentest @ unit_cmds; + fr_elsebucket = elsetest}} + + +(* Block end (no terminating conditional branch): flush and linearlize for + package transaction *) +let cmdstate_finish (cs: cmdstate_t): cmd_t list = + (cmdstate_flush cs).cs_flat + + +(* Terminator hookup: if the terminator's own setter_key_t matches the still + open fragment, hand the fragment's buckets to make_condtiion instead of + flushing them into an intra-block BRANCH; otherwise close the branch first.*) +let cmdstate_take_for_terminator + (cs: cmdstate_t) + ~(key: setter_key_t) + ~(cc: arm_opcode_cc_t): cmd_t list * cmd_t list * cmd_t list = + match cs.cs_open with + | Some fr when fr.fr_key = key && cc = fr.fr_opencc -> + (cs.cs_flat, fr.fr_thenbucket, fr.fr_elsebucket) + | Some fr when fr.fr_key = key && Some cc = get_inverse_cc fr.fr_opencc -> + (cs.cs_flat, fr.fr_elsebucket, fr.fr_thenbucket) + | _ -> + (cmdstate_finish cs, [], []) + + (* Returns the predicate instruction and associated info for a conditional, in particular, it returns a tuple consisting of: - a list of temporary variables created to preserve the (frozen) values @@ -533,7 +657,7 @@ let translate_arm_instruction ~(funloc:location_int) ~(codepc:arm_code_pc_int) ~(blocklabel:symbol_t) - ~(cmds:cmd_t list) = + ~(cmdstate:cmdstate_t) = let (ctxtiaddr, instr) = codepc#get_next_instruction in let faddr = funloc#f in let finfo = get_function_info faddr in @@ -585,42 +709,72 @@ let translate_arm_instruction else (loc#i#add_int 8)#to_numerical in let pcassign = floc#get_assign_commands pcv (XConst (IntConst iaddr8)) in + + let build_unit newcmds = + frozenAsserts @ (invop :: newcmds) @ [bwdinvop] @ pcassign in + let default newcmds = - ([], [], cmds @ frozenAsserts @ (invop :: newcmds) @ [bwdinvop] @ pcassign) in + ([], [], cmdstate_append_linear cmdstate (build_unit newcmds)) in - let make_conditional_commands (_c: arm_opcode_cc_t) (cmds: cmd_t list) = + let make_conditional_commands (c: arm_opcode_cc_t) (cmds: cmd_t list) = if instr#is_condition_covered then default cmds else match get_associated_test_instr finfo ctxtiaddr with | Some (testloc, testinstr) -> - let (_, tests) = - make_instr_local_tests - ~condloc:loc ~testloc ~condinstr:instr ~testinstr in - (match tests with - | Some (thentest, elsetest) -> - if has_false_condition_context ctxtiaddr then - default elsetest - else if has_true_condition_context ctxtiaddr then - default (thentest @ cmds) - else - default [BRANCH [LF.mkCode (thentest @ cmds); LF.mkCode elsetest]] - | _ -> - (* make non-deterministic branch, unless covered by True/False - context*) - if has_false_condition_context ctxtiaddr then - default [] - else if has_true_condition_context ctxtiaddr then - default cmds - else - default [BRANCH [LF.mkCode cmds; LF.mkCode [SKIP]]]) + if has_false_condition_context ctxtiaddr then + let (_, tests) = + make_instr_local_tests + ~condloc:loc ~testloc ~condinstr:instr ~testinstr in + (match tests with + | Some (_, elsetest) -> default elsetest + | _ -> default []) + else if has_true_condition_context ctxtiaddr then + let (_, tests) = + make_instr_local_tests + ~condloc:loc ~testloc ~condinstr:instr ~testinstr in + (match tests with + | Some (thentest, _) -> default (thentest @ cmds) + | _ -> default cmds) + else + let key = get_setter_key finfo testloc testinstr in + let unit_cmds = build_unit cmds in + (* make_instr_local_tests must be called for every predicated + instruction, not just the one that opens a fragment: besides + returning the then/else test commands, arm_conditional_expr / + arm_conditional_conditional_expr has the side effect of + registering condfloc#set_test_expr for this instruction's own + location, which bCHFnARMDictionary.ml's xdata generation and + bCHFnARMTypeConstraints.ml's type-constraint generation both + depend on per-instruction. *) + let (_, tests) = + make_instr_local_tests + ~condloc:loc ~testloc ~condinstr:instr ~testinstr in + let already_open = + match cmdstate.cs_open with + | Some fr -> + fr.fr_key = key + && (c = fr.fr_opencc || get_inverse_cc fr.fr_opencc = Some c) + | None -> false in + if already_open then + ([], [], + cmdstate_append_predicated + cmdstate ~key ~cc:c ~thentest:[] ~elsetest:[] ~unit_cmds) + else + let (thentest, elsetest) = + match tests with + | Some (t, e) -> (t, e) + | None -> ([], []) in + ([], [], + cmdstate_append_predicated cmdstate + ~key ~cc:c ~thentest ~elsetest ~unit_cmds) | _ -> if has_false_condition_context ctxtiaddr then default [] else if has_true_condition_context ctxtiaddr then default cmds else - default [BRANCH [LF.mkCode cmds; LF.mkCode [SKIP]]] in + default [BRANCH [LF.mkCode cmds; LF.mkCode[SKIP]]] in let get_register_vars (ops: arm_operand_int list) = List.fold_left (fun acc op -> @@ -649,7 +803,8 @@ let translate_arm_instruction List.fold_left (fun acc (op1, op2) -> let regvars = List.map get_register [op1; op2] in match regvars with - | [Some r1; Some r2] -> (floc#env#mk_arm_double_register_variable r1 r2) :: acc + | [Some r1; Some r2] -> + (floc#env#mk_arm_double_register_variable r1 r2) :: acc | _ -> acc) [] ops in let get_use_high_vars ?(is_pop=false) (xprs: xpr_t list): variable_t list = @@ -779,7 +934,8 @@ let translate_arm_instruction let extract_wide_lo x_r = TR.tmap (fun x -> XOp (XMod, [x; num_constant_expr numerical_e32])) x_r in - let unary_wop_cmds (f: xpr_t -> xpr_t) (wop: arm_wide_op_sequence_int): cmd_t list = + let unary_wop_cmds + (f: xpr_t -> xpr_t) (wop: arm_wide_op_sequence_int): cmd_t list = let (rdlo, rdhi) = get_wide_op_destination_operand wop in let (rnlo, rnhi) = get_unary_wide_op_source_operand wop in let vrdlo = floc#env#mk_register_variable rdlo#to_register in @@ -1102,7 +1258,12 @@ let translate_arm_instruction | _ -> [] in let elseaddr = codepc#get_false_branch_successor in - let cmds = cmds @ [invop] @ defcmds @ [bwdinvop] in + let (prefix_flat, thencode, elsecode) = + match get_setter_key_at finfo ctxtiaddr with + | Some (key, _, _) -> cmdstate_take_for_terminator cmdstate ~key ~cc:c + | _ -> (cmdstate_finish cmdstate, [], []) in + let cmds = prefix_flat @ [invop] @ defcmds @ [bwdinvop] in + (* let cmds = cmds @ [invop] @ defcmds @ [bwdinvop] in *) let transaction = package_transaction finfo blocklabel cmds in if finfo#has_associated_cc_setter ctxtiaddr then let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in @@ -1115,6 +1276,8 @@ let translate_arm_instruction (get_arm_assembly_instruction testaddr) in let (nodes, edges) = make_condition + ~thencode + ~elsecode ~condinstr:instr ~testinstr:testinstr ~condloc:loc @@ -1122,13 +1285,13 @@ let translate_arm_instruction ~blocklabel ~thenaddr ~elseaddr () in - ((blocklabel, [transaction]) :: nodes, edges, []) + ((blocklabel, [transaction]) :: nodes, edges, cmdstate_start) else let thenlabel = make_code_label thenaddr in let elselabel = make_code_label elseaddr in let nodes = [(blocklabel, [transaction])] in let edges = [(blocklabel, thenlabel); (blocklabel, elselabel)] in - (nodes, edges, []) + (nodes, edges, cmdstate_start) | CompareBranchZero (op, tgt) | CompareBranchNonzero (op, tgt) -> @@ -1145,11 +1308,11 @@ let translate_arm_instruction end) (op#to_expr floc) in let defcmds = floc#get_vardef_commands ~use:usevars ~usehigh ctxtiaddr in - let cmds = cmds @ defcmds @ [invop] in + let cmds = (cmdstate_finish cmdstate) @ defcmds @ [invop] in let transaction = package_transaction finfo blocklabel cmds in let (nodes, edges) = make_local_condition instr loc blocklabel thenaddr elseaddr in - ((blocklabel, [transaction]) :: nodes, edges, []) + ((blocklabel, [transaction]) :: nodes, edges, cmdstate_start) | Branch (_, op, _) | BranchExchange (ACCAlways, op) when op#is_absolute_address -> @@ -1815,7 +1978,7 @@ let translate_arm_instruction | IfThen _ when instr#is_block_condition -> let thenaddr = codepc#get_true_branch_successor in let elseaddr = codepc#get_false_branch_successor in - let cmds = cmds @ [invop] in + let cmds = (cmdstate_finish cmdstate) @ [invop] in let transaction = package_transaction finfo blocklabel cmds in (match get_associated_test_instr finfo ctxtiaddr with | Some (testloc, testinstr) -> @@ -1828,13 +1991,13 @@ let translate_arm_instruction ~blocklabel ~thenaddr ~elseaddr () in - ((blocklabel, [transaction]) :: nodes, edges, []) + ((blocklabel, [transaction]) :: nodes, edges, cmdstate_start) | _ -> let thenlabel = make_code_label thenaddr in let elselabel = make_code_label elseaddr in let nodes = [(blocklabel, [transaction])] in let edges = [(blocklabel, thenlabel); (blocklabel, elselabel)] in - (nodes, edges, [])) + (nodes, edges, cmdstate_start)) (* ---------------------------------------- LoadMultipleDecrementAfter -- * Loads multiple registers from consecutive memory locations using an @@ -2918,7 +3081,7 @@ let translate_arm_instruction (* collect all previous commands in the block and the invariant anchor and package them together with the vardef commands in a transaction *) - let cmds = cmds @ (invop :: ccvardefs) in + let cmds = (cmdstate_finish cmdstate) @ (invop :: ccvardefs) in let transaction = package_transaction finfo blocklabel cmds in (* create the branches according to the condition *) @@ -2934,7 +3097,7 @@ let translate_arm_instruction ~blocklabel ~thenaddr ~elseaddr () in - ((blocklabel, [transaction]) :: nodes, edges, []) + ((blocklabel, [transaction]) :: nodes, edges, cmdstate_start) | _ -> let (poplabel, popnode) = let label = make_code_label ~modifier:"pop" thenaddr in @@ -2947,7 +3110,7 @@ let translate_arm_instruction (blocklabel, poplabel); (poplabel, thenlabel); (blocklabel, elselabel)] in - (nodes, edges, [])) + (nodes, edges, cmdstate_start)) else (* regular, unconditional Pop, or conditional pop without pc *) @@ -4066,10 +4229,10 @@ let translate_arm_instruction | _ -> make_conditional_commands c cmds) | TableBranchByte _ -> - default cmds + default [] (* ?? *) | TableBranchHalfword _ -> - default cmds + default [] (* ?? *) | Test (c, rn, rm, _) -> let xrn_r = rn#to_expr floc in @@ -4962,10 +5125,10 @@ object (self) method translate_block (block:arm_assembly_block_int) exitLabel = let codepc = make_arm_code_pc block in let blocklabel = make_code_label block#get_context_string in - let rec aux cmds = - let (nodes,edges,newcmds) = + let rec aux (cmdstate: cmdstate_t) = + let (nodes, edges, newcmdstate) = try - translate_arm_instruction ~funloc ~codepc ~blocklabel ~cmds + translate_arm_instruction ~funloc ~codepc ~blocklabel ~cmdstate with | BCH_failure p -> let msg = @@ -4983,18 +5146,10 @@ object (self) match nodes with | [] -> if codepc#has_more_instructions then - aux newcmds - (* - else if codepc#has_conditional_successor then - let (testloc,jumploc,theniaddr,elseiaddr,testexpr) = - codepc#get_conditional_successor_info in - let transaction = package_transaction finfo blocklabel newcmds in - let (nodes,edges) = - make_condition - ~testloc ~jumploc ~theniaddr ~elseiaddr ~blocklabel ~testexpr in - ((blocklabel, [transaction])::nodes, edges) *) + aux newcmdstate else - let transaction = package_transaction finfo blocklabel newcmds in + let transaction = + package_transaction finfo blocklabel (cmdstate_finish newcmdstate) in let nodes = [(blocklabel, [transaction])] in let edges = List.map @@ -5008,7 +5163,7 @@ object (self) (nodes, edges) | _ -> (nodes,edges) in let _ = finfo#env#start_transaction in - let (nodes, edges) = aux [] in + let (nodes, edges) = aux cmdstate_start in begin List.iter (fun (label, node) -> codegraph#add_node label node) nodes; List.iter (fun (src, tgt) -> codegraph#add_edge src tgt) edges diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli index 990dd518a..f4e8a63bd 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli @@ -1,10 +1,10 @@ (* ============================================================================= - CodeHawk Binary Analyzer + CodeHawk Binary Analyzer Author: Henny Sipma ------------------------------------------------------------------------------ The MIT License (MIT) - - Copyright (c) 2021-2025 Aarno Labs LLC + + Copyright (c) 2021-2026 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 @@ -12,10 +12,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 @@ -36,15 +36,33 @@ open BCHLibTypes open BCHARMTypes +type setter_key_t = { + sk_testloc: ctxt_iaddress_t; + sk_testtestloc: ctxt_iaddress_t option + } + +type fragment_t = { + fr_key: setter_key_t; + fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) + fr_thenbucket: cmd_t list; (* starts with thentest, grows by append *) + fr_elsebucket: cmd_t list (* starts with elsetest *) + } + +type cmdstate_t = { + cs_flat: cmd_t list; (* closed-out cmds, in order *) + cs_open: fragment_t option (* at most one open fragement *) + } + + val translate_arm_instruction: funloc:location_int -> codepc:arm_code_pc_int -> blocklabel:symbol_t - -> cmds:cmd_t list + -> cmdstate:cmdstate_t -> ((symbol_t * (code_t, 'a) command_t list) list * (symbol_t * symbol_t) list - * cmd_t list) + * cmdstate_t) val translate_arm_assembly_function: arm_assembly_function_int -> unit From a795eb31422b60286bc95567a7bf613962c0e071 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 26 Aug 2026 11:49:32 -0700 Subject: [PATCH 05/22] XPR: simplify composite conjunction --- CodeHawk/CH/xprlib/xsimplify.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/CodeHawk/CH/xprlib/xsimplify.ml b/CodeHawk/CH/xprlib/xsimplify.ml index 839a534d5..3f282fdc9 100644 --- a/CodeHawk/CH/xprlib/xsimplify.ml +++ b/CodeHawk/CH/xprlib/xsimplify.ml @@ -1195,7 +1195,15 @@ and reduce_and m e1 e2 = else if syntactically_equal e1 e2 then (true, e1) else - default + match (e1, e2) with + + (* (x == y) and (x != y) *) + | (XOp (XEq, [x1; y1]), XOp (XNe, [x2; y2])) + when syntactically_equal x1 x2 && syntactically_equal y1 y2 -> + (true, false_constant_expr) + + | _ -> + default and reduce_shiftleft (m: bool) (e1: xpr_t) (e2: xpr_t): bool * xpr_t = From d349da5b592c856371f8326dfac053f78579f239 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 26 Aug 2026 11:50:07 -0700 Subject: [PATCH 06/22] CHB: fragment membership infrastructure --- CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 63 ++++++++++++++++++++++++++ CodeHawk/CHB/bchlib/bCHLibTypes.mli | 31 ++++++++++++- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +- 3 files changed, 95 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 78a5aacc3..0efa338fb 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1670,6 +1670,7 @@ object (self) val cc_user_to_setter = H.create 3 (* cc-users *) val test_expressions = H.create 3 (* test-expressions *) + val fragment_membership = H.create 3 val test_variables = H.create 3 (* test-variables *) (* val cvariable_types = H.create 3 *) (* types of constant-value variables *) @@ -2125,6 +2126,23 @@ object (self) let _ = H.iter (fun ix v -> result := (ix,v) :: !result) test_expressions in !result + method set_fragment_membership + (iaddr: ctxt_iaddress_t) (fm: fragment_membership_t) = + H.replace fragment_membership iaddr fm + + method get_fragment_membership + (iaddr: ctxt_iaddress_t): fragment_membership_t = + if H.mem fragment_membership iaddr then + H.find fragment_membership iaddr + else + raise + (BCH_failure + (LBLOCK [STR "function_info#get_fragment_membership: "; + STR iaddr])) + + method has_fragment_membership (iaddr: ctxt_iaddress_t) = + H.mem fragment_membership iaddr + method set_test_variables (test_iaddr: ctxt_iaddress_t) (vars: (variable_t * variable_t) list) = @@ -2484,6 +2502,46 @@ object (self) constant_table#set v (mkNumericalFromString (n#getAttribute "value"))) (node#getTaggedChildren "var") + method private write_xml_fragment_memberships (node: xml_element_int) = + let l = ref [] in + let _ = H.iter (fun k e -> l := (k, e) :: !l) fragment_membership in + let l = List.sort (fun (k1, _) (k2, _) -> Stdlib.compare k1 k2) !l in + begin + node#appendChildren + (List.map (fun (k, fm) -> + let eNode = xmlElement "fmem" in + begin + eNode#setAttribute "opener" fm.fmem_openerloc#ci; + eNode#setAttribute "iaddr" k; + eNode#setAttribute + "pol" (match fm.fmem_bucket with + | FragThen -> "then" | FragElse -> "else"); + eNode + end) l) + end + + method private read_xml_fragment_memberships (node: xml_element_int) = + let getcc = node#getTaggedChildren in + List.iter (fun eNode -> + let get = eNode#getAttribute in + let iaddr = get "iaddr" in + let opener = + BCHLocation.ctxt_string_to_location (self#get_address) (get "opener") in + let polarity = + match (get "pol") with + | "then" -> FragThen + | "else" -> FragElse + | s -> + raise + (BCH_failure + (LBLOCK [STR "read_xml_fragment_memberships: "; + self#get_address#toPretty; + STR ": "; + STR s])) in + H.add fragment_membership iaddr + {fmem_openerloc = opener; fmem_bucket = polarity}) + (getcc "fmem") + method private write_xml_test_expressions (node:xml_element_int) = let l = ref [] in let _ = H.iter (fun k e -> l := (k,e) :: !l) test_expressions in @@ -2594,6 +2652,7 @@ object (self) let cNode = xmlElement "constants" in let tvNode = xmlElement "test-variables" in let teNode = xmlElement "test-expressions" in + let fmNode = xmlElement "fragment-memberships" in let jtNode = xmlElement "jump-targets" in let ctNode = xmlElement "call-targets" in let fsNode = xmlElement "format-strings" in @@ -2608,6 +2667,7 @@ object (self) self#write_xml_constants cNode; self#write_xml_cc_users ccNode; self#write_xml_test_expressions teNode; + self#write_xml_fragment_memberships fmNode; self#write_xml_test_variables tvNode; (* self#write_xml_jump_targets jtNode ; *) self#write_xml_call_targets ctNode; @@ -2624,6 +2684,7 @@ object (self) ccNode; tvNode; teNode; + fmNode; cNode; ctNode; fsNode; @@ -2649,6 +2710,8 @@ object (self) self#read_xml_test_variables (getc "test-variables")); (if hasc "test-expressions" then self#read_xml_test_expressions (getc "test-expressions")); + (if hasc "fragment-memberships" then + self#read_xml_fragment_memberships (getc "fragment-memberships")); (if hasc "format-strings" then self#read_xml_format_strings (getc "format-strings")); (if hasc "base-pointers" then diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 2d052bd3e..2a9e717bd 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -5778,6 +5778,7 @@ class type proofobligations_int = end + (** {b Principal access point for function characteristics and analysis results.} This data structure keeps track of: @@ -5786,7 +5787,18 @@ class type proofobligations_int = - jump targets It also maintains a summary of the function api and semantics. -*) + *) + +(** Fragments represent sequences of instructions within a basic block that + are executed under the same polarity of a shared governing condition.*) +type fragment_bucket_t = FragThen | FragElse + +type fragment_membership_t = { + fmem_openerloc: location_int; + fmem_bucket: fragment_bucket_t + } + + class type function_info_int = object @@ -6070,6 +6082,22 @@ object method get_test_variables: ctxt_iaddress_t -> (variable_t * variable_t) list + (** [finfo#set_fragment_membership iaddr mem] records that the instruction at + [iaddr] belongs to a predicated fragment starting at [mem]'s openerloc + with polarity given by [mem']s bucket (currently only used in arm32).*) + method set_fragment_membership: + ctxt_iaddress_t -> fragment_membership_t -> unit + + (** [finfo#get_fragment_membership iaddr] returns fragment membership info if + the instruction at [iaddr] belongs to a fragment. + + raise BCH_failure if the instruction at [iaddr] does not have an + associated fragment_membership.*) + method get_fragment_membership: ctxt_iaddress_t -> fragment_membership_t + + method has_fragment_membership: ctxt_iaddress_t -> bool + + (** {2 Connections}*) (** [finfo#connect_cc_user u_iaddr s_iaddr] records that the instruction at @@ -6619,6 +6647,7 @@ class type floc_int = jump. *) method has_test_expr: bool + (** {1 Jump targets}*) (** [set_jumptable_target base jt reg] registers jumptable [jt] with base diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 7f5f9e114..65c78374c 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_20260823" - ~date:"2026-0823" + ~version:"0.6.0_20260826" + ~date:"2026-0826" ~licensee: None ~maxfilesize: None () From c93f85c70e3ce2d768fda70df645268cef025cc8 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 26 Aug 2026 11:50:41 -0700 Subject: [PATCH 07/22] CHB:ARM: fragment translation for predicated instructions --- .../CHB/bchlibarm32/bCHFnARMDictionary.ml | 56 +++++++++++++++- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 65 +++++++++++++++---- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.mli | 3 +- 3 files changed, 109 insertions(+), 15 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 228e4aee6..86403e11c 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -679,12 +679,63 @@ object (self) match c with | ACCAlways -> ([tagstring], args) | _ when instr#is_condition_covered -> ([tagstring], args) + | c when is_cond_conditional c && floc#f#has_fragment_membership floc#cia -> + let csetter = floc#f#get_associated_cc_setter floc#cia in + let fm = floc#f#get_fragment_membership floc#cia in + let openerloc = fm.fmem_openerloc in + let openerfloc = get_floc openerloc in + let fmxpr = floc#f#get_test_expr openerloc#ci in + let txpr = + match fm.fmem_bucket with + | FragThen -> fmxpr + | FragElse -> simplify_xpr (XOp (XLNot, [fmxpr])) in + let fxpr = simplify_xpr (XOp (XLNot, [txpr])) in + let tcond = rewrite_floc_expr openerfloc txpr in + let fcond = rewrite_floc_expr openerfloc fxpr in + let ctcond_r = floc#xpr_to_cxpr ~size:(Some 4) tcond in + let cfcond_r = floc#xpr_to_cxpr ~size:(Some 4) fcond in + let rdefs = (get_all_rdefs txpr) @ (get_all_rdefs tcond) in + let argslen = List.length args in + let xtag = "xxcc" ^ (string_repeat "r" (List.length rdefs)) in + let xtag = tagstring ^ xtag in + let newargs = [ + index_xpr (Ok tcond); + index_xpr (Ok fcond); + index_xpr ctcond_r; + index_xpr cfcond_r + ] @ rdefs in + let ictag = "ic:" ^ (string_of_int argslen) in + let icrtag = "icr:" ^ (string_of_int (argslen + 1)) in + let icctag = "icc:" ^ (string_of_int (argslen + 2)) in + let iccrtag = "iccr:" ^ (string_of_int (argslen + 3)) in + let icsetter = "icsetter:" ^ csetter in + let icopenerloc = "icopener:" ^ openerloc#ci in + let icbucket = + "icbucket:" + ^ (match fm.fmem_bucket with FragThen -> "then" | FragElse -> "else") in + let tags = + xtag + :: [ictag; + icrtag; + icctag; + iccrtag; + icsetter; + icbucket; + icopenerloc;] in + let args = args @ newargs in + (tags, args) + + (* conditional that was not made part of a fragment *) | c when is_cond_conditional c && floc#has_test_expr -> + let _ = + log_diagnostics_result + ~tag:"add_optional_instr_condition:no fragment" + ~msg:(p2s floc#l#toPretty) + __FILE__ __LINE__ + [p2s instr#toPretty] in let csetter = floc#f#get_associated_cc_setter floc#cia in let txpr = floc#get_test_expr in let fxpr = simplify_xpr (XOp (XLNot, [txpr])) 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#xpr_to_cxpr ~size:(Some 4) tcond in @@ -707,6 +758,7 @@ object (self) let tags = xtag :: [ictag; icrtag; icctag; iccrtag; icsetter] in let args = args @ newargs in (tags, args) + | _ -> (tagstring :: ["uc"], args) in let add_optional_subsumption (tags: string list): string list = diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 6c1ca2baf..34c25a1f1 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -135,7 +135,8 @@ type setter_key_t = { type fragment_t = { fr_key: setter_key_t; - fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) + fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) + fr_openerloc: location_int; (* location of first instr in fragment *) fr_thenbucket: cmd_t list; (* starts with thentest, grows by append *) fr_elsebucket: cmd_t list (* starts with elsetest *) } @@ -183,9 +184,11 @@ let cmdstate_flush (cs: cmdstate_t): cmdstate_t = match cs.cs_open with | None -> cs | Some fr -> + let invlabel = get_invariant_label fr.fr_openerloc in + let openerinvop = OPERATION {op_name = invlabel; op_args = []} in let branch = BRANCH [LF.mkCode fr.fr_thenbucket; LF.mkCode fr.fr_elsebucket] in - {cs_flat = cs.cs_flat @ [branch]; cs_open = None} + {cs_flat = cs.cs_flat @ [openerinvop; branch]; cs_open = None} (* Extend cmdstate with the cmds for an unconditional / condition-covered instruction: closes any open fragment, and appends the already wrapped @@ -200,6 +203,7 @@ let cmdstate_append_predicated (cs: cmdstate_t) ~(key: setter_key_t) ~(cc: arm_opcode_cc_t) + ~(openerloc: location_int) ~(thentest: cmd_t list) ~(elsetest: cmd_t list) ~(unit_cmds: cmd_t list): cmdstate_t = @@ -214,7 +218,9 @@ let cmdstate_append_predicated let cs = cmdstate_flush cs in {cs with cs_open = - Some {fr_key = key; fr_opencc = cc; + Some {fr_key = key; + fr_opencc = cc; + fr_openerloc = openerloc; fr_thenbucket = thentest @ unit_cmds; fr_elsebucket = elsetest}} @@ -234,9 +240,13 @@ let cmdstate_take_for_terminator ~(cc: arm_opcode_cc_t): cmd_t list * cmd_t list * cmd_t list = match cs.cs_open with | Some fr when fr.fr_key = key && cc = fr.fr_opencc -> - (cs.cs_flat, fr.fr_thenbucket, fr.fr_elsebucket) + let invlabel = get_invariant_label fr.fr_openerloc in + let openerinvop = OPERATION {op_name = invlabel; op_args = []} in + (cs.cs_flat @ [openerinvop], fr.fr_thenbucket, fr.fr_elsebucket) | Some fr when fr.fr_key = key && Some cc = get_inverse_cc fr.fr_opencc -> - (cs.cs_flat, fr.fr_elsebucket, fr.fr_thenbucket) + let invlabel = get_invariant_label fr.fr_openerloc in + let openerinvop = OPERATION {op_name = invlabel; op_args = []} in + (cs.cs_flat @ [openerinvop], fr.fr_elsebucket, fr.fr_thenbucket) | _ -> (cmdstate_finish cs, [], []) @@ -710,6 +720,9 @@ let translate_arm_instruction (loc#i#add_int 8)#to_numerical in let pcassign = floc#get_assign_commands pcv (XConst (IntConst iaddr8)) in + let build_opener_unit newcmds = + frozenAsserts @ newcmds @ [bwdinvop] @ pcassign in + let build_unit newcmds = frozenAsserts @ (invop :: newcmds) @ [bwdinvop] @ pcassign in @@ -738,7 +751,6 @@ let translate_arm_instruction | _ -> default cmds) else let key = get_setter_key finfo testloc testinstr in - let unit_cmds = build_unit cmds in (* make_instr_local_tests must be called for every predicated instruction, not just the one that opens a fragment: besides returning the then/else test commands, arm_conditional_expr / @@ -756,18 +768,40 @@ let translate_arm_instruction fr.fr_key = key && (c = fr.fr_opencc || get_inverse_cc fr.fr_opencc = Some c) | None -> false in + let fmem = + match cmdstate.cs_open with + | Some fr when already_open -> + {fmem_openerloc = fr.fr_openerloc; + fmem_bucket = if c = fr.fr_opencc then FragThen else FragElse} + | _ -> + {fmem_openerloc = loc; fmem_bucket = FragThen} in + let _ = finfo#set_fragment_membership ctxtiaddr fmem in if already_open then + let unit_cmds = build_unit cmds in ([], [], cmdstate_append_predicated - cmdstate ~key ~cc:c ~thentest:[] ~elsetest:[] ~unit_cmds) + cmdstate + ~key + ~cc:c + ~openerloc:fmem.fmem_openerloc + ~thentest:[] + ~elsetest:[] + ~unit_cmds) else + let unit_cmds = build_opener_unit cmds in let (thentest, elsetest) = match tests with | Some (t, e) -> (t, e) | None -> ([], []) in ([], [], - cmdstate_append_predicated cmdstate - ~key ~cc:c ~thentest ~elsetest ~unit_cmds) + cmdstate_append_predicated + cmdstate + ~key + ~cc:c + ~openerloc:fmem.fmem_openerloc + ~thentest + ~elsetest + ~unit_cmds) | _ -> if has_false_condition_context ctxtiaddr then default [] @@ -1234,6 +1268,8 @@ let translate_arm_instruction | Branch (c, op, _) | BranchExchange (c, op) when is_cond_conditional c -> + let is_direct_branch = + match instr#get_opcode with Branch _ -> true | _ -> false in let thenaddr = if op#is_absolute_address then (make_i_location loc op#get_absolute_address)#ci @@ -1259,9 +1295,14 @@ let translate_arm_instruction [] in let elseaddr = codepc#get_false_branch_successor in let (prefix_flat, thencode, elsecode) = - match get_setter_key_at finfo ctxtiaddr with - | Some (key, _, _) -> cmdstate_take_for_terminator cmdstate ~key ~cc:c - | _ -> (cmdstate_finish cmdstate, [], []) in + (* Don't merge fragment branch with CFG branch if this is an indirect + jump *) + if is_direct_branch then + match get_setter_key_at finfo ctxtiaddr with + | Some (key, _, _) -> cmdstate_take_for_terminator cmdstate ~key ~cc:c + | _ -> (cmdstate_finish cmdstate, [], []) + else + (cmdstate_finish cmdstate, [], []) in let cmds = prefix_flat @ [invop] @ defcmds @ [bwdinvop] in (* let cmds = cmds @ [invop] @ defcmds @ [bwdinvop] in *) let transaction = package_transaction finfo blocklabel cmds in diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli index f4e8a63bd..1f32a0bf8 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli @@ -43,7 +43,8 @@ type setter_key_t = { type fragment_t = { fr_key: setter_key_t; - fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) + fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) + fr_openerloc: location_int; (* location of first instr in fragment *) fr_thenbucket: cmd_t list; (* starts with thentest, grows by append *) fr_elsebucket: cmd_t list (* starts with elsetest *) } From 37eebc3af147f15f5c61704415d719038658c36c Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 8 Sep 2026 13:01:09 -0700 Subject: [PATCH 08/22] CHB: recognize struct first field with target type --- CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml index 67e802a49..c182ee1e0 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml @@ -310,6 +310,20 @@ object (self) && Option.is_none tgtsize && Option.is_none tgtbtype -> Ok NoOffset + | XConst (IntConst n) when + n#equal CHNumerical.numerical_zero + && Option.is_some tgtbtype + && is_struct_type (Option.get tgtbtype) + && is_struct_type btype -> + let tgttype = Option.get tgtbtype in + let cinfo1 = get_struct_type_compinfo tgttype in + let cinfo2 = get_struct_type_compinfo btype in + if cinfo1.bckey = cinfo2.bckey then + Ok NoOffset + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "cinfo1: " ^ cinfo1.bcname + ^ "; cinfo2: " ^ cinfo2.bcname] | XConst (IntConst _) -> if is_struct_type btype then let compinfo = get_struct_type_compinfo btype in From 6624c67fdf007b007cee570d39968b35b06ad4b9 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 8 Sep 2026 13:03:24 -0700 Subject: [PATCH 09/22] CHB: identify struct type if there is no array --- CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml | 1 + CodeHawk/CHB/bchlib/bCHVersion.ml | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml index 371e1df4c..7a38371fb 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml @@ -910,6 +910,7 @@ object (self) let ty = bcd#get_typ ixty in match ty with | TArray (TComp _, _, _) -> Some ty + | TComp _ -> Some ty | _ -> None) None in match optstructty with | None -> None diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 65c78374c..a6cb593a9 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_20260826" - ~date:"2026-0826" + ~version:"0.6.0_20260908" + ~date:"2026-0908" ~licensee: None ~maxfilesize: None () From 73389041269ea06076832e5644780e8ebd46764c Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 8 Sep 2026 13:04:06 -0700 Subject: [PATCH 10/22] XPR: add simplifications --- CodeHawk/CH/xprlib/xsimplify.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/CodeHawk/CH/xprlib/xsimplify.ml b/CodeHawk/CH/xprlib/xsimplify.ml index 3f282fdc9..c5f2c4bce 100644 --- a/CodeHawk/CH/xprlib/xsimplify.ml +++ b/CodeHawk/CH/xprlib/xsimplify.ml @@ -1143,6 +1143,9 @@ and reduce_or m e1 e2 = XOp (XSubset, [ _s ; _t ])) when (is_zero y) -> (true, XOp (XLe, [ x ; z])) + | (XOp (XNe, [x1; y1]), XOp (XEq, [x2; y2])) + when syntactically_equal x1 x2 && syntactically_equal y1 y2 -> + (true, true_constant_expr) | _ -> default @@ -1201,7 +1204,9 @@ and reduce_and m e1 e2 = | (XOp (XEq, [x1; y1]), XOp (XNe, [x2; y2])) when syntactically_equal x1 x2 && syntactically_equal y1 y2 -> (true, false_constant_expr) - + | (XOp (XNe, [x1; y1]), XOp (XEq, [x2; y2])) + when syntactically_equal x1 x2 && syntactically_equal y1 y2 -> + (true, false_constant_expr) | _ -> default From d63a23c237c23ebe8764edd2772b8b7bc71ff5d4 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 8 Sep 2026 13:05:22 -0700 Subject: [PATCH 11/22] CHB:ARM: move translation utilities to separate file --- .../CHB/bchlibarm32/bCHARMTranslationUtil.ml | 90 +++++++++++++++++++ .../CHB/bchlibarm32/bCHARMTranslationUtil.mli | 55 ++++++++++++ 2 files changed, 145 insertions(+) create mode 100644 CodeHawk/CHB/bchlibarm32/bCHARMTranslationUtil.ml create mode 100644 CodeHawk/CHB/bchlibarm32/bCHARMTranslationUtil.mli diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMTranslationUtil.ml b/CodeHawk/CHB/bchlibarm32/bCHARMTranslationUtil.ml new file mode 100644 index 000000000..dcd9f9240 --- /dev/null +++ b/CodeHawk/CHB/bchlibarm32/bCHARMTranslationUtil.ml @@ -0,0 +1,90 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2026 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 + in the Software without restriction, including without limitation the rights + 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 + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chlib *) +open CHLanguage +open CHPretty + +(* bchlib *) +open BCHLibTypes +open BCHLocation + + +module LF = CHOnlineCodeSet.LanguageFactory + + +let make_code_label + ?(src:doubleword_int option) + ?(modifier:string option) + (address:ctxt_iaddress_t): symbol_t = + let name = + if address = "exit" || address = "?" then + "exit" + else + "pc_" ^ address in + let atts = match modifier with + | Some s -> [s] + | _ -> [] in + let atts = + if address = "?" then + "unresolved-jump" :: atts + else + atts in + let atts = match src with + | Some s -> s#to_fixed_length_hex_string :: atts | _ -> atts in + ctxt_string_to_symbol name ~atts address + + +let get_invariant_label ?(bwd=false) (loc:location_int) = + if bwd then + ctxt_string_to_symbol "bwd_invariant" loc#ci + else + ctxt_string_to_symbol "invariant" loc#ci + + +let get_invariant_operation (loc: location_int): cmd_t = + let invlabel = get_invariant_label loc in + OPERATION {op_name = invlabel; op_args = []} + + +let package_transaction + (finfo:function_info_int) (label:symbol_t) (cmds:cmd_t list) = + let cmds = + List.filter + (fun cmd -> match cmd with SKIP -> false | _ -> true) cmds in + let cnstAssigns = finfo#env#end_transaction in + TRANSACTION (label, LF.mkCode (cnstAssigns @ cmds), None) + + +let get_frozen_asserts + (finfo: function_info_int) (ctxtiaddr: ctxt_iaddress_t): cmd_t list = + List.map (fun (v, fv) -> ASSERT (EQ (v, fv))) + (finfo#get_test_variables ctxtiaddr) + + +let chif_cmds_to_pretty (cmds: cmd_t list): pretty_t = + pretty_print_list cmds (command_to_pretty 0) "[" "; " "]" diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMTranslationUtil.mli b/CodeHawk/CHB/bchlibarm32/bCHARMTranslationUtil.mli new file mode 100644 index 000000000..dab0ee088 --- /dev/null +++ b/CodeHawk/CHB/bchlibarm32/bCHARMTranslationUtil.mli @@ -0,0 +1,55 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2026 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 + in the Software without restriction, including without limitation the rights + 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 + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chlib *) +open CHLanguage +open CHPretty + +(* bchlib *) +open BCHLibTypes + + +val make_code_label: + ?src:doubleword_int + -> ?modifier:string + -> ctxt_iaddress_t -> symbol_t + + +val get_invariant_label: ?bwd:bool -> location_int -> symbol_t + + +val get_invariant_operation: location_int -> cmd_t + + +val package_transaction: + function_info_int -> symbol_t -> cmd_t list -> cmd_t + + +val get_frozen_asserts: function_info_int -> ctxt_iaddress_t -> cmd_t list + + +val chif_cmds_to_pretty: cmd_t list -> pretty_t From 530e0d24336ad575dd6edfcbe0d484400fa1daf6 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 8 Sep 2026 13:06:25 -0700 Subject: [PATCH 12/22] CHB:ARM: move construction of conditional tests to separate file --- .../CHB/bchlibarm32/bCHARMPredicateTest.ml | 412 ++++++++++++++++++ .../CHB/bchlibarm32/bCHARMPredicateTest.mli | 157 +++++++ 2 files changed, 569 insertions(+) create mode 100644 CodeHawk/CHB/bchlibarm32/bCHARMPredicateTest.ml create mode 100644 CodeHawk/CHB/bchlibarm32/bCHARMPredicateTest.mli diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMPredicateTest.ml b/CodeHawk/CHB/bchlibarm32/bCHARMPredicateTest.ml new file mode 100644 index 000000000..bad8f92fd --- /dev/null +++ b/CodeHawk/CHB/bchlibarm32/bCHARMPredicateTest.ml @@ -0,0 +1,412 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2026 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 + in the Software without restriction, including without limitation the rights + 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 + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chlib *) +open CHLanguage + +(* chutil *) +open CHLogger + +(* xprlib *) +open Xprt +open XprTypes +open XprUtil +open Xsimplify + +(* bchlib *) +open BCHFloc +open BCHLibTypes + +(* bchlibarm32 *) +open BCHARMAssemblyInstructions +open BCHARMConditionalExpr +open BCHARMOpcodeRecords +open BCHARMTestSupport +open BCHARMTranslationUtil +open BCHARMTypes + +module LF = CHOnlineCodeSet.LanguageFactory +module TR = CHTraceResult + +let p2s = CHPrettyUtil.pretty_to_string +(* other useful functions for printing debug messages +let x2p = XprToPretty.xpr_formatter#pr_expr +let x2s x = p2s (x2p x) + *) + +let make_conditional_predicate + ~(condinstr: arm_assembly_instruction_int) + ~(testinstr: arm_assembly_instruction_int) + ~(condloc: location_int) + ~(testloc: location_int) = + let testfloc = get_floc testloc in + let get_default_conditional_expr () = + arm_conditional_expr + ~condopc:condinstr#get_opcode + ~testopc:testinstr#get_opcode + ~condloc:condloc + ~testloc:testloc in + if is_opcode_conditional testinstr#get_opcode then + let finfo = testfloc#f in + match get_associated_test_instr finfo testloc#ci with + | Some (testtestloc , testtestinstr) -> + arm_conditional_conditional_expr + ~condopc:condinstr#get_opcode + ~testopc:testinstr#get_opcode + ~testtestopc: testtestinstr#get_opcode + ~condloc + ~testloc + ~testtestloc + | _ -> + get_default_conditional_expr () + else + get_default_conditional_expr () + + +let make_instr_local_tests + ~(condinstr:arm_assembly_instruction_int) + ~(testinstr:arm_assembly_instruction_int) + ~(condloc:location_int) + ~(testloc:location_int) = + let testfloc = get_floc testloc in + let condfloc = get_floc condloc in + let env = testfloc#f#env in + let reqN () = env#mk_num_temp in + let reqC i = env#request_num_constant i in + let (frozenVars, optboolxpr, _) = + make_conditional_predicate ~condinstr ~testinstr ~condloc ~testloc in + let convert_to_chif expr = + let (cmds, bxpr) = xpr_to_boolexpr reqN reqC expr in + cmds @ [ASSERT bxpr] in + let convert_to_assert eexpr = + let expr = simplify_xpr eexpr in + let vars = variables_in_expr expr in + let varssize = List.length vars in + let xprs = + if varssize = 1 then + let var = List.hd vars in + let extxprs = condfloc#inv#get_external_exprs var in + let extxprs = + List.map (fun e -> substitute_expr (fun _ -> e) expr) extxprs in + expr :: extxprs + else if varssize = 2 then + let varlist = vars in + let var1 = List.nth varlist 0 in + let var2 = List.nth varlist 1 in + let extxprs1 = condfloc#inv#get_external_exprs var1 in + let extxprs2 = condfloc#inv#get_external_exprs var2 in + let xprs = List.concat + (List.map + (fun e1 -> + List.map + (fun e2 -> + substitute_expr + (fun w -> if w#equal var1 then e1 else e2) expr) + extxprs2) + extxprs1) in + expr :: xprs + else + [expr] in + List.concat (List.map convert_to_chif xprs) in + let make_asserts exprs = + List.concat (List.map convert_to_assert exprs) in + let make_branch_assert exprs = + let commands = List.map convert_to_assert exprs in + [BRANCH (List.map LF.mkCode commands)] in + let make_assert expr = convert_to_assert expr in + let make_test_code expr = + if is_conjunction expr then + let conjuncts = get_conjuncts expr in + make_asserts conjuncts + else if is_disjunction expr then + let disjuncts = get_disjuncts expr in + make_branch_assert disjuncts + else + make_assert expr in + match optboolxpr with + Some bbxpr -> + let bxpr = simplify_xpr bbxpr in + let thencode = make_test_code bxpr in + let elsecode = make_test_code (simplify_xpr (XOp (XLNot, [bxpr]))) in + (frozenVars, Some (thencode, elsecode)) + | _ -> + (frozenVars, None) + + +let make_tests + ~(condinstr:arm_assembly_instruction_int) + ~(testinstr:arm_assembly_instruction_int) + ~(condloc:location_int) + ~(testloc:location_int) = + let testfloc = get_floc testloc in + let condfloc = get_floc condloc in + let env = testfloc#f#env in + let reqN () = env#mk_num_temp in + let reqC i = env#request_num_constant i in + let (frozenVars, optboolxpr, _) = + make_conditional_predicate ~condinstr ~testinstr ~condloc ~testloc in + + let _ = + if testsupport#requested_arm_conditional_expr then + testsupport#submit_arm_conditional_expr condinstr testinstr optboolxpr in + + let convert_to_chif ?(high=true) expr = + let vars = variables_in_expr expr in + let varscmds = + if high then + condfloc#get_vardef_commands ~usehigh:vars condloc#ci + else + condfloc#get_vardef_commands ~use:vars condloc#ci in + let (cmds, bxpr) = xpr_to_boolexpr reqN reqC expr in + cmds @ varscmds @ [ASSERT bxpr] in + let convert_to_assert expr = + let vars = variables_in_expr expr in + let varssize = List.length vars in + let xprs = + if varssize = 1 then + let var = List.hd vars in + let extxprs = condfloc#inv#get_external_exprs var in + let extxprs = + List.map (fun e -> substitute_expr (fun _ -> e) expr) extxprs in + match extxprs with + | [] -> [expr] + | _ -> extxprs + else if varssize = 2 then + let varlist = vars in + let var1 = List.nth varlist 0 in + let var2 = List.nth varlist 1 in + let extxprs1 = condfloc#inv#get_external_exprs var1 in + let extxprs2 = condfloc#inv#get_external_exprs var2 in + let xprs = List.concat + (List.map + (fun e1 -> + List.map + (fun e2 -> + substitute_expr + (fun w -> if w#equal var1 then e1 else e2) expr) + extxprs2) + extxprs1) in + expr :: xprs + else + [expr] in + let _ = + if testsupport#requested_chif_conditionxprs then + testsupport#submit_chif_conditionxprs condinstr testinstr xprs in + let basic_asserts = convert_to_chif ~high:false (List.hd xprs) in + let rewritten_asserts = List.concat (List.map convert_to_chif (List.tl xprs)) in + basic_asserts @ rewritten_asserts in + + let make_asserts exprs = + let _ = env#start_transaction in + let commands = List.concat (List.map convert_to_assert exprs) in + let const_assigns = env#end_transaction in + const_assigns @ commands in + let make_branch_assert exprs = + let _ = env#start_transaction in + let commands = List.map convert_to_assert exprs in + let branch = BRANCH (List.map LF.mkCode commands) in + let const_assigns = env#end_transaction in + const_assigns @ [branch] in + let make_assert expr = + let _ = env#start_transaction in + let commands = convert_to_assert expr in + let const_assigns = env#end_transaction in + const_assigns @ commands in + let make_test_code expr = + if is_conjunction expr then + let conjuncts = get_conjuncts expr in + make_asserts conjuncts + else if is_disjunction expr then + let disjuncts = get_disjuncts expr in + make_branch_assert disjuncts + else + make_assert expr in + match optboolxpr with + Some bbxpr -> + let bxpr = simplify_xpr bbxpr in + let thencode = make_test_code bxpr in + let elsecode = make_test_code (simplify_xpr (XOp (XLNot, [bxpr]))) in + (frozenVars, Some (thencode, elsecode)) + | _ -> (frozenVars, None) + + +(* Returns the CHIF code for a conditional branch instruction that + incorporates the full condition as part of the instruction (i.e. no + dependency on a separate test instruction), such as CBZ or CBNZ. + + The CHIF code consists of a tuple of two sequences of CHIF commands. + The first sequence is the CHIF for the then test, the second sequence + is the CHIF for the else test. + + If the condition cannot be converted to CHIF SKIP commands are + returned, that is, the conditional branch is effectively turned into + a nondeterminstic branch. + *) +let make_local_tests + (condinstr: arm_assembly_instruction_int) + (condloc: location_int): (cmd_t list * cmd_t list) = + let floc = get_floc condloc in + let env = floc#f#env in + let reqN () = env#mk_num_temp in + let reqC i = env#request_num_constant i in + let boolxpr_r = + match condinstr#get_opcode with + | CompareBranchZero (op, _) -> + TR.tmap + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (fun x -> XOp (XEq, [x; zero_constant_expr])) + (op#to_expr floc) + | CompareBranchNonzero (op, _) -> + TR.tmap + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (fun x -> XOp (XNe, [x; zero_constant_expr])) + (op#to_expr floc) + | _ -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Unexpected condition: " ^ (p2s condinstr#toPretty)] in + + let convert_to_chif expr = + let vars = variables_in_expr expr in + let defcmds = floc#get_vardef_commands ~usehigh:vars floc#l#ci in + let (cmds, bxpr) = xpr_to_boolexpr reqN reqC expr in + cmds @ defcmds @ [ASSERT bxpr] in + let make_assert x = + let _ = env#start_transaction in + let commands = convert_to_chif x in + let const_assigns = env#end_transaction in + const_assigns @ commands in + TR.tfold + ~ok:(fun boolxpr -> + let thencode = make_assert boolxpr in + let elsecode = make_assert (simplify_xpr (XOp (XLNot, [boolxpr]))) in + (thencode, elsecode)) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ e; + ([SKIP], [SKIP]) + end) + boolxpr_r + + +let make_local_condition + (condinstr: arm_assembly_instruction_int) + (condloc: location_int) + (blocklabel: symbol_t) + (thenaddr: ctxt_iaddress_t) + (elseaddr: ctxt_iaddress_t) = + let thenlabel = make_code_label thenaddr in + let elselabel = make_code_label elseaddr in + let (thentest, elsetest) = make_local_tests condinstr condloc in + let make_node_and_label testcode tgtaddr modifier = + let src = condloc#i in + let nextlabel = make_code_label ~src ~modifier tgtaddr in + let transaction = TRANSACTION (nextlabel, LF.mkCode testcode, None) in + (nextlabel, [transaction]) in + let (thentestlabel, thennode) = + make_node_and_label thentest thenaddr "then" in + let (elsetestlabel, elsenode) = + make_node_and_label elsetest elseaddr "else" in + let thenedges = + [(blocklabel, thentestlabel); (thentestlabel, thenlabel)] in + let elseedges = + [(blocklabel, elsetestlabel); (elsetestlabel, elselabel) ] in + ([(thentestlabel, thennode); (elsetestlabel, elsenode)], thenedges @ elseedges) + + +let make_condition + ?(thencode: (symbol_t * cmd_t list) option) + ?(elsecode: (symbol_t * cmd_t list) option) + ~(condinstr:arm_assembly_instruction_int) + ~(testinstr:arm_assembly_instruction_int) + ~(condloc:location_int) + ~(testloc:location_int) + ~(blocklabel:symbol_t) + ~(thenaddr:ctxt_iaddress_t) + ~(elseaddr:ctxt_iaddress_t) + () = + let thenlabel = make_code_label thenaddr in + let elselabel = make_code_label elseaddr in + let (frozenVars, tests) = + make_tests ~condloc ~testloc ~condinstr ~testinstr in + match tests with + Some (thentest, elsetest) -> + let make_node_and_label testcode tgtaddr modifier = + let src = condloc#i in + let nextlabel = make_code_label ~src ~modifier tgtaddr in + let testcode = + testcode + @ (match frozenVars with + | [] -> [] + | _ -> [ABSTRACT_VARS frozenVars]) in + let transaction = TRANSACTION (nextlabel, LF.mkCode testcode, None) in + (nextlabel, [transaction]) in + let (thentestlabel, thennode) = + make_node_and_label thentest thenaddr "then" in + let (elsetestlabel, elsenode) = + make_node_and_label elsetest elseaddr "else" in + let thenbucket = + match thencode with + | Some (label, cmds) -> + [(label, [TRANSACTION (label, LF.mkCode cmds, None)])] + | _ -> [] in + let elsebucket = + match elsecode with + | Some (label, cmds) -> + [(label, [TRANSACTION (label, LF.mkCode cmds, None)])] + | _ -> [] in + let thenedges = + match thenbucket with + | [(thenbucketlabel, _)] -> + [(blocklabel, thenbucketlabel); + (thenbucketlabel, thentestlabel); + (thentestlabel, thenlabel)] + | _ -> + [(blocklabel, thentestlabel); (thentestlabel, thenlabel)] in + let elseedges = + match elsebucket with + | [(elsebucketlabel, _)] -> + [(blocklabel, elsebucketlabel); + (elsebucketlabel, elsetestlabel); + (elsetestlabel, elselabel)] + | _ -> + [(blocklabel, elsetestlabel); (elsetestlabel, elselabel) ] in + (thenbucket @ elsebucket @ [(thentestlabel, thennode); (elsetestlabel, elsenode)], + thenedges @ elseedges) + | _ -> + let abstractlabel = + make_code_label ~modifier:"abstract" testloc#ci in + let trcode = + match frozenVars with + | [] -> [SKIP] + | _ -> [ABSTRACT_VARS frozenVars] in + let transaction = + TRANSACTION (abstractlabel, LF.mkCode trcode, None) in + let edges = [ + (blocklabel, abstractlabel); + (abstractlabel, thenlabel); + (abstractlabel, elselabel)] in + ([(abstractlabel, [transaction])], edges) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMPredicateTest.mli b/CodeHawk/CHB/bchlibarm32/bCHARMPredicateTest.mli new file mode 100644 index 000000000..b43d47220 --- /dev/null +++ b/CodeHawk/CHB/bchlibarm32/bCHARMPredicateTest.mli @@ -0,0 +1,157 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2026 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 + in the Software without restriction, including without limitation the rights + 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 + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chlib *) +open CHLanguage + +(* xprlib *) +open XprTypes + +(* bchlib *) +open BCHLibTypes + +(* bchlibarm32 *) +open BCHARMTypes + +(** Functions to construct the branch conditions for conditional jumps and + predicated instructions *) + + +(** Given a condition instruction (e.g., BEQ) with its location and a test + instruction (e.g., CMP) with its location, [make_conditional_predicate] + returns a tuple consisting of: + - a list of temporary variables created to preserve the (frozen) values + at the test location [testloc] for the location of the conditional, + [condloc]. + - the predicate that expresses the joint condition of test and condition + code, e.g., CMP X, Y with EQ produces X = Y. + - a list of the operands used in the creation of the predicate, to be used + in determining use location in def-use analysis. + + Side effect: + If a predicate expression can be constructed, that expression is registered + with the [floc] for the condition location, from where it can be retrieved + later for xdata reporting. The pairs of register variables with their + associated frozen values are registered with [floc] for the test location. + *) +val make_conditional_predicate: + condinstr:arm_assembly_instruction_int + -> testinstr:arm_assembly_instruction_int + -> condloc:location_int + -> testloc:location_int + -> (variable_t list * xpr_t option * arm_operand_int list) + + +(** [make_instr_local_tests] calls [make_conditional_predicate] to create a + predicate expression (with the same side effect as above) and converts + the predicate expression to CHIF code: one set of asserts for the then + branch and one set of asserts for the else branch. The list of frozen + variables created by [make_conditional_predicate] is returned as well. + + CHIF asserts are limited to atomic conditions like X op Y (e.g., X < Y), + and thus expressions must be decomposed. At present there is only one + level of decomposition into disjuncts and conjuncts. Disjuncts give rise + to BRANCH constructs (which in practice do not strengthen the downstream + invariant due to their immediate join) and conjuncts, which individually + strengthen the downstream invariant. More complex expressions are not + currently represented, and result in RANDOM asserts. + + [make_instr_local_tests] is only used for predicated instructions other + than branch instructions. + *) +val make_instr_local_tests: + condinstr:arm_assembly_instruction_int + -> testinstr:arm_assembly_instruction_int + -> condloc:location_int + -> testloc:location_int + -> variable_t list * (cmd_t list * cmd_t list) option + + +(** [make_local_condition instr loc label thenaddr elseaddr] returns + a list of CFG nodes and edges for a conditional jump instruction, [instr] + that incorporates the full condition as part of the instruction itself + (i.e., there is no dependency on a separate test instruction), such as + CBZ (CompareBranchZer) or CBNZ). + + Two CFG nodes are created: a 'then' node with the then-test and an 'else' + node with the else-test. Four CFG edges are created: (1) from block label + [label] to thennode, (2) from block label [label] to elsenode, (3) from + thennode to the CFG jump target address, [thenaddr], and (4) from elsenode + to the CFG fall-through address, [elseaddr]. + *) +val make_local_condition: + arm_assembly_instruction_int + -> location_int + -> symbol_t + -> ctxt_iaddress_t + -> ctxt_iaddress_t + -> ((symbol_t * cmd_t list) list) * (symbol_t * symbol_t) list + + +(** Returns the control-flow graph nodes and edges of a conditional branch or an + IfThen instruction that is handled with full control flow rather than with an + aggregate. It applies to conditional branches in which the test is performed + by a separate instruction (the test instruction) and the branch condition + is determined by the combination of the test instruction and the condition + code that is part of the branch instruction (or IfThen). + + If a conditional predicate for the branch can be synthesized and converted into + CHIF, a 'then node' with the then-test and an 'else node' with the else-test + are created. In both nodes the temporary variables that were created to carry + the frozen values are abstracted to avoid unnecessary propagation of variables + that will never be used again. Four edges are created: (1) from block-label + to thenblock, (2) from thenblock to the cfg target jump address, (3) from + block-label to elseblock, and (4) from elseblock to the cfg fall-through + instruction. + + If a conditional predicate for the branch cannot be constructed the control flow + components created represent a non-deterministic branch. One node is + constructed, to abstract the temporary variables created by the attempt to + create a condition. Three edges are created: (1) from block-label to the new + node, (2) from the new node to the cfg target jump address, and (3) from the new + node to the cfg fall-through instruction. + + The optional arguments [thencode] and [elsecode] are prefixed to the code in + the thenblock and elseblock, resp. This code is the code generated for + predicated instructions that precede the jump and whose predicate coincides + with the respective predicates for the thenblock and elseblock. This code + is transferred from the source block to the thenblock/elseblock, prefixing + the thentest/elsetest code. The generation of the [thencode] and [elsecode] + is managed by [bCHPredicatedFragment]. +*) +val make_condition: + ?thencode:(symbol_t * cmd_t list) + -> ?elsecode:(symbol_t * cmd_t list) + -> condinstr:arm_assembly_instruction_int + -> testinstr:arm_assembly_instruction_int + -> condloc:location_int + -> testloc:location_int + -> blocklabel:symbol_t + -> thenaddr:ctxt_iaddress_t + -> elseaddr:ctxt_iaddress_t + -> unit + -> ((symbol_t * cmd_t list) list) * (symbol_t * symbol_t) list From 5e144f72e180c75ac32a062d3b520d53bd49e2d9 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 8 Sep 2026 13:07:20 -0700 Subject: [PATCH 13/22] CHB:ARM: move construction of predicated fragments to separate file --- .../bchlibarm32/bCHARMPredicatedFragment.ml | 350 ++++++++++++++++++ .../bchlibarm32/bCHARMPredicatedFragment.mli | 250 +++++++++++++ 2 files changed, 600 insertions(+) create mode 100644 CodeHawk/CHB/bchlibarm32/bCHARMPredicatedFragment.ml create mode 100644 CodeHawk/CHB/bchlibarm32/bCHARMPredicatedFragment.mli diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMPredicatedFragment.ml b/CodeHawk/CHB/bchlibarm32/bCHARMPredicatedFragment.ml new file mode 100644 index 000000000..b558bfc19 --- /dev/null +++ b/CodeHawk/CHB/bchlibarm32/bCHARMPredicatedFragment.ml @@ -0,0 +1,350 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2026 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 + in the Software without restriction, including without limitation the rights + 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 + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chlib *) +open CHLanguage + +(* chutil *) +open CHLogger + +(* bchlib *) +open BCHLibTypes +open BCHLocation + +(* bchlibarm32 *) +open BCHARMAssemblyInstructions +open BCHARMOpcodeRecords +open BCHARMDisassemblyUtils +open BCHARMPredicateTest +open BCHARMTranslationUtil +open BCHARMTypes + + +module LF = CHOnlineCodeSet.LanguageFactory + +let p2s = CHPrettyUtil.pretty_to_string + +(* ------------------------------------------------------------------ cmdstate_t + Data structure and associated functions for the collection of commands inside + a basic block. The data structure allows for a refinement of the otherwise + linear sequence of commands, to enable a representation of predicated + instructions that result in increased precision of analysis results, due to + the collection of instructions with equal predicate in separate branches, + rather than having a single branch instruction per predicated instruction + with intervening joins. + *) + + +type setter_key_t = { + sk_testloc: ctxt_iaddress_t; + sk_testtestloc: ctxt_iaddress_t option + } + +type fragment_t = { + fr_key: setter_key_t; + fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) + fr_openerloc: location_int; (* location of first instr in fragment *) + fr_thenbucket: cmd_t list; (* starts with thentest, grows by append *) + fr_elsebucket: cmd_t list (* starts with elsetest *) + } + +type cmdstate_t = { + cs_flat: cmd_t list; (* closed-out cmds, in order *) + cs_open: fragment_t option (* at most one open fragement *) + } + + +let setter_key_to_string (key: setter_key_t) = + match key.sk_testtestloc with + | Some a -> "skey:(" ^ key.sk_testloc ^ ", " ^ a ^ ")" + | _ -> "skey:" ^ key.sk_testloc + + +let get_setter_key + (finfo: function_info_int) + (testloc: location_int) + (testinstr: arm_assembly_instruction_int): setter_key_t = + let sk_testtestloc = + if is_opcode_conditional testinstr#get_opcode then + match get_associated_test_instr finfo testloc#ci with + | Some (testtestloc, _) -> Some testtestloc#ci + | None -> + let _ = + log_error_result + ~tag:"get_setter_key:Unable to get test-test-loc" + ~msg:testloc#ci + __FILE__ __LINE__ + [testinstr#toString] in + None + else + None in + {sk_testloc = testloc#ci; sk_testtestloc} + + +let get_setter_key_at + (finfo: function_info_int) + (ctxtiaddr: ctxt_iaddress_t) + : (setter_key_t * arm_assembly_instruction_int * location_int) option = + match get_associated_test_instr finfo ctxtiaddr with + | None -> None + | Some (testloc, testinstr) -> + Some (get_setter_key finfo testloc testinstr, testinstr, testloc) + + +let cmdstate_start: cmdstate_t = {cs_flat = []; cs_open = None} + + +(* Close cs_open (if any) into one BRANCH appended to cs_flat *) +let cmdstate_flush (finfo: function_info_int) (cs: cmdstate_t): cmdstate_t = + match cs.cs_open with + | None -> cs + | Some fr -> + let frozenAsserts = get_frozen_asserts finfo fr.fr_openerloc#ci in + let openerinvop = get_invariant_operation fr.fr_openerloc in + let branch = + BRANCH [LF.mkCode fr.fr_thenbucket; LF.mkCode fr.fr_elsebucket] in + {cs_flat = cs.cs_flat @ frozenAsserts @ [openerinvop; branch]; cs_open = None} + + +(* Extend cmdstate with the cmds for an unconditional / condition-covered + instruction: closes any open fragment, and appends the already wrapped + unit cmds *) +let cmdstate_append_linear + (finfo: function_info_int) (cs: cmdstate_t) (unit_cmds: cmd_t list): cmdstate_t = + let cs = cmdstate_flush finfo cs in + {cs with cs_flat = cs.cs_flat @ unit_cmds} + + +let cmdstate_append_predicated + (finfo: function_info_int) + (cs: cmdstate_t) + ~(key: setter_key_t) + ~(cc: arm_opcode_cc_t) + ~(openerloc: location_int) + ~(thentest: cmd_t list) + ~(elsetest: cmd_t list) + ~(unit_cmds: cmd_t list): cmdstate_t = + let _ = + log_diagnostics_result + ~tag:"cmdstate_append_predicated" + ~msg:openerloc#ci + __FILE__ __LINE__ + ["key: " ^ (setter_key_to_string key); + "thentest: " ^ (p2s (chif_cmds_to_pretty thentest))] in + match cs.cs_open with + | Some fr when fr.fr_key = key && cc = fr.fr_opencc -> + {cs with cs_open = + Some {fr with fr_thenbucket = fr.fr_thenbucket @ unit_cmds}} + | Some fr when fr.fr_key = key && Some cc = get_inverse_cc fr.fr_opencc -> + {cs with cs_open = + Some {fr with fr_elsebucket = fr.fr_elsebucket @ unit_cmds}} + | Some fr when fr.fr_openerloc#ci = key.sk_testloc + && (cc = fr.fr_opencc || Some cc = get_inverse_cc fr.fr_opencc) -> + let frozenAsserts = get_frozen_asserts finfo fr.fr_openerloc#ci in + let openerinvop = get_invariant_operation fr.fr_openerloc in + let cs = {cs_flat = cs.cs_flat @ frozenAsserts @ [openerinvop]; cs_open = None} in + if cc = fr.fr_opencc then + {cs with cs_open = + Some {fr_key = key; fr_opencc = cc; fr_openerloc = openerloc; + fr_thenbucket = thentest @ fr.fr_thenbucket @ unit_cmds; + fr_elsebucket = elsetest}} + else + {cs with cs_open = + Some {fr_key = key; fr_opencc = fr.fr_opencc; + fr_openerloc = openerloc; + fr_thenbucket = thentest @ fr.fr_thenbucket; + fr_elsebucket = elsetest @ unit_cmds}} + | _ -> + let cs = cmdstate_flush finfo cs in + (* elsebucket is set to [], to avoid adding an ASSERT that must be weakened + later, as in CMP / CMPNE / BNE *) + {cs with + cs_open = + Some {fr_key = key; + fr_opencc = cc; + fr_openerloc = openerloc; + fr_thenbucket = thentest @ unit_cmds; + fr_elsebucket = []}} + + +(* Block end (no terminating conditional branch): flush and linearlize for + package transaction *) +let cmdstate_finish (finfo: function_info_int) (cs: cmdstate_t): cmd_t list = + (cmdstate_flush finfo cs).cs_flat + + +(* Terminator hookup: if the terminator's own setter_key_t matches the still + open fragment, hand the fragment's buckets to make_condtiion instead of + flushing them into an intra-block BRANCH; otherwise close the branch first.*) +let cmdstate_take_for_terminator + (finfo: function_info_int) + (cs: cmdstate_t) + ~(key: setter_key_t) + ~(cc: arm_opcode_cc_t): cmd_t list * cmd_t list * cmd_t list = + match cs.cs_open with + | Some fr when fr.fr_key = key && cc = fr.fr_opencc -> + let frozenAsserts = get_frozen_asserts finfo fr.fr_openerloc#ci in + let openerinvop = get_invariant_operation fr.fr_openerloc in + (cs.cs_flat @ frozenAsserts @ [openerinvop], fr.fr_thenbucket, fr.fr_elsebucket) + + | Some fr when fr.fr_key = key && Some cc = get_inverse_cc fr.fr_opencc -> + let frozenAsserts = get_frozen_asserts finfo fr.fr_openerloc#ci in + let openerinvop = get_invariant_operation fr.fr_openerloc in + (cs.cs_flat @ frozenAsserts @ [openerinvop], fr.fr_elsebucket, fr.fr_thenbucket) + + | Some fr when fr.fr_openerloc#ci = key.sk_testloc + && (cc = fr.fr_opencc || Some cc = get_inverse_cc fr.fr_opencc) -> + let frozenAsserts = get_frozen_asserts finfo fr.fr_openerloc#ci in + let openerinvop = get_invariant_operation fr.fr_openerloc in + let _ = + log_diagnostics_result + ~tag:"cmdstate_take_for_terminator" + ~msg:fr.fr_openerloc#ci + __FILE__ __LINE__ + ["thenbucket: " ^ (p2s (chif_cmds_to_pretty fr.fr_thenbucket)); + "elsebucket: " ^ (p2s (chif_cmds_to_pretty fr.fr_elsebucket))] in + if cc = fr.fr_opencc then + (cs.cs_flat @ frozenAsserts @ [openerinvop], fr.fr_thenbucket, fr.fr_elsebucket) + else + (cs.cs_flat @ frozenAsserts @ [openerinvop], fr.fr_elsebucket, fr.fr_thenbucket) + | _ -> + (cmdstate_finish finfo cs, [], []) + + +let package_terminator_transactions + (finfo: function_info_int) + (blocklabel: symbol_t) + (cmds: cmd_t list) + (thencode: cmd_t list) + (elsecode: cmd_t list) + : (cmd_t + * (symbol_t * cmd_t list) option + * (symbol_t * cmd_t list) option) = + let cnstAssigns = finfo#env#end_transaction in + let cmds = List.filter (fun cmd -> match cmd with SKIP -> false | _ -> true) cmds in + let transaction = TRANSACTION (blocklabel, LF.mkCode (cnstAssigns @ cmds), None) in + let mk cl suffix = + match cl with + | [] -> None + | _ -> + let cl = List.filter (fun c -> match c with SKIP -> false | _ -> true) cl in + let label = + let atts = blocklabel#getAttributes in + let atts = if suffix = "" then atts else atts @ [suffix] in + new symbol_t ~atts blocklabel#getBaseName in + Some (label, [TRANSACTION (label, LF.mkCode (cnstAssigns @ cl), None)]) in + (transaction, mk thencode "thenbucket", mk elsecode "elsebucket") + + +let append_predicated_instruction + (finfo: function_info_int) + (cmdstate: cmdstate_t) + ~(instr: arm_assembly_instruction_int) + ~(loc: location_int) + ~(cc: arm_opcode_cc_t) + ~(build_unit:(cmd_t list -> cmd_t list)) + ~(cmds: cmd_t list): cmdstate_t = + let ctxtiaddr = loc#ci in + let frozenAsserts = get_frozen_asserts finfo ctxtiaddr in + let default newcmds = + let invop = get_invariant_operation loc in + let newcmds = frozenAsserts @ (invop :: (build_unit newcmds)) in + cmdstate_append_linear finfo cmdstate newcmds in + + if instr#is_condition_covered then + default cmds + + else + match get_associated_test_instr finfo ctxtiaddr with + | Some (testloc, testinstr) -> + let (_, tests) = + make_instr_local_tests + ~condloc:loc ~testloc ~condinstr:instr ~testinstr in + if has_false_condition_context ctxtiaddr then + (match tests with + | Some (_, elsetest) -> default elsetest + | _ -> default []) + else if has_true_condition_context ctxtiaddr then + (match tests with + | Some (thentest, _) -> default (thentest @ cmds) + | _ -> default cmds) + else + let key = get_setter_key finfo testloc testinstr in + let (thentest, elsetest) = + match tests with + | Some (t, e) -> (t, e) + | _ -> ([], []) in + (match cmdstate.cs_open with + | Some fr when (fr.fr_key = key) + && (cc = fr.fr_opencc + || get_inverse_cc fr.fr_opencc = Some cc) -> + let invop = get_invariant_operation loc in + let unit_cmds = frozenAsserts @ (invop :: (build_unit cmds)) in + let fmem = + {fmem_openerloc = fr.fr_openerloc; + fmem_bucket = if cc = fr.fr_opencc then FragThen else FragElse} in + begin + finfo#set_fragment_membership ctxtiaddr fmem; + cmdstate_append_predicated + finfo cmdstate + ~key ~cc ~openerloc:fr.fr_openerloc ~thentest:[] ~elsetest:[] ~unit_cmds + end + + | Some fr when (fr.fr_openerloc#ci = key.sk_testloc) + && (cc = fr.fr_opencc + || get_inverse_cc fr.fr_opencc = Some cc) -> + let unit_cmds = frozenAsserts @ (build_unit cmds) in + let fmem = + {fmem_openerloc = loc; + fmem_bucket = if cc = fr.fr_opencc then FragThen else FragElse} in + begin + finfo#set_fragment_membership ctxtiaddr fmem; + cmdstate_append_predicated + finfo cmdstate ~key ~cc ~openerloc:loc ~thentest ~elsetest ~unit_cmds + end + + | _ -> + let unit_cmds = frozenAsserts @ (build_unit cmds) in + let fmem = {fmem_openerloc = loc; fmem_bucket = FragThen} in + begin + finfo#set_fragment_membership ctxtiaddr fmem; + cmdstate_append_predicated + finfo cmdstate ~key ~cc ~openerloc:loc ~thentest ~elsetest ~unit_cmds + end) + | _ -> + if has_false_condition_context ctxtiaddr then + default [] + else if has_true_condition_context ctxtiaddr then + default cmds + else + let _ = + log_diagnostics_result + ~tag:"append_predicated_instruction:no associated test" + ~msg:ctxtiaddr + __FILE__ __LINE__ + [] in + default [BRANCH [LF.mkCode cmds; LF.mkCode [SKIP]]] diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMPredicatedFragment.mli b/CodeHawk/CHB/bchlibarm32/bCHARMPredicatedFragment.mli new file mode 100644 index 000000000..ba152d9d9 --- /dev/null +++ b/CodeHawk/CHB/bchlibarm32/bCHARMPredicatedFragment.mli @@ -0,0 +1,250 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2026 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 + in the Software without restriction, including without limitation the rights + 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 + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chlib *) +open CHLanguage + +(* bchlib *) +open BCHLibTypes + +(* bchlibarm32 *) +open BCHARMTypes + + +(** Data structure and associated functions for the collection of predicated + instructions into positive and negative branches within a basic block. + + The data structure allows for a refinement of the otherwise linear + sequence of commands in a basic block, into internal branches with + sequences of instructions with the same polarity to avoid joins after every + predicated instruction. + + Sequences of code split by polarity are called fragments. Fragments are + constructed incrementally during translation, one instruction at a time, + their bucket selected by the polarity of the instruction relative to the + polarity of the opener instruction (the first instruction after the test + instruction. + + {b Example 1:} + + The basic block + + {v + 0x1e0ec 00 00 56 e3 CMP R6, #0 + 0x1e0f0 01 b0 8b 02 ADDEQ R11, R11, #1 + 0x1e0f4 06 b0 a0 11 MOVNE R11, R6 + 0x1e0f8 02 80 a0 11 MOVNE R8, R2 + 0x1e0fc 00 00 55 e3 CMP R5, #0 + 0x1e100 04 30 85 10 ADDNE R3, R5, R4 + 0x1e104 00 60 a0 13 MOVNE R6, #0 + 0x1e108 05 60 a0 01 MOVEQ R6, R5 + 0x1e10c 20 20 a0 13 MOVNE R2, #0x20 + 0x1e110 01 20 43 15 STRBNE R2, [R3,-#1] + v} + + would give rise to two fragments within one basic block: + + {v + fragment 1: + setter_key: 0x1e0ec, None + opencc : EQ + thenbucket: [0x1e0f0] + elsebucket: [0x1e0f4; 0x1e0f8] + + fragment 2: + setter_key: 0x1e0fc, None + opencc : NE + thenbucket: [0x1e100; 0x1e104; 0x1010c; 0x1e110] + elsebucket: [0x1e108] + v} + + If a basic block containing one or more fragments ends in a conditional + jump with the same setter_key as the last fragment, as in, e.g., + + {b Example 2:} + + {v + 0x1e2c0 00 20 a0 e3 MOV R2, #0 + 0x1e2c4 02 00 56 e1 CMP R6, R2 + 0x1e2c8 00 20 c3 e5 STRB R2, [R3] + 0x1e2cc 06 70 a0 11 MOVNE R7, R6 + 0x1e2d0 06 b0 a0 11 MOVNE R11, R6 + 0x1e2d4 e8 ff ff 0a BEQ 0x1e27c + v} + + the branch instruction is hoisted just before the opener location (in this + example just before 0x1e2cc) and the then bucket and else bucket of the + fragment are, conceptually, added to the respective successor blocks, + according to their polarity. In the above example, the instructions at + 0x1e2cc and 0x1e2d0 are added to the else block, that is, the block starting + at 0x1e2d8, effectively connecting the instruction at 0x1e2cc directly to + the then block. Note that there is no join between 0x1e2d0 and 0x1e2d4 in + this case. + *) + +(** location of the test instruction of a fragment. If the test instruction itself + is predicated (e.g., CMPNE), the [sk_testtestloc] contains the location of the + test associated with that predicate, otherwise this field is [None]. + + Note that the chain of test instructions is limited to two instructions. + *) +type setter_key_t = { + sk_testloc: ctxt_iaddress_t; + sk_testtestloc: ctxt_iaddress_t option + } + +(** data structure that represents a sequence of predicated instructions that all + depend on the same test instruction (or test instructions, in case of a chained + test instruction). The openerloc is the location of the first instruction + after the test (or tests), whose condition code (fr_opencc) determines the + polarity of the thenbucket. The thenbucket and elsebucket contain the commands + associated with the predicated instructions of the respective polarity. + *) +type fragment_t = { + fr_key: setter_key_t; + fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) + fr_openerloc: location_int; (* location of first instr in fragment *) + fr_thenbucket: cmd_t list; (* starts with thentest, grows by append *) + fr_elsebucket: cmd_t list (* starts with elsetest *) + } + +(** data structure that captures the current state of the translation, with at + most one open fragment; cs_flat contains all closed_out commands, in order, + including both unpredicated instructions and fragments of predicated + instructions now closed. + *) +type cmdstate_t = { + cs_flat: cmd_t list; + cs_open: fragment_t option + } + + +(** [get_setter_key finfo testloc testinstr] returns a setter_key with the + address of [testloc]. If the instruction [testinstr] at [testloc] is + itself predicated, the function will attempt to retrieve the location of + the test instruction for that predicated. If successful, this location + will be added as sk_testtestloc. If not successful, the location will be + set to [None] and a message is added to the error log. + *) +val get_setter_key: + function_info_int + -> location_int + -> arm_assembly_instruction_int + -> setter_key_t + + +(** [get_setter_key_at finfo addr] returns the setter key that is associated + with the predicated instruction at [addr], together with the test instruction + and location of the test instruction. [None] is returned if no associated + test instruction can be found. + *) +val get_setter_key_at: + function_info_int + -> ctxt_iaddress_t + -> (setter_key_t * arm_assembly_instruction_int * location_int) option + + +(** constant cmdstate_t object with cs_flat empty and cs_open [None].*) +val cmdstate_start: cmdstate_t + + +(** Closes cs_open (if any) into one BRANCH and adds it to cs_flat. Returns + a new cmdstate_t object with the updated cs_flat, and cs_open set to + [None]. + *) +val cmdstate_flush: function_info_int -> cmdstate_t -> cmdstate_t + + +(** [cmdstate_append_linear finfo cmdstate cmds] flushes [cmdstate], adds + the [cmds] for a non-predicated instruction (or a predicated instruction + that is part of an aggregate) to cs_flat, and returns the updated [cmdstate]. + *) +val cmdstate_append_linear: + function_info_int -> cmdstate_t -> cmd_t list -> cmdstate_t + + +(** [cmdstate_append_predicated] adds a predicated instruction to [cmdstate]. + - If [cmdstate] does not have an open fragment (cs_open is [None]), a new + fragment is created with the given [key], [cc], and openerloc, and the + [thentest] and [unit_cmds] are added to the thenbucket. + - If an open fragment with the same key and cc flavor as the opencc (the cc + are the same or each other inverse), the [unit_cmds] are added to the + thenbucket if cc equals opencc, and to the elsebucket otherwise. + - If an open fragment exists whose openerloc is the same as the testloc of + the instruction to be added (i.e., the openerloc of the open fragment + belongs to a predicated test instruction), the openerloc of the open fragment + is changed to the location of the instruction to be added and the opencc is + set to the cc of the new instruction. + *) +val cmdstate_append_predicated: + function_info_int + -> cmdstate_t + -> key:setter_key_t + -> cc:arm_opcode_cc_t + -> openerloc:location_int + -> thentest:cmd_t list + -> elsetest:cmd_t list + -> unit_cmds:cmd_t list + -> cmdstate_t + + +(** flushes the [cmdstate] and returns the linearized command list from cs_flat + from the resulting cmdstate. [cmdstate_finish] is called at the end of a + basic block without terminating conditional branch. + *) +val cmdstate_finish: function_info_int -> cmdstate_t -> cmd_t list + + + +val cmdstate_take_for_terminator: + function_info_int + -> cmdstate_t + -> key:setter_key_t + -> cc:arm_opcode_cc_t + -> cmd_t list * cmd_t list * cmd_t list + + +val package_terminator_transactions: + function_info_int + -> symbol_t + -> cmd_t list + -> cmd_t list + -> cmd_t list + -> (cmd_t + * (symbol_t * cmd_t list) option + * (symbol_t * cmd_t list) option) + + +val append_predicated_instruction: + function_info_int + -> cmdstate_t + -> instr:arm_assembly_instruction_int + -> loc:location_int + -> cc: arm_opcode_cc_t + -> build_unit:(cmd_t list -> cmd_t list) + -> cmds:cmd_t list + -> cmdstate_t From 07953534a873a779404454e3af043a6488ffa48a Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 8 Sep 2026 13:09:01 -0700 Subject: [PATCH 14/22] CHB:ARM: update CHIF translation for predicated fragments --- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 716 +----------------- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.mli | 22 +- 2 files changed, 33 insertions(+), 705 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 34c25a1f1..aae2184be 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -61,11 +61,11 @@ open BCHSystemInfo open BCHARMAssemblyInstructions open BCHARMCHIFSystem open BCHARMCodePC -open BCHARMConditionalExpr -open BCHARMDisassemblyUtils open BCHARMOpcodeRecords open BCHARMOperand -open BCHARMTestSupport +open BCHARMPredicatedFragment +open BCHARMPredicateTest +open BCHARMTranslationUtil open BCHARMTypes @@ -83,586 +83,6 @@ let log_error (tag: string) (msg: string): tracelogspec_t = let valueset_domain = "valuesets" -let make_code_label ?src ?modifier (address:ctxt_iaddress_t) = - let name = - if address = "exit" || address = "?" then - "exit" - else - "pc_" ^ address in - let atts = match modifier with - | Some s -> [s] - | _ -> [] in - let atts = - if address = "?" then - "unresolved-jump" :: atts - else - atts in - let atts = match src with - | Some s -> s#to_fixed_length_hex_string :: atts | _ -> atts in - ctxt_string_to_symbol name ~atts address - - -let get_invariant_label ?(bwd=false) (loc:location_int) = - if bwd then - ctxt_string_to_symbol "bwd_invariant" loc#ci - else - ctxt_string_to_symbol "invariant" loc#ci - - -let package_transaction - (finfo:function_info_int) (label:symbol_t) (cmds:cmd_t list) = - let cmds = - List.filter - (fun cmd -> match cmd with SKIP -> false | _ -> true) cmds in - let cnstAssigns = finfo#env#end_transaction in - TRANSACTION (label, LF.mkCode (cnstAssigns @ cmds), None) - - -(* ------------------------------------------------------------------ cmdstate_t - Data structure and associated functions for the collection of commands inside - a basic block. The data structure allows for a refinement of the otherwise - linear sequence of commands, to enable a representation of predicated - instructions that result in increased precision of analysis results, due to - the collection of instructions with equal predicate in separate branches, - rather than having a single branch instruction per predicated instruction - with intervening joins. - *) - -type setter_key_t = { - sk_testloc: ctxt_iaddress_t; - sk_testtestloc: ctxt_iaddress_t option - } - -type fragment_t = { - fr_key: setter_key_t; - fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) - fr_openerloc: location_int; (* location of first instr in fragment *) - fr_thenbucket: cmd_t list; (* starts with thentest, grows by append *) - fr_elsebucket: cmd_t list (* starts with elsetest *) - } - -type cmdstate_t = { - cs_flat: cmd_t list; (* closed-out cmds, in order *) - cs_open: fragment_t option (* at most one open fragement *) - } - - -let get_setter_key - (finfo: function_info_int) - (testloc: location_int) - (testinstr: arm_assembly_instruction_int): setter_key_t = - let sk_testtestloc = - if is_opcode_conditional testinstr#get_opcode then - match get_associated_test_instr finfo testloc#ci with - | Some (testtestloc, _) -> Some testtestloc#ci - | None -> - let _ = - log_error_result - ~tag:"get_setter_key:Unable to get test-test-loc" - ~msg:testloc#ci - __FILE__ __LINE__ - [testinstr#toString] in - None - else - None in - {sk_testloc = testloc#ci; sk_testtestloc} - -let get_setter_key_at - (finfo: function_info_int) - (ctxtiaddr: ctxt_iaddress_t) - : (setter_key_t * arm_assembly_instruction_int * location_int) option = - match get_associated_test_instr finfo ctxtiaddr with - | None -> None - | Some (testloc, testinstr) -> - Some (get_setter_key finfo testloc testinstr, testinstr, testloc) - - -let cmdstate_start: cmdstate_t = {cs_flat = []; cs_open = None} - -(* Close cs_open (if any) into one BRANCH appended to cs_flat *) -let cmdstate_flush (cs: cmdstate_t): cmdstate_t = - match cs.cs_open with - | None -> cs - | Some fr -> - let invlabel = get_invariant_label fr.fr_openerloc in - let openerinvop = OPERATION {op_name = invlabel; op_args = []} in - let branch = - BRANCH [LF.mkCode fr.fr_thenbucket; LF.mkCode fr.fr_elsebucket] in - {cs_flat = cs.cs_flat @ [openerinvop; branch]; cs_open = None} - -(* Extend cmdstate with the cmds for an unconditional / condition-covered - instruction: closes any open fragment, and appends the already wrapped - unit cmds *) -let cmdstate_append_linear - (cs: cmdstate_t) (unit_cmds: cmd_t list): cmdstate_t = - let cs = cmdstate_flush cs in - {cs with cs_flat = cs.cs_flat @ unit_cmds} - - -let cmdstate_append_predicated - (cs: cmdstate_t) - ~(key: setter_key_t) - ~(cc: arm_opcode_cc_t) - ~(openerloc: location_int) - ~(thentest: cmd_t list) - ~(elsetest: cmd_t list) - ~(unit_cmds: cmd_t list): cmdstate_t = - match cs.cs_open with - | Some fr when fr.fr_key = key && cc = fr.fr_opencc -> - {cs with cs_open = - Some {fr with fr_thenbucket = fr.fr_thenbucket @ unit_cmds}} - | Some fr when fr.fr_key = key && Some cc = get_inverse_cc fr.fr_opencc -> - {cs with cs_open = - Some {fr with fr_elsebucket = fr.fr_elsebucket @ unit_cmds}} - | _ -> - let cs = cmdstate_flush cs in - {cs with - cs_open = - Some {fr_key = key; - fr_opencc = cc; - fr_openerloc = openerloc; - fr_thenbucket = thentest @ unit_cmds; - fr_elsebucket = elsetest}} - - -(* Block end (no terminating conditional branch): flush and linearlize for - package transaction *) -let cmdstate_finish (cs: cmdstate_t): cmd_t list = - (cmdstate_flush cs).cs_flat - - -(* Terminator hookup: if the terminator's own setter_key_t matches the still - open fragment, hand the fragment's buckets to make_condtiion instead of - flushing them into an intra-block BRANCH; otherwise close the branch first.*) -let cmdstate_take_for_terminator - (cs: cmdstate_t) - ~(key: setter_key_t) - ~(cc: arm_opcode_cc_t): cmd_t list * cmd_t list * cmd_t list = - match cs.cs_open with - | Some fr when fr.fr_key = key && cc = fr.fr_opencc -> - let invlabel = get_invariant_label fr.fr_openerloc in - let openerinvop = OPERATION {op_name = invlabel; op_args = []} in - (cs.cs_flat @ [openerinvop], fr.fr_thenbucket, fr.fr_elsebucket) - | Some fr when fr.fr_key = key && Some cc = get_inverse_cc fr.fr_opencc -> - let invlabel = get_invariant_label fr.fr_openerloc in - let openerinvop = OPERATION {op_name = invlabel; op_args = []} in - (cs.cs_flat @ [openerinvop], fr.fr_elsebucket, fr.fr_thenbucket) - | _ -> - (cmdstate_finish cs, [], []) - - -(* Returns the predicate instruction and associated info for a conditional, - in particular, it returns a tuple consisting of: - - a list of temporary variables created to preserve the (frozen) values - at the test location (testloc) for the location of the conditional (condloc) - - the predicate that expresses the joint condition of test and condition - code (cc, e.g., EQ), and - - a list of the operands used in the creation of the predicate - *) -let make_conditional_predicate - ~(condinstr: arm_assembly_instruction_int) - ~(testinstr: arm_assembly_instruction_int) - ~(condloc: location_int) - ~(testloc: location_int) = - let testfloc = get_floc testloc in - let get_default_conditional_expr () = - arm_conditional_expr - ~condopc:condinstr#get_opcode - ~testopc:testinstr#get_opcode - ~condloc:condloc - ~testloc:testloc in - if is_opcode_conditional testinstr#get_opcode then - let finfo = testfloc#f in - match get_associated_test_instr finfo testloc#ci with - | Some (testtestloc , testtestinstr) -> - arm_conditional_conditional_expr - ~condopc:condinstr#get_opcode - ~testopc:testinstr#get_opcode - ~testtestopc: testtestinstr#get_opcode - ~condloc - ~testloc - ~testtestloc - | _ -> - get_default_conditional_expr () - else - get_default_conditional_expr () - - -let make_instr_local_tests - ~(condinstr:arm_assembly_instruction_int) - ~(testinstr:arm_assembly_instruction_int) - ~(condloc:location_int) - ~(testloc:location_int) = - let testfloc = get_floc testloc in - let condfloc = get_floc condloc in - let env = testfloc#f#env in - let reqN () = env#mk_num_temp in - let reqC i = env#request_num_constant i in - let get_default_conditional_expr () = - arm_conditional_expr - ~condopc:condinstr#get_opcode - ~testopc:testinstr#get_opcode - ~condloc - ~testloc in - let (frozenVars, optboolxpr, _) = - if is_opcode_conditional testinstr#get_opcode then - let finfo = testfloc#f in - match get_associated_test_instr finfo testloc#ci with - | Some (testtestloc, testtestinstr) -> - arm_conditional_conditional_expr - ~condopc:condinstr#get_opcode - ~testopc: testinstr#get_opcode - ~testtestopc: testtestinstr#get_opcode - ~condloc - ~testloc - ~testtestloc - | _ -> - get_default_conditional_expr () - else - get_default_conditional_expr () in - - let convert_to_chif expr = - let (cmds,bxpr) = xpr_to_boolexpr reqN reqC expr in - cmds @ [ASSERT bxpr] in - let convert_to_assert expr = - let vars = variables_in_expr expr in - let varssize = List.length vars in - let xprs = - if varssize = 1 then - let var = List.hd vars in - let extxprs = condfloc#inv#get_external_exprs var in - let extxprs = - List.map (fun e -> substitute_expr (fun _ -> e) expr) extxprs in - expr :: extxprs - else if varssize = 2 then - let varlist = vars in - let var1 = List.nth varlist 0 in - let var2 = List.nth varlist 1 in - let extxprs1 = condfloc#inv#get_external_exprs var1 in - let extxprs2 = condfloc#inv#get_external_exprs var2 in - let xprs = List.concat - (List.map - (fun e1 -> - List.map - (fun e2 -> - substitute_expr - (fun w -> if w#equal var1 then e1 else e2) expr) - extxprs2) - extxprs1) in - expr :: xprs - else - [expr] in - List.concat (List.map convert_to_chif xprs) in - let make_asserts exprs = - List.concat (List.map convert_to_assert exprs) in - let make_branch_assert exprs = - let commands = List.map convert_to_assert exprs in - [BRANCH (List.map LF.mkCode commands)] in - let make_assert expr = - convert_to_assert expr in - let make_test_code expr = - if is_conjunction expr then - let conjuncts = get_conjuncts expr in - make_asserts conjuncts - else if is_disjunction expr then - let disjuncts = get_disjuncts expr in - make_branch_assert disjuncts - else - make_assert expr in - match optboolxpr with - Some bxpr -> - let thencode = make_test_code bxpr in - let elsecode = make_test_code (simplify_xpr (XOp (XLNot, [bxpr]))) in - (frozenVars, Some (thencode, elsecode)) - | _ -> (frozenVars, None) - - -let make_tests - ~(condinstr:arm_assembly_instruction_int) - ~(testinstr:arm_assembly_instruction_int) - ~(condloc:location_int) - ~(testloc:location_int) = - let testfloc = get_floc testloc in - let condfloc = get_floc condloc in - let env = testfloc#f#env in - let reqN () = env#mk_num_temp in - let reqC i = env#request_num_constant i in - let get_default_conditional_expr () = - arm_conditional_expr - ~condopc:condinstr#get_opcode - ~testopc:testinstr#get_opcode - ~condloc - ~testloc in - let (frozenVars, optboolxpr, _) = - if is_opcode_conditional testinstr#get_opcode then - let finfo = testfloc#f in - match get_associated_test_instr finfo testloc#ci with - | Some (testtestloc, testtestinstr) -> - arm_conditional_conditional_expr - ~condopc:condinstr#get_opcode - ~testopc: testinstr#get_opcode - ~testtestopc: testtestinstr#get_opcode - ~condloc - ~testloc - ~testtestloc - | _ -> - get_default_conditional_expr () - else - get_default_conditional_expr () in - - let _ = - if testsupport#requested_arm_conditional_expr then - testsupport#submit_arm_conditional_expr condinstr testinstr optboolxpr in - - let convert_to_chif ?(high=true) expr = - let vars = variables_in_expr expr in - let varscmds = - if high then - condfloc#get_vardef_commands ~usehigh:vars condloc#ci - else - condfloc#get_vardef_commands ~use:vars condloc#ci in - let (cmds, bxpr) = xpr_to_boolexpr reqN reqC expr in - cmds @ varscmds @ [ASSERT bxpr] in - let convert_to_assert expr = - let vars = variables_in_expr expr in - let varssize = List.length vars in - let xprs = - if varssize = 1 then - let var = List.hd vars in - let extxprs = condfloc#inv#get_external_exprs var in - let extxprs = - List.map (fun e -> substitute_expr (fun _ -> e) expr) extxprs in - match extxprs with - | [] -> [expr] - | _ -> extxprs - else if varssize = 2 then - let varlist = vars in - let var1 = List.nth varlist 0 in - let var2 = List.nth varlist 1 in - let extxprs1 = condfloc#inv#get_external_exprs var1 in - let extxprs2 = condfloc#inv#get_external_exprs var2 in - let xprs = List.concat - (List.map - (fun e1 -> - List.map - (fun e2 -> - substitute_expr - (fun w -> if w#equal var1 then e1 else e2) expr) - extxprs2) - extxprs1) in - expr :: xprs - else - [expr] in - let _ = - if testsupport#requested_chif_conditionxprs then - testsupport#submit_chif_conditionxprs condinstr testinstr xprs in - let basic_asserts = convert_to_chif ~high:false (List.hd xprs) in - let rewritten_asserts = List.concat (List.map convert_to_chif (List.tl xprs)) in - basic_asserts @ rewritten_asserts in - - let make_asserts exprs = - let _ = env#start_transaction in - let commands = List.concat (List.map convert_to_assert exprs) in - let const_assigns = env#end_transaction in - const_assigns @ commands in - let make_branch_assert exprs = - let _ = env#start_transaction in - let commands = List.map convert_to_assert exprs in - let branch = BRANCH (List.map LF.mkCode commands) in - let const_assigns = env#end_transaction in - const_assigns @ [branch] in - let make_assert expr = - let _ = env#start_transaction in - let commands = convert_to_assert expr in - let const_assigns = env#end_transaction in - const_assigns @ commands in - let make_test_code expr = - if is_conjunction expr then - let conjuncts = get_conjuncts expr in - make_asserts conjuncts - else if is_disjunction expr then - let disjuncts = get_disjuncts expr in - make_branch_assert disjuncts - else - make_assert expr in - match optboolxpr with - Some bxpr -> - let thencode = make_test_code bxpr in - let elsecode = make_test_code (simplify_xpr (XOp (XLNot, [bxpr]))) in - (frozenVars, Some (thencode, elsecode)) - | _ -> (frozenVars, None) - - -(* Returns the CHIF code for a conditional branch instruction that - incorporates the full condition as part of the instruction (i.e. no - dependency on a separate test instruction), such as CBZ or CBNZ. - - The CHIF code consists of a tuple of two sequences of CHIF commands. - The first sequence is the CHIF for the then test, the second sequence - is the CHIF for the else test. - - If the condition cannot be converted to CHIF SKIP commands are - returned, that is, the conditional branch is effectively turned into - a nondeterminstic branch. - *) -let make_local_tests - (condinstr: arm_assembly_instruction_int) - (condloc: location_int): (cmd_t list * cmd_t list) = - let floc = get_floc condloc in - let env = floc#f#env in - let reqN () = env#mk_num_temp in - let reqC i = env#request_num_constant i in - let boolxpr_r = - match condinstr#get_opcode with - | CompareBranchZero (op, _) -> - TR.tmap - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun x -> XOp (XEq, [x; zero_constant_expr])) - (op#to_expr floc) - | CompareBranchNonzero (op, _) -> - TR.tmap - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun x -> XOp (XNe, [x; zero_constant_expr])) - (op#to_expr floc) - | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Unexpected condition: " ^ (p2s condinstr#toPretty)] in - - let convert_to_chif expr = - let vars = variables_in_expr expr in - let defcmds = floc#get_vardef_commands ~usehigh:vars floc#l#ci in - let (cmds, bxpr) = xpr_to_boolexpr reqN reqC expr in - cmds @ defcmds @ [ASSERT bxpr] in - let make_assert x = - let _ = env#start_transaction in - let commands = convert_to_chif x in - let const_assigns = env#end_transaction in - const_assigns @ commands in - TR.tfold - ~ok:(fun boolxpr -> - let thencode = make_assert boolxpr in - let elsecode = make_assert (simplify_xpr (XOp (XLNot, [boolxpr]))) in - (thencode, elsecode)) - ~error:(fun e -> - begin - log_error_result __FILE__ __LINE__ e; - ([SKIP], [SKIP]) - end) - boolxpr_r - - -(* Returns the control-flow graph nodes and edges of a conditional branch - instruction that incorporates the full condition as part of the instruction - (i.e., no dependency on a separate test instruction), such as CBZ - (CompareBranchZero) or CBNZ) - - Two cfg nodes are created: a 'then' node with the then-test and an 'else' - node with the else-test. Four cfg edges are created: (1) from block label - to thennode, (2) from block label to elsenode, (3) from thennode to the - cfg target jump address, and (4) from elsenode to the cfg fall-through - address. - *) -let make_local_condition - (condinstr: arm_assembly_instruction_int) - (condloc: location_int) - (blocklabel: symbol_t) - (thenaddr: ctxt_iaddress_t) - (elseaddr: ctxt_iaddress_t) = - let thenlabel = make_code_label thenaddr in - let elselabel = make_code_label elseaddr in - let (thentest, elsetest) = make_local_tests condinstr condloc in - let make_node_and_label testcode tgtaddr modifier = - let src = condloc#i in - let nextlabel = make_code_label ~src ~modifier tgtaddr in - let transaction = TRANSACTION (nextlabel, LF.mkCode testcode, None) in - (nextlabel, [transaction]) in - let (thentestlabel, thennode) = - make_node_and_label thentest thenaddr "then" in - let (elsetestlabel, elsenode) = - make_node_and_label elsetest elseaddr "else" in - let thenedges = - [(blocklabel, thentestlabel); (thentestlabel, thenlabel)] in - let elseedges = - [(blocklabel, elsetestlabel); (elsetestlabel, elselabel) ] in - ([(thentestlabel, thennode); (elsetestlabel, elsenode)], thenedges @ elseedges) - - -(* Returns the control-flow graph nodes and edges of a conditional branch or an - IfThen instruction that is handled with full control flow rather than with an - aggregate. It applies to conditional branches in which the test is performed - by a separate instruction (the test instruction) and the branch condition - is determined by the combination of the test instruction and the condition - code that is part of the branch instruction (or IfThen). - - If a conditional predicate for the branch can be synthesized and converted into - CHIF, a 'then node' with the then-test and an 'else node' with the else-test - are created. In both nodes the temporary variables that were created to carry - the frozen values are abstracted to avoid unnecessary propagation of variables - that will never be used again. Four edges are created: (1) from block-label - to thenblock, (2) from thenblock to the cfg target jump address, (3) from - block-label to elseblock, and (4) from elseblock to the cfg fall-through - instruction. - - If a conditional predicate for the branch cannot be constructed the control flow - components created represent a non-deterministic branch. One node is - constructed, to abstract the temporary variables created by the attempt to - create a condition. Three edges are created: (1) from block-label to the new - node, (2) from the new node to the cfg target jump address, and (3) from the new - node to the cfg fall-through instruction. -*) -let make_condition - ?(thencode: cmd_t list = []) - ?(elsecode: cmd_t list = []) - ~(condinstr:arm_assembly_instruction_int) - ~(testinstr:arm_assembly_instruction_int) - ~(condloc:location_int) - ~(testloc:location_int) - ~(blocklabel:symbol_t) - ~(thenaddr:ctxt_iaddress_t) - ~(elseaddr:ctxt_iaddress_t) - () = - let thenlabel = make_code_label thenaddr in - let elselabel = make_code_label elseaddr in - let (frozenVars, tests) = - make_tests ~condloc ~testloc ~condinstr ~testinstr in - match tests with - Some (thentest, elsetest) -> - let make_node_and_label testcode tgtaddr modifier = - let src = condloc#i in - let nextlabel = make_code_label ~src ~modifier tgtaddr in - let testcode = - testcode - @ (match frozenVars with - | [] -> [] - | _ -> [ABSTRACT_VARS frozenVars]) in - let transaction = TRANSACTION (nextlabel, LF.mkCode testcode, None) in - (nextlabel, [transaction]) in - let (thentestlabel, thennode) = - make_node_and_label (thencode @ thentest) thenaddr "then" in - let (elsetestlabel, elsenode) = - make_node_and_label (elsecode @ elsetest) elseaddr "else" in - let thenedges = - [(blocklabel, thentestlabel); (thentestlabel, thenlabel)] in - let elseedges = - [(blocklabel, elsetestlabel); (elsetestlabel, elselabel) ] in - ([(thentestlabel, thennode); (elsetestlabel, elsenode)], - thenedges @ elseedges) - | _ -> - let abstractlabel = - make_code_label ~modifier:"abstract" testloc#ci in - let trcode = - match frozenVars with - | [] -> [SKIP] - | _ -> [ABSTRACT_VARS frozenVars] in - let transaction = - TRANSACTION (abstractlabel, LF.mkCode trcode, None) in - let edges = [ - (blocklabel, abstractlabel); - (abstractlabel, thenlabel); - (abstractlabel, elselabel)] in - ([(abstractlabel, [transaction])], edges) - - let translate_arm_instruction ~(funloc:location_int) ~(codepc:arm_code_pc_int) @@ -676,9 +96,6 @@ let translate_arm_instruction let invop = OPERATION {op_name = invlabel; op_args = []} in let bwdinvlabel = get_invariant_label ~bwd:true loc in let bwdinvop = OPERATION {op_name = bwdinvlabel; op_args = []} in - let frozenAsserts = - List.map (fun (v,fv) -> ASSERT (EQ (v, fv))) - (finfo#get_test_variables ctxtiaddr) in let rewrite_expr (floc: floc_int) (x:xpr_t): xpr_t = let xpr = floc#inv#rewrite_expr x in let rec expand x = @@ -720,95 +137,17 @@ let translate_arm_instruction (loc#i#add_int 8)#to_numerical in let pcassign = floc#get_assign_commands pcv (XConst (IntConst iaddr8)) in - let build_opener_unit newcmds = - frozenAsserts @ newcmds @ [bwdinvop] @ pcassign in - - let build_unit newcmds = - frozenAsserts @ (invop :: newcmds) @ [bwdinvop] @ pcassign in + let build_unit newcmds = newcmds @ [bwdinvop] @ pcassign in let default newcmds = - ([], [], cmdstate_append_linear cmdstate (build_unit newcmds)) in + let asserts = get_frozen_asserts finfo loc#ci in + let invop = get_invariant_operation loc in + let newcmds = asserts @ (invop :: (build_unit newcmds)) in + ([], [], cmdstate_append_linear finfo cmdstate newcmds) in let make_conditional_commands (c: arm_opcode_cc_t) (cmds: cmd_t list) = - if instr#is_condition_covered then - default cmds - else - match get_associated_test_instr finfo ctxtiaddr with - | Some (testloc, testinstr) -> - if has_false_condition_context ctxtiaddr then - let (_, tests) = - make_instr_local_tests - ~condloc:loc ~testloc ~condinstr:instr ~testinstr in - (match tests with - | Some (_, elsetest) -> default elsetest - | _ -> default []) - else if has_true_condition_context ctxtiaddr then - let (_, tests) = - make_instr_local_tests - ~condloc:loc ~testloc ~condinstr:instr ~testinstr in - (match tests with - | Some (thentest, _) -> default (thentest @ cmds) - | _ -> default cmds) - else - let key = get_setter_key finfo testloc testinstr in - (* make_instr_local_tests must be called for every predicated - instruction, not just the one that opens a fragment: besides - returning the then/else test commands, arm_conditional_expr / - arm_conditional_conditional_expr has the side effect of - registering condfloc#set_test_expr for this instruction's own - location, which bCHFnARMDictionary.ml's xdata generation and - bCHFnARMTypeConstraints.ml's type-constraint generation both - depend on per-instruction. *) - let (_, tests) = - make_instr_local_tests - ~condloc:loc ~testloc ~condinstr:instr ~testinstr in - let already_open = - match cmdstate.cs_open with - | Some fr -> - fr.fr_key = key - && (c = fr.fr_opencc || get_inverse_cc fr.fr_opencc = Some c) - | None -> false in - let fmem = - match cmdstate.cs_open with - | Some fr when already_open -> - {fmem_openerloc = fr.fr_openerloc; - fmem_bucket = if c = fr.fr_opencc then FragThen else FragElse} - | _ -> - {fmem_openerloc = loc; fmem_bucket = FragThen} in - let _ = finfo#set_fragment_membership ctxtiaddr fmem in - if already_open then - let unit_cmds = build_unit cmds in - ([], [], - cmdstate_append_predicated - cmdstate - ~key - ~cc:c - ~openerloc:fmem.fmem_openerloc - ~thentest:[] - ~elsetest:[] - ~unit_cmds) - else - let unit_cmds = build_opener_unit cmds in - let (thentest, elsetest) = - match tests with - | Some (t, e) -> (t, e) - | None -> ([], []) in - ([], [], - cmdstate_append_predicated - cmdstate - ~key - ~cc:c - ~openerloc:fmem.fmem_openerloc - ~thentest - ~elsetest - ~unit_cmds) - | _ -> - if has_false_condition_context ctxtiaddr then - default [] - else if has_true_condition_context ctxtiaddr then - default cmds - else - default [BRANCH [LF.mkCode cmds; LF.mkCode[SKIP]]] in + ([], [], + append_predicated_instruction finfo cmdstate ~instr ~loc ~cc:c ~build_unit ~cmds) in let get_register_vars (ops: arm_operand_int list) = List.fold_left (fun acc op -> @@ -1299,13 +638,19 @@ let translate_arm_instruction jump *) if is_direct_branch then match get_setter_key_at finfo ctxtiaddr with - | Some (key, _, _) -> cmdstate_take_for_terminator cmdstate ~key ~cc:c - | _ -> (cmdstate_finish cmdstate, [], []) + | Some (key, _, _) -> + cmdstate_take_for_terminator finfo cmdstate ~key ~cc:c + | _ -> + (cmdstate_finish finfo cmdstate, [], []) else - (cmdstate_finish cmdstate, [], []) in + (cmdstate_finish finfo cmdstate, [], []) in let cmds = prefix_flat @ [invop] @ defcmds @ [bwdinvop] in - (* let cmds = cmds @ [invop] @ defcmds @ [bwdinvop] in *) - let transaction = package_transaction finfo blocklabel cmds in + let (transaction, thenbucket, elsebucket) = + match (thencode, elsecode) with + | ([], []) -> + (package_transaction finfo blocklabel cmds, None, None) + | _ -> + package_terminator_transactions finfo blocklabel cmds thencode elsecode in if finfo#has_associated_cc_setter ctxtiaddr then let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in let testloc = ctxt_string_to_location faddr testiaddr in @@ -1317,8 +662,8 @@ let translate_arm_instruction (get_arm_assembly_instruction testaddr) in let (nodes, edges) = make_condition - ~thencode - ~elsecode + ?thencode:thenbucket + ?elsecode:elsebucket ~condinstr:instr ~testinstr:testinstr ~condloc:loc @@ -1349,7 +694,7 @@ let translate_arm_instruction end) (op#to_expr floc) in let defcmds = floc#get_vardef_commands ~use:usevars ~usehigh ctxtiaddr in - let cmds = (cmdstate_finish cmdstate) @ defcmds @ [invop] in + let cmds = (cmdstate_finish finfo cmdstate) @ defcmds @ [invop] in let transaction = package_transaction finfo blocklabel cmds in let (nodes, edges) = make_local_condition instr loc blocklabel thenaddr elseaddr in @@ -2019,7 +1364,7 @@ let translate_arm_instruction | IfThen _ when instr#is_block_condition -> let thenaddr = codepc#get_true_branch_successor in let elseaddr = codepc#get_false_branch_successor in - let cmds = (cmdstate_finish cmdstate) @ [invop] in + let cmds = (cmdstate_finish finfo cmdstate) @ [invop] in let transaction = package_transaction finfo blocklabel cmds in (match get_associated_test_instr finfo ctxtiaddr with | Some (testloc, testinstr) -> @@ -3122,15 +2467,16 @@ let translate_arm_instruction (* collect all previous commands in the block and the invariant anchor and package them together with the vardef commands in a transaction *) - let cmds = (cmdstate_finish cmdstate) @ (invop :: ccvardefs) in - let transaction = package_transaction finfo blocklabel cmds in + let cmds = (cmdstate_finish finfo cmdstate) @ (invop :: ccvardefs) in + let (transaction, thencode, _) = + package_terminator_transactions finfo blocklabel cmds (popcmds ()) [] in (* create the branches according to the condition *) (match get_associated_test_instr finfo ctxtiaddr with | Some (testloc, testinstr) -> let (nodes, edges) = make_condition - ~thencode:(popcmds ()) + ?thencode ~condinstr:instr ~testinstr:testinstr ~condloc:loc @@ -5190,7 +4536,7 @@ object (self) aux newcmdstate else let transaction = - package_transaction finfo blocklabel (cmdstate_finish newcmdstate) in + package_transaction finfo blocklabel (cmdstate_finish finfo newcmdstate) in let nodes = [(blocklabel, [transaction])] in let edges = List.map @@ -5452,7 +4798,7 @@ object (self) let cfg = codegraph#to_cfg entryLabel exitLabel in let body = LF.mkCode [CFG (procname, cfg)] in let proc = LF.mkProcedure procname ~signature:[] ~bindings:[] ~scope ~body in - (* let _ = pr_debug [proc#toPretty; NL] in *) + let _ = pr_debug [proc#toPretty; NL] in arm_chif_system#add_arm_procedure proc end diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli index 1f32a0bf8..1bb26d6a4 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.mli @@ -33,35 +33,17 @@ open CHOnlineCodeSet open BCHLibTypes (* bchlibarm32 *) +open BCHARMPredicatedFragment open BCHARMTypes -type setter_key_t = { - sk_testloc: ctxt_iaddress_t; - sk_testtestloc: ctxt_iaddress_t option - } - -type fragment_t = { - fr_key: setter_key_t; - fr_opencc: arm_opcode_cc_t; (* the cc that defines "then" *) - fr_openerloc: location_int; (* location of first instr in fragment *) - fr_thenbucket: cmd_t list; (* starts with thentest, grows by append *) - fr_elsebucket: cmd_t list (* starts with elsetest *) - } - -type cmdstate_t = { - cs_flat: cmd_t list; (* closed-out cmds, in order *) - cs_open: fragment_t option (* at most one open fragement *) - } - - val translate_arm_instruction: funloc:location_int -> codepc:arm_code_pc_int -> blocklabel:symbol_t -> cmdstate:cmdstate_t -> ((symbol_t - * (code_t, 'a) command_t list) list + * (code_t, cfg_int) command_t list) list * (symbol_t * symbol_t) list * cmdstate_t) From d3c179066ab57aa23e645335b69c9fa71958718d Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 8 Sep 2026 13:10:30 -0700 Subject: [PATCH 15/22] CHB:ARM: update xdata export for predicated fragments --- .../CHB/bchlibarm32/bCHARMConditionalExpr.ml | 10 +++- .../CHB/bchlibarm32/bCHFnARMDictionary.ml | 46 ++++++++++++++++++- 2 files changed, 53 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml index e348cb6cf..6f751600a 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml @@ -112,6 +112,8 @@ module TR = CHTraceResult let x2p = xpr_formatter#pr_expr let max32_constant_expr = int_constant_expr e32 +let p2s = CHPrettyUtil.pretty_to_string +let x2s x = p2s (x2p x) let tracked_locations = [] @@ -541,8 +543,12 @@ let arm_conditional_conditional_expr let xpr = XOp (XLOr, [XOp (XLAnd, [XOp (XLNot, [cond1]); cond3]); XOp (XLAnd, [cond1; cond2])]) in begin - (if collect_diagnostics () then - ch_diagnostics_log#add "condition" (x2p xpr)); + let _ = + log_diagnostics_result + ~tag:"arm_conditional_conditional_expr:set_test_expr" + ~msg:condfloc#l#ci + __FILE__ __LINE__ + ["xpr set: " ^ (x2s xpr)] in condfloc#set_test_expr xpr; (frozenVars#toList, Some xpr, opsused) end diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 86403e11c..9cbb7ad5e 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -687,11 +687,19 @@ object (self) let fmxpr = floc#f#get_test_expr openerloc#ci in let txpr = match fm.fmem_bucket with - | FragThen -> fmxpr + | FragThen -> simplify_xpr fmxpr | FragElse -> simplify_xpr (XOp (XLNot, [fmxpr])) in let fxpr = simplify_xpr (XOp (XLNot, [txpr])) in let tcond = rewrite_floc_expr openerfloc txpr in let fcond = rewrite_floc_expr openerfloc fxpr in + let _ = + log_diagnostics_result + ~tag:"add_optional_instr_condtiion" + ~msg:floc#cia + __FILE__ __LINE__ + ["fmxpr: " ^ (x2s fmxpr); + "txpr: " ^ (x2s txpr); + "tcond: " ^ (x2s tcond)] in let ctcond_r = floc#xpr_to_cxpr ~size:(Some 4) tcond in let cfcond_r = floc#xpr_to_cxpr ~size:(Some 4) fcond in let rdefs = (get_all_rdefs txpr) @ (get_all_rdefs tcond) in @@ -1767,6 +1775,42 @@ object (self) (LBLOCK [ STR "Aggregate branch not recognized at "; iaddr#toPretty])) + | Branch (c, tgt, _) + when is_cond_conditional c + && tgt#is_absolute_address + && floc#f#has_fragment_membership floc#cia -> + let xtgt_r = tgt#to_expr floc in + let fm = floc#f#get_fragment_membership floc#cia in + let openerloc = fm.fmem_openerloc in + let openerfloc = get_floc openerloc in + let fmxpr = floc#f#get_test_expr openerloc#ci in + let txpr = + match fm.fmem_bucket with + | FragThen -> simplify_xpr fmxpr + | FragElse -> simplify_xpr (XOp (XLNot, [fmxpr])) in + let fxpr = simplify_xpr (XOp (XLNot, [txpr])) in + let tcond = rewrite_floc_expr openerfloc txpr in + let fcond = rewrite_floc_expr openerfloc fxpr in + let ctcond_r = floc#xpr_to_cxpr ~size:(Some 4) tcond in + let cfcond_r = floc#xpr_to_cxpr ~size:(Some 4) fcond in + let csetter = floc#f#get_associated_cc_setter floc#cia in + let csetter_addr_r = string_to_doubleword csetter in + let csetter_instr_r = + TR.tbind get_arm_assembly_instruction csetter_addr_r in + let bytestr = + TR.tfold + ~ok:(fun instr -> instr#get_bytes_ashexstring) + ~error:(fun e -> + begin log_error_result __FILE__ __LINE__ e; "0x0" end) + csetter_instr_r in + let rdefs = (get_all_rdefs txpr) @ (get_all_rdefs tcond) in + let xprs_r = [Ok txpr; Ok fxpr; Ok tcond; Ok fcond; xtgt_r] in + let cxprs_r = [ctcond_r; cfcond_r] in + let (tagstring, args) = mk_instrx_data_r ~xprs_r ~cxprs_r ~rdefs () in + let (tags, args) = (tagstring :: ["TF"; csetter; bytestr], args) in + let tags = add_optional_subsumption tags in + (tags, args) + | Branch (c, tgt, _) when is_cond_conditional c && tgt#is_absolute_address From 156799b95f0129ed16766287b98b062bde6a8864 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 9 Sep 2026 13:06:06 -0700 Subject: [PATCH 16/22] CHB: add error handling for location context --- CodeHawk/CHB/bchlib/bCHFloc.ml | 31 +++-- CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 42 ++++--- CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml | 82 ++++++++----- CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml | 28 +++-- CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml | 2 +- CodeHawk/CHB/bchlib/bCHLocation.ml | 70 ++++++----- CodeHawk/CHB/bchlib/bCHLocation.mli | 7 +- CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml | 109 ++++++++++++------ CodeHawk/CHB/bchlib/bCHMetrics.ml | 21 +++- CodeHawk/CHB/bchlib/bCHProofObligations.ml | 37 +++--- 10 files changed, 273 insertions(+), 156 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 5a633543e..271c344ac 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -2429,20 +2429,27 @@ object (self) TR.tbind ~msg:(eloc __LINE__) (fun callsite -> - let loc = ctxt_string_to_location self#fa callsite in - let fndata = functions_data#get_function self#fa in - if fndata#has_regvar_type_annotation loc#i then - fndata#get_regvar_type_annotation loc#i - else - let ctinfo = self#f#get_call_target callsite in - let rty = ctinfo#get_returntype in - if is_unknown_type rty then + TR.tfold + ~ok:(fun loc -> + let fndata = functions_data#get_function self#fa in + if fndata#has_regvar_type_annotation loc#i then + fndata#get_regvar_type_annotation loc#i + else + let ctinfo = self#f#get_call_target callsite in + let rty = ctinfo#get_returntype in + if is_unknown_type rty then + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "return type of function " ^ ctinfo#get_name + ^ " not known"] + else + Ok rty) + ~error:(fun e -> Error [(elocm __LINE__); (p2s self#l#toPretty); - "return type of function " ^ ctinfo#get_name - ^ " not known"] - else - Ok rty) + String.concat "; " e; + "location of return type of function invalid"]) + (ctxt_string_to_location self#fa callsite)) (self#f#env#get_call_site v) else if self#f#env#is_register_variable v then diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 0efa338fb..0984ebad8 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -2525,21 +2525,33 @@ object (self) List.iter (fun eNode -> let get = eNode#getAttribute in let iaddr = get "iaddr" in - let opener = - BCHLocation.ctxt_string_to_location (self#get_address) (get "opener") in - let polarity = - match (get "pol") with - | "then" -> FragThen - | "else" -> FragElse - | s -> - raise - (BCH_failure - (LBLOCK [STR "read_xml_fragment_memberships: "; - self#get_address#toPretty; - STR ": "; - STR s])) in - H.add fragment_membership iaddr - {fmem_openerloc = opener; fmem_bucket = polarity}) + let faddr = self#get_address in + TR.tfold + ~ok:(fun opener -> + let polarity = + match (get "pol") with + | "then" -> FragThen + | "else" -> FragElse + | s -> + raise + (BCH_failure + (LBLOCK [STR "read_xml_fragment_memberships: "; + self#get_address#toPretty; + STR ": "; + STR s])) in + H.add fragment_membership iaddr + {fmem_openerloc = opener; fmem_bucket = polarity}) + ~error:(fun e -> + begin + log_error_result + ~tag:"read_xml_fragment_memberships" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end) + (BCHLocation.ctxt_string_to_location faddr (get "opener"))) (getcc "fmem") method private write_xml_test_expressions (node:xml_element_int) = diff --git a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml index 7fb6b6a1b..3e388a1f7 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionPODischarge.ml @@ -139,7 +139,17 @@ let buffer_writer_callsite if defcia = "init" then None else if finfo#has_call_target defcia then - Some (BCHLocation.ctxt_string_to_location finfo#a defcia) + TR.tfold + ~ok:(fun loc -> Some loc) + ~error:(fun e -> + begin + log_error_result + ~tag:"buffer_writer_callsite" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ e; + None + end) + (BCHLocation.ctxt_string_to_location finfo#a defcia) else None) vinv#get_reaching_defs) @@ -199,7 +209,17 @@ let external_buffer_writer_callsite if defcia = "init" then None else if finfo#has_call_target defcia then - Some (BCHLocation.ctxt_string_to_location finfo#a defcia) + TR.tfold + ~ok:(fun loc -> Some loc) + ~error:(fun e -> + begin + log_error_result + ~tag:"external_buffer_writer_callsite" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ e; + None + end) + (BCHLocation.ctxt_string_to_location finfo#a defcia) else None) vinv#get_reaching_defs) @@ -1555,33 +1575,37 @@ let impose_trusted_os_cmd_string_pc let* memvar = finfo#env#mk_basevar_memory_variable paramvar NoOffset in let errors = List.fold_left (fun errors rcia -> - let loc = BCHLocation.ctxt_string_to_location finfo#get_address rcia in - match external_buffer_writer_callsite finfo loc memvar with - | Some defloc -> - let deffloc = BCHFloc.get_finfo_floc finfo defloc in - if call_writes_to_buffer deffloc (XVar paramvar) then - let xpo = XPOTrustedOsCmdString (XVar paramvar) in - begin - finfo#proofobligations#add_proofobligation defloc#ci xpo Open; - (log_diagnostics_result - ~tag:"impose_trusted_os_cmd_string_pc" - ~msg:(p2s defloc#toPretty) - __FILE__ __LINE__ - ["returnloc: " ^ rcia; - "xpo: " ^ (p2s (xpo_predicate_to_pretty xpo))]); - errors - end - else - [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc"; - "no buffer write"; - "returnloc: " ^ rcia; - "deffloc: " ^ (p2s deffloc#l#toPretty); - "memvar: " ^ (p2s memvar#toPretty)] @ errors - | _ -> - [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc"; - "no defloc"; - "returnloc: " ^ rcia; - "memvar: " ^ (p2s memvar#toPretty)] @ errors) + TR.tfold + ~ok:(fun loc -> + match external_buffer_writer_callsite finfo loc memvar with + | Some defloc -> + let deffloc = BCHFloc.get_finfo_floc finfo defloc in + if call_writes_to_buffer deffloc (XVar paramvar) then + let xpo = XPOTrustedOsCmdString (XVar paramvar) in + begin + finfo#proofobligations#add_proofobligation defloc#ci xpo Open; + (log_diagnostics_result + ~tag:"impose_trusted_os_cmd_string_pc" + ~msg:(p2s defloc#toPretty) + __FILE__ __LINE__ + ["returnloc: " ^ rcia; + "xpo: " ^ (p2s (xpo_predicate_to_pretty xpo))]); + errors + end + else + [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc"; + "no buffer write"; + "returnloc: " ^ rcia; + "deffloc: " ^ (p2s deffloc#l#toPretty); + "memvar: " ^ (p2s memvar#toPretty)] @ errors + | _ -> + [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc"; + "no defloc"; + "returnloc: " ^ rcia; + "memvar: " ^ (p2s memvar#toPretty)] @ errors) + ~error:(fun e -> + [(elocm __LINE__) ^ "impose_trusted_os_cmd_string_pc"] @ e @ errors) + (BCHLocation.ctxt_string_to_location finfo#get_address rcia)) [] returnlocs in match errors with | [] -> Ok () diff --git a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml index 76ffcf511..89c8f35b4 100644 --- a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml +++ b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024-2025 Aarno Labs LLC + Copyright (c) 2024-2026 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 @@ -793,14 +793,24 @@ object (self) (btype: btype_t) = match self#xpr_containing_location gxpr with | Some gloc -> - let loc = BCHLocation.ctxt_string_to_location faddr iaddr in - let memoff = TR.to_option (gloc#address_memory_offset loc gxpr) in - let garg = - GAddressArgument (gloc#address, iaddr, argindex, gxpr, btype, memoff) in - begin - self#add_global_ref faddr garg; - Some gloc - end + TR.tfold + ~ok:(fun loc -> + let memoff = TR.to_option (gloc#address_memory_offset loc gxpr) in + let garg = + GAddressArgument (gloc#address, iaddr, argindex, gxpr, btype, memoff) in + begin + self#add_global_ref faddr garg; + Some gloc + end) + ~error:(fun e -> + begin + log_error_result + ~tag:"add_gaddr_argument" + ~msg:iaddr + __FILE__ __LINE__ e; + None + end) + (BCHLocation.ctxt_string_to_location faddr iaddr) | _ -> (match gxpr with | XConst (IntConst n) -> diff --git a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml index 669ec11b7..bcfe0571a 100644 --- a/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHInterfaceDictionary.ml @@ -403,7 +403,7 @@ object (self) let getdw (s: string) = TR.tget_ok (string_to_doubleword s) in let makeloc (faddr: string) (ci: string) = let dw = TR.tget_ok (string_to_doubleword faddr) in - ctxt_string_to_location dw ci in + TR.tget_ok (ctxt_string_to_location dw ci) in let t = t name tags in let a = a name args in match (t 0) with diff --git a/CodeHawk/CHB/bchlib/bCHLocation.ml b/CodeHawk/CHB/bchlib/bCHLocation.ml index 5149378d8..764f0d3a3 100644 --- a/CodeHawk/CHB/bchlib/bCHLocation.ml +++ b/CodeHawk/CHB/bchlib/bCHLocation.ml @@ -40,6 +40,10 @@ module H = Hashtbl module TR = CHTraceResult +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + + let nsplit (separator:char) (s:string):string list = let result = ref [] in let len = String.length s in @@ -108,7 +112,7 @@ let mk_base_location (faddr:doubleword_int) (iaddr:doubleword_int) = let mk_function_context ~(faddr: doubleword_int) ~(callsite: doubleword_int) - ~(returnsite: doubleword_int) = + ~(returnsite: doubleword_int): context_t = FunctionContext {ctxt_faddr = faddr; ctxt_callsite = callsite; @@ -119,10 +123,10 @@ let contexts = H.create 3 let add_function_ctxt_iaddress - (faddr:doubleword_int) (* outer function address *) - (s:ctxt_iaddress_t) - (basef:doubleword_int) (* inner function address *) - (c:context_t list) = + (faddr: doubleword_int) (* outer function address *) + (s: ctxt_iaddress_t) + (basef: doubleword_int) (* inner function address *) + (c: context_t list) = let faddr = faddr#to_hex_string in let basef = basef#to_hex_string in let f_entry = @@ -135,48 +139,46 @@ let add_function_ctxt_iaddress if H.mem f_entry s then () else - H.add f_entry s (basef,c) + H.add f_entry s (basef, c) -let get_context (faddr: doubleword_int) (s: string) = +let get_context + (faddr: doubleword_int) (s: string) + : (doubleword_int * context_t list) TR.traceresult = if s = "" then - (faddr, []) + Ok (faddr, []) else let faddr = faddr#to_hex_string in if H.mem contexts faddr then let f_entry = H.find contexts faddr in if H.mem f_entry s then let (f, c) = H.find f_entry s in - (TR.tget_ok (string_to_doubleword f), c) + TR.tmap (fun dw -> (dw, c)) (string_to_doubleword f) else - raise - (BCH_failure - (LBLOCK [ - STR "Contexts for "; - STR faddr; - STR " do not include: "; - STR s])) + Error [(elocm __LINE__) + ^ "Contexts for " ^ faddr ^ " do not include " ^ s] else - raise - (BCH_failure - (LBLOCK [STR "No contexts found for "; STR faddr])) + Error [(elocm __LINE__) + ^ "No contexts fround for " ^ s ^ " in function " ^ faddr] let decompose_ctxt_string (faddr:doubleword_int) (* outer function address *) - (s:ctxt_iaddress_t) = + (s:ctxt_iaddress_t) + : (context_t list * doubleword_int * doubleword_int) TR.traceresult = let s2dw = (fun s -> TR.tget_ok (string_to_doubleword s)) in let components = nsplit '_' s in let iaddr = s2dw (List.hd (List.rev components)) in let ctxtcomponents = List.rev (List.tl (List.rev components)) in match ctxtcomponents with - | [] -> ([], faddr, iaddr) - | ["T@"] -> ([ConditionContext true], faddr, iaddr) - | ["F@"] -> ([ConditionContext false], faddr, iaddr) + | [] -> Ok ([], faddr, iaddr) + | ["T@"] -> Ok ([ConditionContext true], faddr, iaddr) + | ["F@"] -> Ok ([ConditionContext false], faddr, iaddr) | _ -> let ctxtstr = String.concat "_" ctxtcomponents in - let (basef, ctxt) = get_context faddr ctxtstr in - (ctxt, basef, iaddr) + TR.tmap + (fun (basef, ctxt) -> (ctxt, basef, iaddr)) + (get_context faddr ctxtstr) let has_false_condition_context (ctxt_iaddr: ctxt_iaddress_t): bool = @@ -299,17 +301,23 @@ let make_function_context_location make_c_location loc ctxt -let ctxt_string_to_location (faddr:doubleword_int) (s:ctxt_iaddress_t) = - let (ctxt, basef, iaddr) = decompose_ctxt_string faddr s in - make_location ~ctxt {loc_faddr = basef; loc_iaddr = iaddr} +let ctxt_string_to_location + (faddr:doubleword_int) (s:ctxt_iaddress_t): location_int TR.traceresult = + TR.tmap + ~msg:((elocm __LINE__) ^ "ctxt_string_to_location") + (fun (ctxt, basef, iaddr) -> + make_location ~ctxt {loc_faddr = basef; loc_iaddr = iaddr}) + (decompose_ctxt_string faddr s) let add_ctxt_to_ctxt_string (faddr:doubleword_int) (* outer function of existing context *) (ctxtstr:ctxt_iaddress_t) - (newctxt:context_t) = - let loc = ctxt_string_to_location faddr ctxtstr in - (make_c_location loc newctxt)#ci + (newctxt:context_t): string TR.traceresult = + TR.tmap + ~msg:"add_ctxt_string_to_string" + (fun loc -> (make_c_location loc newctxt)#ci) + (ctxt_string_to_location faddr ctxtstr) let symbol_to_ctxt_string (s:symbol_t) = diff --git a/CodeHawk/CHB/bchlib/bCHLocation.mli b/CodeHawk/CHB/bchlib/bCHLocation.mli index 9686df65f..912ac0386 100644 --- a/CodeHawk/CHB/bchlib/bCHLocation.mli +++ b/CodeHawk/CHB/bchlib/bCHLocation.mli @@ -30,6 +30,9 @@ (* chlib *) open CHLanguage +(* chutil *) +open CHTraceResult + (* bchlib *) open BCHLibTypes @@ -154,14 +157,14 @@ val make_function_context_location: val ctxt_string_to_location: doubleword_int (* outer function address *) -> ctxt_iaddress_t (* string that represents the base location and context *) - -> location_int + -> location_int traceresult val add_ctxt_to_ctxt_string: doubleword_int (* outer function address *) -> ctxt_iaddress_t (* string that represents the context, outer context first *) -> context_t (* new context to be prepended *) - -> ctxt_iaddress_t + -> ctxt_iaddress_t traceresult (** [ctxt_string_to_string ctxt_iaddr] converts [ctxt_iaddr] to a string (which, diff --git a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml index 55ed56963..fa68d8973 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml @@ -91,7 +91,7 @@ object (self) method iaddr = iaddr - method private loc: location_int = + method private loc: location_int traceresult = ctxt_string_to_location self#faddr self#iaddr method private get_gvalue (x: xpr_t) = @@ -100,11 +100,21 @@ object (self) | XVar v when self#env#is_return_value v -> TR.tfold ~ok:(fun callSite -> - GReturnValue (ctxt_string_to_location self#faddr callSite)) + TR.tfold + ~ok:(fun callsiteloc -> GReturnValue callsiteloc) + ~error:(fun e -> + begin + log_dc_error_result + ~tag:"get_gvalue" + __FILE__ __LINE__ + (("x: " ^ (x2s x)) :: e); + GUnknownValue + end) + (ctxt_string_to_location self#faddr callSite)) ~error:(fun e -> begin log_diagnostics_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"memrecorder:get_gvalue" __FILE__ __LINE__ (e @ ["invalid callsite"]); GUnknownValue @@ -112,24 +122,33 @@ object (self) (self#env#get_call_site v) | XVar v when self#env#is_sideeffect_value v -> TR.tfold - ~ok: (fun callSite -> + ~ok:(fun callSite -> TR.tfold - ~ok:(fun argdescr -> - GSideeffectValue - (ctxt_string_to_location self#faddr callSite, argdescr)) + ~ok:(fun callsiteloc -> + TR.tfold + ~ok:(fun argdescr -> GSideeffectValue (callsiteloc, argdescr)) + ~error:(fun e -> + begin + log_diagnostics_result + ~msg:iaddr + ~tag:"memrecorder:get_gvalue" + __FILE__ __LINE__ (e @ ["invalide side-effect descriptor"]); + GUnknownValue + end) + (self#env#get_se_argument_descriptor v)) ~error:(fun e -> begin - log_diagnostics_result - ~msg:(p2s self#loc#toPretty) - ~tag:"memrecorder:get_gvalue" - __FILE__ __LINE__ (e @ ["invalide side-effect descriptor"]); + log_dc_error_result + ~tag:"get_gvalue" + __FILE__ __LINE__ + (("x: " ^ (x2s x)) :: e); GUnknownValue end) - (self#env#get_se_argument_descriptor v)) + (ctxt_string_to_location self#faddr callSite)) ~error:(fun e -> begin log_diagnostics_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"memrecorder:get_gvalue" __FILE__ __LINE__ (e @ ["invalide side-effect value"]); GUnknownValue @@ -172,12 +191,20 @@ object (self) && (self#env#has_global_variable_address lhs) then TR.tfold ~ok:(fun gaddr -> - global_system_state#add_writer - ~ty:vtype ~size (self#get_gvalue rhs) gaddr self#loc) + TR.tfold + ~ok:(fun loc -> + global_system_state#add_writer + ~ty:vtype ~size (self#get_gvalue rhs) gaddr loc) + ~error:(fun e -> + log_error_result + ~tag:"record_assignment_lhs" + ~msg:iaddr + __FILE__ __LINE__ e) + self#loc) ~error:(fun e -> log_error_result ~tag:"record_assignment_lhs" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ (["invalid global address for: " ^ (p2s lhs#toPretty)] @ e)) (self#env#get_global_variable_address lhs) @@ -197,21 +224,21 @@ object (self) | _ -> log_diagnostics_result ~tag:"record_assignment_lhs" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ ["stack assignment lhs not recorded"; "lhs: " ^ (p2s lhs#toPretty)]) ~error:(fun e -> log_error_result ~tag:"record_assignment_lhs" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ (["invalid offset for: " ^ (p2s lhs#toPretty)] @ e)) (self#env#get_memvar_offset lhs) else log_diagnostics_result ~tag:"record_assignment_lhs" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ ["assignment lhs not recorded"; "lhs: " ^ (p2s lhs#toPretty); @@ -225,11 +252,19 @@ object (self) && (self#env#has_global_variable_address v) then TR.tfold ~ok:(fun gaddr -> - global_system_state#add_reader ~ty:vtype ~size gaddr self#loc) + TR.tfold + ~ok:(fun loc -> + global_system_state#add_reader ~ty:vtype ~size gaddr loc) + ~error:(fun e -> + log_error_result + ~tag:"record_assignment_rhs" + ~msg:iaddr + __FILE__ __LINE__ e) + self#loc) ~error:(fun e -> log_error_result ~tag:"record_assignment_rhs" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ (["invalid global address for: " ^ (x2s rhs)] @ e)) (self#env#get_global_variable_address v) @@ -248,7 +283,7 @@ object (self) | _ -> log_diagnostics_result ~tag:"record_assignment_rhs" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ ["stack assignment rhs not recorded"; "v: " ^ (p2s v#toPretty); @@ -256,14 +291,14 @@ object (self) ~error:(fun e -> log_error_result ~tag:"record_assignment_rhs" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ (["invalid offset for: " ^ (x2s rhs)] @ e)) (self#env#get_memvar_offset v) else log_diagnostics_result ~tag:"record_assignment_rhs" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ ["assignment not recorded"; "v: " ^ (p2s v#toPretty); @@ -276,7 +311,7 @@ object (self) ~(size: int) ~(vtype: btype_t) = log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"deprecated: record_load" __FILE__ __LINE__ ["memory_recorder#record_load is deprecated. "; @@ -326,7 +361,7 @@ object (self) | _ -> log_dc_error_result ~tag:"record_stack_variable_load" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ ["offset: " ^ (BCHMemoryReference.memory_offset_to_string stackoffset); "signed: " ^ (if signed then "yes" else "no")]) @@ -345,14 +380,14 @@ object (self) mmap#add_location_gload self#faddr iaddr gaddr offset size signed t_unknown | _ -> log_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record_global_variable_load" __FILE__ __LINE__ ["Unexpected offset for global variable " ^ (p2s var#toPretty) ^ ": " ^ (memory_offset_to_string globaloffset)]) ~error:(fun e -> log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record_global_variable_load" __FILE__ __LINE__ (e @ ["Unable to obtain offset from variable " ^ (p2s var#toPretty)])) @@ -367,7 +402,7 @@ object (self) let _ = log_diagnostics_result ~tag:"record_load_r" - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr __FILE__ __LINE__ ["addr: " ^ (TR.tfold_default x2s "?" addr_r); "var: " ^ (TR.tfold_default (fun v -> p2s v#toPretty) "?" var_r)] in @@ -379,7 +414,7 @@ object (self) self#record_global_variable_load ~signed ~var ~size else if self#env#is_basevar_memory_variable var then log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record_load_r" __FILE__ __LINE__ ["Recording of basevar loads not yet supported. Var: " @@ -389,14 +424,14 @@ object (self) TR.tfold ~ok:(fun addr -> log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record_load_r" __FILE__ __LINE__ ["Unable to record memory load for variable " ^ (p2s var#toPretty) ^ " with address " ^ (x2s addr)]) ~error:(fun e -> log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record_load_r" __FILE__ __LINE__ (["Unable to record memory load for variable " ^ (p2s var#toPretty)] @@ -426,7 +461,7 @@ object (self) self#record_stack_variable_store ~var ~size ~vtype ~xpr_r:(Ok xpr) else if self#env#is_basevar_memory_variable var then log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record memory store" __FILE__ __LINE__ ["Recording of basevar loads not yet supported. Var: " @@ -442,7 +477,7 @@ object (self) | Ok () -> () | Error e -> log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record_store" __FILE__ __LINE__ (["addr: " ^ (x2s addr); "var: " ^ (p2s var#toPretty)] @ e) in @@ -482,7 +517,7 @@ object (self) iaddr | _ -> log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record_store" __FILE__ __LINE__ ["var: " ^ (p2s var#toPretty); @@ -503,7 +538,7 @@ object (self) self#record_stack_variable_store ~var ~size ~vtype ~xpr_r else if self#env#is_basevar_memory_variable var then log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record memory store" __FILE__ __LINE__ ["Recording of basevar loads not yet supported. Var: " @@ -520,7 +555,7 @@ object (self) | Ok () -> () | Error e -> log_dc_error_result - ~msg:(p2s self#loc#toPretty) + ~msg:iaddr ~tag:"record store" __FILE__ __LINE__ e) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) diff --git a/CodeHawk/CHB/bchlib/bCHMetrics.ml b/CodeHawk/CHB/bchlib/bCHMetrics.ml index 1f8a4cf26..d06a40647 100644 --- a/CodeHawk/CHB/bchlib/bCHMetrics.ml +++ b/CodeHawk/CHB/bchlib/bCHMetrics.ml @@ -31,6 +31,7 @@ open CHPretty (* chutil *) +open CHLogger open CHXmlDocument (* bchlib *) @@ -97,10 +98,22 @@ let get_jumps_metrics (finfo:function_info_int) = let norange = List.fold_left (fun acc ctxtiaddr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - match floc#get_jump_successors with - | [] -> acc + 1 | _ -> acc) 0 jts in + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + match floc#get_jump_successors with + | [] -> acc + 1 + | _ -> acc) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_jumps_metrics" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + acc + end) + (ctxt_string_to_location faddr ctxtiaddr)) + 0 jts in { mjumps_indirect = finfo#get_indirect_jumps_count ; mjumps_jumptable = finfo#get_jumptable_count ; mjumps_jumptable_norange = norange ; diff --git a/CodeHawk/CHB/bchlib/bCHProofObligations.ml b/CodeHawk/CHB/bchlib/bCHProofObligations.ml index e253959a0..151e161a1 100644 --- a/CodeHawk/CHB/bchlib/bCHProofObligations.ml +++ b/CodeHawk/CHB/bchlib/bCHProofObligations.ml @@ -41,7 +41,7 @@ open BCHLocation open BCHXPOPredicate module H = Hashtbl - +module TR = CHTraceResult let p2s = CHPrettyUtil.pretty_to_string @@ -147,21 +147,26 @@ object (self) (cia: ctxt_iaddress_t) (xpo: xpo_predicate_t) (status: po_status_t) = - let loc = ctxt_string_to_location self#faddr cia in - let po = new proofobligation_t xpo loc status in - let _ = - log_diagnostics_result - ~tag:"add_proofobligation" - ~msg:(p2s loc#toPretty) - __FILE__ __LINE__ - ["xpo: " ^ (p2s (xpo_predicate_to_pretty xpo)); - "status: " ^ (p2s (po_status_to_pretty status))] in - let entry = - if H.mem store cia then - H.find store cia - else - [] in - H.replace store cia (po :: entry) + TR.tfold + ~ok:(fun loc -> + let po = new proofobligation_t xpo loc status in + let _ = + log_diagnostics_result + ~tag:"add_proofobligation" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpo: " ^ (p2s (xpo_predicate_to_pretty xpo)); + "status: " ^ (p2s (po_status_to_pretty status))] in + let entry = + if H.mem store cia then + H.find store cia + else + [] in + H.replace store cia (po :: entry)) + ~error:(fun e -> + log_error_result + ~tag:"add_proofobligation" ~msg:cia __FILE__ __LINE__ e) + (ctxt_string_to_location self#faddr cia) method loc_proofobligations (cia: ctxt_iaddress_t): proofobligation_int list = From 0959a54611f304bc37ee8ac33a986e2f22391dcd Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 9 Sep 2026 13:07:34 -0700 Subject: [PATCH 17/22] CHB:ARM: add error handling for location context --- .../CHB/bchlibarm32/bCHARMAnalysisResults.ml | 17 +- .../CHB/bchlibarm32/bCHARMAssemblyFunction.ml | 68 +++++--- .../bchlibarm32/bCHARMAssemblyFunctions.ml | 60 ++++--- .../bchlibarm32/bCHARMAssemblyInstructions.ml | 22 ++- CodeHawk/CHB/bchlibarm32/bCHARMMetrics.ml | 55 ++++--- .../bchlibarm32/bCHConstructARMFunction.ml | 69 +++++--- CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml | 58 +++++-- .../CHB/bchlibarm32/bCHFnARMDictionary.ml | 149 ++++++++++++------ .../bchlibarm32/bCHFnARMTypeConstraints.ml | 17 +- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 36 ++++- 10 files changed, 401 insertions(+), 150 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index 85edb454d..6077f12e9 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml @@ -30,6 +30,7 @@ open CHLogger open CHXmlDocument (* bchlib *) +open BCHBasicTypes open BCHBCTypes open BCHByteUtilities open BCHFloc @@ -54,6 +55,9 @@ let bd = BCHDictionary.bdictionary let bcd = BCHBCDictionary.bcdictionary let mmap = BCHGlobalMemoryMap.global_memory_map +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + class fn_analysis_results_t (fn:arm_assembly_function_int) = object (self) @@ -69,7 +73,18 @@ object (self) (node:xml_element_int) (ctxtiaddr:ctxt_iaddress_t) (instr:arm_assembly_instruction_int) = - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + match ctxt_string_to_location faddr ctxtiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"write_xml_instruction" + ~msg:ctxtiaddr __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR "write_xml_instruction"])) + end in let floc = get_floc loc in let espoffset = floc#get_stackpointer_offset "arm" in let has_control_flow = diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunction.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunction.ml index d3be3118a..1d42306f8 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunction.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunction.ml @@ -48,6 +48,9 @@ module TR = CHTraceResult let id = BCHInterfaceDictionary.interface_dictionary +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + let armreg_compare r1 r2 = Stdlib.compare (armreg_to_string r1) (armreg_to_string r2) @@ -348,17 +351,24 @@ let inline_blocks let _ = chlog#add "to be inlined" (STR s) in let succblock = f#get_block s in let ctxt = BlockContext block#get_first_address in - let newctxtstr = add_ctxt_to_ctxt_string faddr s ctxt in - let _ = - if H.mem newblocks newctxtstr then - () - else - let newblock = - make_block_ctxt_arm_assembly_block ctxt succblock in - H.add newblocks newctxtstr newblock in - let thisnewblock = - update_arm_assembly_block_successors block s [newctxtstr] in - H.replace newblocks baddr thisnewblock) block#get_successors; + TR.tfold + ~ok:(fun newctxtstr -> + let _ = + if H.mem newblocks newctxtstr then + () + else + let newblock = + make_block_ctxt_arm_assembly_block ctxt succblock in + H.add newblocks newctxtstr newblock in + let thisnewblock = + update_arm_assembly_block_successors block s [newctxtstr] in + H.replace newblocks baddr thisnewblock) + ~error:(fun e -> + log_error_result + ~tag:"inline_blocks" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (add_ctxt_to_ctxt_string faddr s ctxt)) block#get_successors; List.iter process_block block#get_successors end in let _ = process_block faddr#to_hex_string in @@ -386,19 +396,29 @@ let create_path_contexts let rec create_path (p: string) (s: ctxt_iaddress_t) = let pblock = f#get_block s in let ctxt = PathContext p in - let pctxtaddr = add_ctxt_to_ctxt_string faddr s ctxt in - if H.mem newblocks pctxtaddr then - pctxtaddr - else - (* add first to avoid infinite recursion for loop *) - let _ = H.add newblocks pctxtaddr pblock in - let psucc = pblock#get_successors in - let new_succ = List.map (create_path p) psucc in - let newblock = make_ctxt_arm_assembly_block ctxt pblock new_succ in - begin - H.replace newblocks pctxtaddr newblock; - pctxtaddr - end in + TR.tfold + ~ok:(fun pctxtaddr -> + if H.mem newblocks pctxtaddr then + pctxtaddr + else + (* add first to avoid infinite recursion for loop *) + let _ = H.add newblocks pctxtaddr pblock in + let psucc = pblock#get_successors in + let new_succ = List.map (create_path p) psucc in + let newblock = make_ctxt_arm_assembly_block ctxt pblock new_succ in + begin + H.replace newblocks pctxtaddr newblock; + pctxtaddr + end) + ~error:(fun e -> + begin + log_error_result + ~tag:"create_patch_contexts" ~msg:s __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR "create_path_contexts"])) + end) + (add_ctxt_to_ctxt_string faddr s ctxt) in let rec process_block (baddr: ctxt_iaddress_t) = if H.mem newblocks baddr then diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunctions.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunctions.ml index 14d4d5840..aeaaacfd8 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunctions.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunctions.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2024 Aarno Labs, LLC + Copyright (c) 2021-2026 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 @@ -338,11 +338,19 @@ object (self) method get_function_coverage = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"get_function_coverage" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let add_library_stub_instr (iaddr:doubleword_int) = if H.mem table iaddr#index then () @@ -375,11 +383,19 @@ object (self) method private get_live_instructions = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"get_live_instructions" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let add_library_stub_instr (iaddr: doubleword_int) = if H.mem table iaddr#index then () @@ -403,13 +419,21 @@ object (self) method private get_duplicate_instructions = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - let entry = - if H.mem table a#index then - H.find table a#index - else - [] in - H.add table a#index (faddr#to_hex_string :: entry) in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + let entry = + if H.mem table a#index then + H.find table a#index + else + [] in + H.add table a#index (faddr#to_hex_string :: entry)) + ~error:(fun e -> + log_error_result + ~tag:"get_duplicate_instructions" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let _ = List.iter (fun f -> f#iteri (fun faddr a _ -> add faddr a)) self#get_functions in diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml index 10422855c..829f31166 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2025 Aarno Labs, LLC + Copyright (c) 2021-2026 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 @@ -1136,15 +1136,25 @@ let get_associated_test_instr if finfo#has_associated_cc_setter ctxtiaddr then let faddr = finfo#get_address in let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in - let testloc = BCHLocation.ctxt_string_to_location faddr testiaddr in - let testaddr = testloc#i in TR.tfold - ~ok:(fun testinstr -> Some (testloc, testinstr)) + ~ok:(fun testloc -> + let testaddr = testloc#i in + TR.tfold + ~ok:(fun testinstr -> Some (testloc, testinstr)) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ e; + None + end) + (get_arm_assembly_instruction testaddr)) ~error:(fun e -> begin - log_error_result __FILE__ __LINE__ e; + log_error_result + ~tag:"get_associated_test_instr" + ~msg:ctxtiaddr + __FILE__ __LINE__ e; None end) - (get_arm_assembly_instruction testaddr) + (BCHLocation.ctxt_string_to_location faddr testiaddr) else None diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMMetrics.ml b/CodeHawk/CHB/bchlibarm32/bCHARMMetrics.ml index 4dab9874b..699870295 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMMetrics.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMMetrics.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -25,6 +25,9 @@ SOFTWARE. ============================================================================= *) +(* chutil *) +open CHLogger + (* bchlib *) open BCHFloc open BCHLibTypes @@ -88,17 +91,24 @@ let get_arm_op_metrics (f:arm_assembly_function_int) (_finfo:function_info_int) match ops with | [] -> () | _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - List.iter (fun (op: arm_operand_int) -> - match op#get_mode with - | RD -> add_reads floc op - | WR -> add_writes floc op - | RW -> - begin - add_reads floc op; - add_writes floc op - end) ops) in + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + List.iter (fun (op: arm_operand_int) -> + match op#get_mode with + | RD -> add_reads floc op + | WR -> add_writes floc op + | RW -> + begin + add_reads floc op; + add_writes floc op + end) ops) + ~error:(fun e -> + log_error_result + ~tag: "get_arm_op_metrics" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr)) in (!reads, !qreads, !writes, !qwrites) @@ -110,13 +120,20 @@ let get_arm_stackpointer_metrics let _ = f#iteri (fun _ ctxtiaddr _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - let (_,range) = floc#get_stackpointer_offset "arm" in - if range#isTop then - esptop := !esptop + 1 - else match range#singleton with - Some _ -> () | _ -> esprange := !esprange + 1) in + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + let (_,range) = floc#get_stackpointer_offset "arm" in + if range#isTop then + esptop := !esptop + 1 + else match range#singleton with + Some _ -> () | _ -> esprange := !esprange + 1) + ~error:(fun e -> + log_error_result + ~tag:"get_arm_stackpointer_metrics" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr)) in (!esptop, !esprange) diff --git a/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml b/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml index 43fc688b3..5a37797ac 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHConstructARMFunction.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2022-2025 Aarno Labs LLC + Copyright (c) 2022-2026 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 @@ -51,9 +51,11 @@ open BCHARMAssemblyInstructions open BCHARMTypes open BCHLocation - module TR = CHTraceResult +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + module DoublewordCollections = CHCollections.Make ( struct @@ -402,29 +404,40 @@ let construct_arm_assembly_block let exitixs = b#exit_edges_indices in let (_, xix, succ) = List.fold_left (fun (ix, xix, acc) s -> - match xix with - | [] -> - (ix + 1, - [], - (add_ctxt_to_ctxt_string faddr s functioncontext) - :: acc) - | h :: tl when ix = h -> - (ix + 1, - tl, - inline_exit - :: (add_ctxt_to_ctxt_string faddr s functioncontext) - :: acc) - | _ -> - (ix + 1, - xix, - (add_ctxt_to_ctxt_string faddr s functioncontext) - :: acc)) + TR.tfold + ~ok:(fun newctxtstr -> + match xix with + | [] -> + (ix + 1, [], newctxtstr :: acc) + | h :: tl when ix = h -> + (ix + 1, tl, inline_exit :: newctxtstr :: acc) + | _ -> + (ix + 1, xix, newctxtstr :: acc)) + ~error:(fun e -> + begin + log_error_result + ~tag:"get_inlined_call_blocks" + ~msg:inline_exit + __FILE__ __LINE__ e; + (ix + 1, xix, acc) + end) + (add_ctxt_to_ctxt_string faddr s functioncontext)) (1, exitixs, []) l in (* add exits for remaining exit indices *) succ @ (List.map (fun _ -> inline_exit) xix) else List.map (fun s -> - add_ctxt_to_ctxt_string faddr s functioncontext) l in + let newctxtstr = + add_ctxt_to_ctxt_string faddr s functioncontext in + match newctxtstr with + | Ok ctxtstr -> ctxtstr + | Error e -> + begin + log_error_result ~tag:"inlinedblocks"__FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR s])) + end) l in make_ctxt_arm_assembly_block functioncontext b succ) inlinedfn#get_blocks in @@ -572,7 +585,21 @@ let construct_arm_assembly_function let newfnentries = new DoublewordCollections.set_t in let workset = new DoublewordCollections.set_t in let doneset = new DoublewordCollections.set_t in - let get_iaddr s = (ctxt_string_to_location faddr s)#i in + let get_ctxt_loc s = + match ctxt_string_to_location faddr s with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"construct_arm_assembly_function" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR s; STR ": "; + STR (String.concat "; " e)])) + end in + let get_iaddr s = (get_ctxt_loc s)#i in let add_to_workset l = List.iter (fun a -> if doneset#has a then () else workset#add a) l in let set_block_entry (baddr: doubleword_int) = diff --git a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml index 6629a11c7..b1251d1f1 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHDisassembleARM.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2024 Aarno Labs, LLC + Copyright (c) 2021-2026 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 @@ -67,6 +67,8 @@ open BCHDisassembleThumbInstruction module H = Hashtbl module TR = CHTraceResult +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " let log_error (tag: string) (msg: string): tracelogspec_t = mk_tracelog_spec ~tag:("disassemble-arm:" ^ tag) msg @@ -836,9 +838,16 @@ let record_call_targets_arm () = | BranchLinkExchange (_, op) -> if finfo#has_call_target ctxtiaddr && not (finfo#get_call_target ctxtiaddr)#is_unknown then - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - floc#update_call_target + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + floc#update_call_target) + ~error:(fun e -> + log_error_result + ~tag:"record_call_targets_arm" + ~msg:ctxtiaddr + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr) else if op#is_absolute_address then begin match get_so_target op#get_absolute_address instr with @@ -862,9 +871,16 @@ let record_call_targets_arm () = tgt#get_absolute_address -> if finfo#has_call_target ctxtiaddr && not (finfo#get_call_target ctxtiaddr)#is_unknown then - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - floc#update_call_target + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + floc#update_call_target) + ~error:(fun e -> + log_error_result + ~tag:"record_call_targets_arm" + ~msg:ctxtiaddr + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr) else begin match get_so_target tgt#get_absolute_address instr with @@ -911,7 +927,20 @@ let associate_condition_code_users () = (ctxtiaddr:ctxt_iaddress_t) (block: arm_assembly_block_int) = let finfo = get_function_info faddr in - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + match ctxt_string_to_location faddr ctxtiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"associate_condition_code_users:set_condition" + ~msg:ctxtiaddr + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR ctxtiaddr; STR ": "; + STR (String.concat "; " e)])) + end in let revInstrs: arm_assembly_instruction_int list = block#get_instructions_rev ~high:loc#i () in @@ -937,9 +966,16 @@ let associate_condition_code_users () = | [] -> set tl | flags_set -> if List.for_all (fun fUsed -> List.mem fUsed flags_set) flags_used then - let iloc = ctxt_string_to_location faddr ctxtiaddr in - let instrctxt = (make_i_location iloc instr#get_address)#ci in - finfo#connect_cc_user ctxtiaddr instrctxt in + TR.tfold + ~ok:(fun iloc -> + let instrctxt = (make_i_location iloc instr#get_address)#ci in + finfo#connect_cc_user ctxtiaddr instrctxt) + ~error:(fun e -> + log_error_result + ~tag:"associate_condition_code_users:set_condition" + ~msg:ctxtiaddr + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr) in set revInstrs in let count = ref 0 in arm_assembly_functions#itera diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 9cbb7ad5e..e7d27cdb1 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -81,13 +81,13 @@ let p2s = CHPrettyUtil.pretty_to_string let x2s x = p2s (x2p x) let x_r2s x_r = TR.tfold_default x2s "error-value" x_r -let log_error (tag: string) (msg: string): tracelogspec_t = - mk_tracelog_spec ~tag:("FnARMDictionary:" ^ tag) msg - let ixd = BCHInterfaceDictionary.interface_dictionary let bcd = BCHBCDictionary.bcdictionary +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + class arm_opcode_dictionary_t (faddr:doubleword_int) @@ -222,18 +222,29 @@ object (self) if varssize = 1 then let xvar = List.hd vars in if floc#env#is_frozen_test_value xvar then - log_tfold - (log_error "index_instr" "invalid test address") - ~ok:(fun (testvar, testiaddr, _) -> - let testloc = ctxt_string_to_location floc#fa testiaddr in - let testfloc = get_floc testloc in - let extxprs = testfloc#inv#get_external_exprs testvar in - let extxprs = - List.map (fun e -> substitute_expr (fun _v -> e) xpr) extxprs in - (match extxprs with - | [] -> xpr - | _ -> List.hd extxprs)) - ~error:(fun _ -> xpr) + TR.tfold + ~ok:(fun (testvar, testiaddr, _) -> + TR.tfold + ~ok:(fun testloc -> + let testfloc = get_floc testloc in + let extxprs = testfloc#inv#get_external_exprs testvar in + let extxprs = + List.map (fun e -> substitute_expr (fun _v -> e) xpr) extxprs in + (match extxprs with + | [] -> xpr + | _ -> List.hd extxprs)) + ~error:(fun e -> + begin + log_error_result + ~tag:"rewrite_expr" ~msg:testiaddr __FILE__ __LINE__ e; + xpr + end) + (ctxt_string_to_location floc#fa testiaddr)) + ~error:(fun e -> + begin + log_error_result ~tag:"rewrite_expr" __FILE__ __LINE__ e; + xpr + end) (floc#env#get_frozen_variable xvar) else xpr @@ -261,33 +272,59 @@ object (self) let xpr = floc#inv#rewrite_expr x in simplify_xpr xpr in let rewrite_test_expr (csetter: ctxt_iaddress_t) (x: xpr_t) = - let testloc = ctxt_string_to_location floc#fa csetter in - let testfloc = get_floc testloc in - let xpr = testfloc#inv#rewrite_expr x in - let xpr = - let vars = variables_in_expr xpr in - let varssize = List.length vars in - if varssize = 1 then - let xvar = List.hd vars in - if floc#env#is_frozen_test_value xvar then - log_tfold - (log_error "rewrite_test_expr" "invalid test address") - ~ok:(fun (testvar, testiaddr, _) -> - let testloc = ctxt_string_to_location floc#fa testiaddr in - let testfloc = get_floc testloc in - let extxprs = testfloc#inv#get_external_exprs testvar in - let extxprs = - List.map (fun e -> substitute_expr (fun _v -> e) xpr) extxprs in - (match extxprs with - | [] -> xpr - | _ -> List.hd extxprs)) - ~error:(fun _ -> xpr) - (floc#env#get_frozen_variable xvar) - else - xpr - else - xpr in - simplify_xpr xpr in + TR.tfold + ~ok:(fun testloc -> + let testfloc = get_floc testloc in + let xpr = testfloc#inv#rewrite_expr x in + let xpr = + let vars = variables_in_expr xpr in + let varssize = List.length vars in + if varssize = 1 then + let xvar = List.hd vars in + if floc#env#is_frozen_test_value xvar then + TR.tfold + ~ok:(fun (testvar, testiaddr, _) -> + TR.tfold + ~ok:(fun testloc -> + let testfloc = get_floc testloc in + let extxprs = testfloc#inv#get_external_exprs testvar in + let extxprs = + List.map (fun e -> substitute_expr (fun _v -> e) xpr) extxprs in + (match extxprs with + | [] -> xpr + | _ -> List.hd extxprs)) + ~error:(fun e -> + begin + log_error_result + ~tag:"rewrite_floc_expr" + ~msg:testiaddr + __FILE__ __LINE__ e; + xpr + end) + (ctxt_string_to_location floc#fa testiaddr)) + ~error:(fun e -> + begin + log_error_result + ~tag:"rewrite_floc_expr" + ~msg:csetter + __FILE__ __LINE__ e; + xpr + end) + (floc#env#get_frozen_variable xvar) + else + xpr + else + xpr in + simplify_xpr xpr) + ~error:(fun e -> + begin + log_error_result + ~tag:"rewrite_floc_expr" + ~msg:csetter + __FILE__ __LINE__ e; + x + end) + (ctxt_string_to_location floc#fa csetter) in let rewrite_in_cc_context (floc: floc_int) (cc: arm_opcode_cc_t) (x: xpr_t): xpr_t = @@ -2031,7 +2068,19 @@ object (self) let ctxtiaddr = floc#l#ci in if finfo#has_associated_cc_setter ctxtiaddr then let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in - let testloc = ctxt_string_to_location faddr testiaddr in + let testloc = + match ctxt_string_to_location faddr testiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"IfThen" + ~msg:floc#cia + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in let testaddr = testloc#i in let testinstr = fail_tvalue @@ -2079,7 +2128,19 @@ object (self) let txpr = floc#get_test_expr in let fxpr = XOp (XLNot, [txpr]) in let csetter = floc#f#get_associated_cc_setter floc#cia in - let testloc = ctxt_string_to_location floc#fa csetter in + let testloc = + match ctxt_string_to_location floc#fa csetter with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"IfThen" + ~msg:csetter + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in let tcond = rewrite_test_expr csetter txpr in let fcond = rewrite_test_expr csetter fxpr in let instr = diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 26c1a0799..e683bbe47 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -40,6 +40,7 @@ open XprUtil open Xsimplify (* bchlib *) +open BCHBasicTypes open BCHBCFiles open BCHBCTypePretty open BCHBCTypes @@ -68,10 +69,9 @@ let p2s = CHPrettyUtil.pretty_to_string let x2s x = p2s (x2p x) -(* let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) let elocm (line: int): string = (eloc line) ^ ": " - *) + class arm_fn_type_constraints_t (store: type_constraint_store_int) @@ -107,7 +107,18 @@ object (self) method private record_instr_type_constraints (iaddr: ctxt_iaddress_t) (instr: arm_assembly_instruction_int) = - let loc = ctxt_string_to_location faddrdw iaddr in + let loc = + match ctxt_string_to_location faddrdw iaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"record_instr_type_constraints" + ~msg:iaddr __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR "record_instr_type_constraints"])) + end in let floc = get_floc loc in let rewrite_expr (x: xpr_t): xpr_t = let x = floc#inv#rewrite_expr x in diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index aae2184be..c57e0bd86 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -77,6 +77,9 @@ let p2s = CHPrettyUtil.pretty_to_string let x2s x = p2s (x2p x) let x_r2s x_r = TR.tfold_default x2s "error-value" x_r +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + let log_error (tag: string) (msg: string): tracelogspec_t = mk_tracelog_spec ~tag:("TranslateARMToCHIF:" ^ tag) msg @@ -91,7 +94,20 @@ let translate_arm_instruction let (ctxtiaddr, instr) = codepc#get_next_instruction in let faddr = funloc#f in let finfo = get_function_info faddr in - let loc = ctxt_string_to_location faddr ctxtiaddr in (* instr location *) + let loc = + match ctxt_string_to_location faddr ctxtiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"translate_arm_instruction" + ~msg:ctxtiaddr + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR ctxtiaddr; STR ": "; + STR (String.concat "; " e)])) + end in let invlabel = get_invariant_label loc in let invop = OPERATION {op_name = invlabel; op_args = []} in let bwdinvlabel = get_invariant_label ~bwd:true loc in @@ -653,8 +669,22 @@ let translate_arm_instruction package_terminator_transactions finfo blocklabel cmds thencode elsecode in if finfo#has_associated_cc_setter ctxtiaddr then let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in - let testloc = ctxt_string_to_location faddr testiaddr in - let testaddr = (ctxt_string_to_location faddr testiaddr)#i in + let testloc = + match ctxt_string_to_location faddr testiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"translate_arm_instruction:Branch" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["testiaddr: " ^ testiaddr]; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR ctxtiaddr; STR " -> "; + STR testiaddr; STR (String.concat "; " e)])) + end in + let testaddr = testloc#i in let testinstr = fail_tvalue (trerror_record From 28d415474685e27de252f47ed72916ab2f613ab2 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 9 Sep 2026 13:08:33 -0700 Subject: [PATCH 18/22] CHB:MIPS: add error handling for location context --- .../CHB/bchlibmips32/bCHDisassembleMIPS.ml | 20 ++++--- .../bchlibmips32/bCHMIPSAnalysisResults.ml | 35 +++++++----- .../CHB/bchlibmips32/bCHMIPSAssemblyBlock.ml | 5 +- .../bchlibmips32/bCHMIPSAssemblyFunction.ml | 48 ++++++++++------- .../bchlibmips32/bCHMIPSAssemblyFunctions.ml | 38 +++++++++---- CodeHawk/CHB/bchlibmips32/bCHMIPSMetrics.ml | 54 +++++++++++++------ .../bchlibmips32/bCHTranslateMIPSToCHIF.ml | 4 +- 7 files changed, 135 insertions(+), 69 deletions(-) diff --git a/CodeHawk/CHB/bchlibmips32/bCHDisassembleMIPS.ml b/CodeHawk/CHB/bchlibmips32/bCHDisassembleMIPS.ml index fac284891..3ae666134 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHDisassembleMIPS.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHDisassembleMIPS.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -692,7 +692,10 @@ let trace_block match b#get_successors with | [] -> [(make_location {loc_faddr = faddr; loc_iaddr = returnsite})#ci] - | l -> List.map (fun s -> add_ctxt_to_ctxt_string faddr s ctxt) l in + | l -> + List.map + (fun s -> + TR.tget_ok (add_ctxt_to_ctxt_string faddr s ctxt)) l in make_ctxt_mips_assembly_block ctxt b succ) fn#get_blocks in Ok (Some [callsucc], va, inlinedblocks) else @@ -748,7 +751,7 @@ let trace_function (faddr:doubleword_int): mips_assembly_function_int = ~ok:(fun instr -> instr#set_block_entry) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) (get_mips_assembly_instruction baddr) in - let get_iaddr s = (ctxt_string_to_location faddr s)#i in + let get_iaddr s = (TR.tget_ok (ctxt_string_to_location faddr s))#i in let add_to_workset l = List.iter (fun a -> if doneSet#has a then () else workSet#add a) l in let blocks = ref [] in @@ -861,7 +864,8 @@ let record_call_targets () = | JumpLink op -> if finfo#has_call_target ctxtiaddr && not (finfo#get_call_target ctxtiaddr)#is_unknown then - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in floc#update_call_target else @@ -875,9 +879,11 @@ let record_call_targets () = ctxtiaddr (mk_app_target op#get_absolute_address) end | JumpLinkRegister (_ra, _op) -> - let iaddr = (ctxt_string_to_location faddr ctxtiaddr)#i in + let iaddr = + (TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr))#i in if finfo#has_call_target ctxtiaddr then - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in floc#update_call_target else if system_info#has_call_target faddr iaddr then @@ -1066,7 +1072,7 @@ let resolve_indirect_mips_calls (f:mips_assembly_function_int) = let _ = f#iteri (fun faddr ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in match instr#get_opcode with | JumpLinkRegister (_ra, tgt) -> let floc = get_floc loc in diff --git a/CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml b/CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml index 911d54834..72da79e7d 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHMIPSAnalysisResults.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -28,6 +28,7 @@ ============================================================================= *) (* chutil *) +open CHLogger open CHXmlDocument (* bchlib *) @@ -46,6 +47,8 @@ open BCHMIPSLoopStructure open BCHMIPSDictionary module H = Hashtbl +module TR = CHTraceResult + class fn_analysis_results_t (fn:mips_assembly_function_int) = object (self) @@ -65,19 +68,27 @@ object (self) None method private write_xml_instruction - (node:xml_element_int) (ctxtiaddr:ctxt_iaddress_t) + (node:xml_element_int) + (ctxtiaddr:ctxt_iaddress_t) (instr:mips_assembly_instruction_int) (restriction:block_restriction_t option) = - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - let espoffset = floc#get_stackpointer_offset "mips" in - begin - mips_dictionary#write_xml_mips_opcode node instr#get_opcode; - id#write_xml_instr node instr floc restriction; - id#write_xml_sp_offset node espoffset; - mips_dictionary#write_xml_mips_bytestring - node (byte_string_to_printed_string instr#get_instruction_bytes) - end + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + let espoffset = floc#get_stackpointer_offset "mips" in + begin + mips_dictionary#write_xml_mips_opcode node instr#get_opcode; + id#write_xml_instr node instr floc restriction; + id#write_xml_sp_offset node espoffset; + mips_dictionary#write_xml_mips_bytestring + node (byte_string_to_printed_string instr#get_instruction_bytes) + end) + ~error:(fun e -> + log_error_result + ~tag:"write_xml_instruction" + ~msg:ctxtiaddr + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr) method private write_xml_instructions (node:xml_element_int) = fn#itera (fun baddr block -> diff --git a/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyBlock.ml b/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyBlock.ml index aa85f0565..c15b4b7e6 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyBlock.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyBlock.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-2026 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 @@ -167,7 +167,8 @@ let make_ctxt_mips_assembly_block :mips_assembly_block_int = let bsucc = b#get_successors in let faddr = b#get_faddr in - let succ = List.map (fun s -> add_ctxt_to_ctxt_string faddr s newctxt) bsucc in + let succ = + List.map (fun s -> TR.tget_ok (add_ctxt_to_ctxt_string faddr s newctxt)) bsucc in make_mips_assembly_block ~ctxt:(newctxt :: b#get_context) b#get_faddr diff --git a/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyFunction.ml b/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyFunction.ml index 14f8dd49c..52c9071b7 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyFunction.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyFunction.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ open BCHMIPSDisassemblyUtils open BCHMIPSTypes module H = Hashtbl +module TR = CHTraceResult class mips_assembly_function_t @@ -180,27 +181,34 @@ let inline_blocks if is_to_be_inlined s then let succblock = f#get_block s in let ctxt = BlockContext block#get_first_address in - let newctxtstr = add_ctxt_to_ctxt_string faddr s ctxt in - let _ = - if H.mem newblocks newctxtstr then - () - else - let newblock = - make_block_ctxt_mips_assembly_block ctxt succblock in + TR.tfold + ~ok:(fun newctxtstr -> + let _ = + if H.mem newblocks newctxtstr then + () + else + let newblock = + make_block_ctxt_mips_assembly_block ctxt succblock in + begin + chlog#add + "mips assembly block: add context" + (LBLOCK [faddr#toPretty; STR ": "; STR newctxtstr]); + H.add newblocks newctxtstr newblock + end in + let thisnewblock = + update_mips_assembly_block_successors block s newctxtstr in begin + H.replace newblocks baddr thisnewblock; chlog#add - "mips assembly block: add context" - (LBLOCK [faddr#toPretty; STR ": "; STR newctxtstr]); - H.add newblocks newctxtstr newblock - end in - let thisnewblock = - update_mips_assembly_block_successors block s newctxtstr in - begin - H.replace newblocks baddr thisnewblock; - chlog#add - "mips assembly block: replace successor" - (LBLOCK [faddr#toPretty; STR ": "; STR baddr]) - end) block#get_successors; + "mips assembly block: replace successor" + (LBLOCK [faddr#toPretty; STR ": "; STR baddr]) + end) + ~error:(fun e -> + log_error_result + ~tag:"inline_blocks" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (add_ctxt_to_ctxt_string faddr s ctxt)) block#get_successors; List.iter process_block block#get_successors end in let _ = process_block faddr#to_hex_string in diff --git a/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyFunctions.ml b/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyFunctions.ml index edaabeee3..a2dc13fad 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyFunctions.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHMIPSAssemblyFunctions.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -259,11 +259,19 @@ object (self) method get_function_coverage = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"get_function_coverage" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let _ = List.iter (fun f -> f#iteri (fun faddr a _ -> add faddr a)) self#get_functions in @@ -357,11 +365,19 @@ object (self) method private get_live_instructions = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"get_live_instructions" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let _ = List.iter (fun f -> f#iteri (fun faddr a _ -> add faddr a)) self#get_functions in diff --git a/CodeHawk/CHB/bchlibmips32/bCHMIPSMetrics.ml b/CodeHawk/CHB/bchlibmips32/bCHMIPSMetrics.ml index d9775fa5c..f6fbea416 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHMIPSMetrics.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHMIPSMetrics.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -27,6 +27,9 @@ SOFTWARE. ============================================================================= *) +(* chutil *) +open CHLogger + (* bchlib *) open BCHFloc open BCHLibTypes @@ -37,6 +40,8 @@ open BCHMIPSLoopStructure open BCHMIPSOpcodeRecords open BCHMIPSTypes +module TR = CHTraceResult + let get_mips_op_metrics (f:mips_assembly_function_int) (finfo:function_info_int) = @@ -67,13 +72,24 @@ let get_mips_op_metrics match ops with | [] -> () | _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - List.iter (fun (op:mips_operand_int) -> - match op#get_mode with - | RD -> add_read floc op - | WR -> add_write floc op - | RW -> begin add_read floc op ; add_write floc op end) ops) in + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + List.iter (fun (op:mips_operand_int) -> + match op#get_mode with + | RD -> add_read floc op + | WR -> add_write floc op + | RW -> + begin + add_read floc op; + add_write floc op + end) ops) + ~error:(fun e -> + log_error_result + ~tag:"get_mips_op_metrics" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr)) in (!reads,!qreads,!writes,!qwrites) @@ -85,13 +101,21 @@ let get_mips_stackpointer_metrics let _ = f#iteri (fun _ ctxtiaddr _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - let (_,range) = floc#get_stackpointer_offset "mips" in - if range#isTop then - esptop := !esptop + 1 - else match range#singleton with - Some _ -> () | _ -> esprange := !esprange + 1) in + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + let (_,range) = floc#get_stackpointer_offset "mips" in + if range#isTop then + esptop := !esptop + 1 + else + match range#singleton with + | Some _ -> () | _ -> esprange := !esprange + 1) + ~error:(fun e -> + log_error_result + ~tag:"get_mips_stackpointer_metrics" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr)) in (!esptop,!esprange) diff --git a/CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml b/CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml index f476616ef..9c27eea95 100644 --- a/CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml +++ b/CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -258,7 +258,7 @@ let translate_mips_instruction ~(cmds:cmd_t list) = (* commands carried over *) let (ctxtiaddr,instr) = codepc#get_next_instruction in let faddr = funloc#f in - let loc = ctxt_string_to_location faddr ctxtiaddr in (* instr location *) + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let finfo = get_function_info faddr in let env = finfo#env in let invlabel = get_invariant_label loc in From 26e4f99979a16e1a1aa8b4bdc3380e7060bc0cfa Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 9 Sep 2026 13:09:10 -0700 Subject: [PATCH 19/22] CHB:Power32: add error handling for location context --- .../bCHConstructPowerFunction.ml | 4 +- .../CHB/bchlibpower32/bCHDisassemblePower.ml | 9 ++-- .../CHB/bchlibpower32/bCHFnPowerDictionary.ml | 51 +++++++++++++------ .../bchlibpower32/bCHPowerAnalysisResults.ml | 31 +++++++---- .../bCHPowerAssemblyFunctions.ml | 40 ++++++++++----- CodeHawk/CHB/bchlibpower32/bCHPowerMetrics.ml | 30 +++++++---- .../bchlibpower32/bCHTranslatePowerToCHIF.ml | 8 +-- 7 files changed, 115 insertions(+), 58 deletions(-) diff --git a/CodeHawk/CHB/bchlibpower32/bCHConstructPowerFunction.ml b/CodeHawk/CHB/bchlibpower32/bCHConstructPowerFunction.ml index af1e43827..4f49a1cd7 100644 --- a/CodeHawk/CHB/bchlibpower32/bCHConstructPowerFunction.ml +++ b/CodeHawk/CHB/bchlibpower32/bCHConstructPowerFunction.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023-2025 Aarno Labs LLC + Copyright (c) 2023-2026 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 @@ -285,7 +285,7 @@ let construct_pwr_assembly_function let newfnentries = new DoublewordCollections.set_t in let workset = new DoublewordCollections.set_t in let doneset = new DoublewordCollections.set_t in - let get_iaddr s = (ctxt_string_to_location faddr s)#i in + let get_iaddr s = (TR.tget_ok (ctxt_string_to_location faddr s))#i in let add_to_workset l = List.iter (fun a -> if doneset#has a then () else workset#add a) l in let set_block_entry (baddr: doubleword_int) = diff --git a/CodeHawk/CHB/bchlibpower32/bCHDisassemblePower.ml b/CodeHawk/CHB/bchlibpower32/bCHDisassemblePower.ml index 7fc3eff0a..3d52d25db 100644 --- a/CodeHawk/CHB/bchlibpower32/bCHDisassemblePower.ml +++ b/CodeHawk/CHB/bchlibpower32/bCHDisassemblePower.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-2026 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 @@ -459,7 +459,8 @@ let record_call_targets_pwr () = | BranchLink (_, tgtop, _) -> if finfo#has_call_target ctxtiaddr && not (finfo#get_call_target ctxtiaddr)#is_unknown then - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in floc#update_call_target else if tgtop#is_absolute_address then @@ -484,7 +485,7 @@ let associate_condition_code_users_pwr () = (ctxtiaddr: ctxt_iaddress_t) (block: pwr_assembly_block_int) = let finfo = get_function_info faddr in - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let revInstrs: pwr_assembly_instruction_int list = block#get_instructions_rev ~high:loc#i () in @@ -510,7 +511,7 @@ let associate_condition_code_users_pwr () = match get_pwr_crfs_set instr#get_opcode with | [] -> set tl | crfs_set when List.mem crf_used crfs_set-> - let iloc = ctxt_string_to_location faddr ctxtiaddr in + let iloc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let instrctxt = (make_i_location iloc instr#get_address)#ci in finfo#connect_cc_user ctxtiaddr instrctxt | _ -> set tl in diff --git a/CodeHawk/CHB/bchlibpower32/bCHFnPowerDictionary.ml b/CodeHawk/CHB/bchlibpower32/bCHFnPowerDictionary.ml index 6aea69ed0..16fa2bff4 100644 --- a/CodeHawk/CHB/bchlibpower32/bCHFnPowerDictionary.ml +++ b/CodeHawk/CHB/bchlibpower32/bCHFnPowerDictionary.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-2026 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 @@ -63,6 +63,8 @@ module TR = CHTraceResult let x2p = xpr_formatter#pr_expr +let p2s = pretty_to_string + let log_error (tag: string) (msg: string): tracelogspec_t = mk_tracelog_spec ~tag:("FnPowerDictionary:"^ tag) msg @@ -120,19 +122,35 @@ object (self) if varssize = 1 then let xvar = List.hd vars in if floc#env#is_frozen_test_value xvar then - log_tfold - (log_error "index_instr" "invalid test address") - ~ok:(fun (testvar, testiaddr, _) -> - let testloc = ctxt_string_to_location floc#fa testiaddr in - let testfloc = get_floc testloc in - let extxprs = testfloc#inv#get_external_exprs testvar in - let extxprs = - List.map (fun e -> substitute_expr (fun _v -> e) xpr) extxprs in - (match extxprs with - | [] -> xpr - | _ -> List.hd extxprs)) - ~error:(fun _ -> xpr) - (floc#env#get_frozen_variable xvar) + TR.tfold + ~ok:(fun (testvar, testiaddr, _) -> + TR.tfold + ~ok:(fun testloc -> + let testfloc = get_floc testloc in + let extxprs = testfloc#inv#get_external_exprs testvar in + let extxprs = + List.map (fun e -> substitute_expr (fun _v -> e) xpr) extxprs in + (match extxprs with + | [] -> xpr + | _ -> List.hd extxprs)) + ~error:(fun e -> + begin + log_error_result + ~tag:"index_instr" + ~msg:(p2s floc#l#toPretty) + __FILE__ __LINE__ e; + xpr + end) + (ctxt_string_to_location floc#fa testiaddr)) + ~error:(fun e -> + begin + log_error_result + ~tag:"index_instr" + ~msg:(p2s floc#l#toPretty) + __FILE__ __LINE__ e; + xpr + end) + (floc#env#get_frozen_variable xvar) else xpr else @@ -156,7 +174,7 @@ object (self) end in let rewrite_test_expr (csetter: ctxt_iaddress_t) (x: xpr_t) = - let testloc = ctxt_string_to_location floc#fa csetter in + let testloc = TR.tget_ok (ctxt_string_to_location floc#fa csetter) in let testfloc = get_floc testloc in let xpr = testfloc#inv#rewrite_expr x in let xpr = @@ -168,7 +186,8 @@ object (self) log_tfold (log_error "rewrite_test_expr" "invalid test address") ~ok:(fun (testvar, testiaddr, _) -> - let testloc = ctxt_string_to_location floc#fa testiaddr in + let testloc = + TR.tget_ok (ctxt_string_to_location floc#fa testiaddr) in let testfloc = get_floc testloc in let extxprs = testfloc#inv#get_external_exprs testvar in let extxprs = diff --git a/CodeHawk/CHB/bchlibpower32/bCHPowerAnalysisResults.ml b/CodeHawk/CHB/bchlibpower32/bCHPowerAnalysisResults.ml index 039701356..4e207bec4 100644 --- a/CodeHawk/CHB/bchlibpower32/bCHPowerAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibpower32/bCHPowerAnalysisResults.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-2026 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 @@ -27,6 +27,7 @@ (* chutil *) +open CHLogger open CHXmlDocument (* bchlib *) @@ -45,6 +46,7 @@ open BCHPowerTypes module H = Hashtbl +module TR = CHTraceResult class fn_analysis_results_t (fn: pwr_assembly_function_int) = @@ -62,16 +64,23 @@ object (self) (node: xml_element_int) (ctxtiaddr: ctxt_iaddress_t) (instr: pwr_assembly_instruction_int) = - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - let espoffset = floc#get_stackpointer_offset "pwr" in - begin - pwr_dictionary#write_xml_pwr_opcode node instr#get_opcode; - id#write_xml_instr node instr floc; - id#write_xml_sp_offset node espoffset; - pwr_dictionary#write_xml_pwr_bytestring - node (byte_string_to_printed_string instr#get_instruction_bytes) - end + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + let espoffset = floc#get_stackpointer_offset "pwr" in + begin + pwr_dictionary#write_xml_pwr_opcode node instr#get_opcode; + id#write_xml_instr node instr floc; + id#write_xml_sp_offset node espoffset; + pwr_dictionary#write_xml_pwr_bytestring + node (byte_string_to_printed_string instr#get_instruction_bytes) + end) + ~error:(fun e -> + log_error_result + ~tag:"write_xml_instruction" + ~msg:ctxtiaddr + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr) method private write_xml_instructions (node: xml_element_int) = fn#itera diff --git a/CodeHawk/CHB/bchlibpower32/bCHPowerAssemblyFunctions.ml b/CodeHawk/CHB/bchlibpower32/bCHPowerAssemblyFunctions.ml index bd09ce078..2ecf45346 100644 --- a/CodeHawk/CHB/bchlibpower32/bCHPowerAssemblyFunctions.ml +++ b/CodeHawk/CHB/bchlibpower32/bCHPowerAssemblyFunctions.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023-2024 Aarno Labs, LLC + Copyright (c) 2023-2026 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 @@ -243,11 +243,19 @@ object (self) method get_function_coverage = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"get_function_coverage" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let add_library_stub_instr (iaddr: doubleword_int) = if H.mem table iaddr#index then () @@ -280,11 +288,19 @@ object (self) method private get_live_instructions = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"get_live_instrucitons" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let add_library_stub_instr (iaddr: doubleword_int) = if H.mem table iaddr#index then () @@ -308,7 +324,7 @@ object (self) method private get_duplicate_instructions = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in + let a = (TR.tget_ok (ctxt_string_to_location faddr ctxta))#i in let entry = if H.mem table a#index then H.find table a#index diff --git a/CodeHawk/CHB/bchlibpower32/bCHPowerMetrics.ml b/CodeHawk/CHB/bchlibpower32/bCHPowerMetrics.ml index 4b4f54e69..1db50602f 100644 --- a/CodeHawk/CHB/bchlibpower32/bCHPowerMetrics.ml +++ b/CodeHawk/CHB/bchlibpower32/bCHPowerMetrics.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-2026 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 @@ -25,6 +25,9 @@ SOFTWARE. ============================================================================= *) +(* chutil *) +open CHLogger + (* bchlib *) open BCHFloc open BCHLibTypes @@ -34,6 +37,8 @@ open BCHLocation open BCHPowerLoopStructure open BCHPowerTypes +module TR = CHTraceResult + let get_pwr_op_metrics (_f: pwr_assembly_function_int) (_finfo: function_info_int) = @@ -48,14 +53,21 @@ let get_pwr_stackpointer_metrics let _ = f#iteri (fun _ ctxtiaddr _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc loc in - let (_, range) = floc#get_stackpointer_offset "pwr" in - if range#isTop then - sptop := !sptop + 1 - else - match range#singleton with - | Some _ -> () | _ -> sprange := !sprange + 1) in + TR.tfold + ~ok:(fun loc -> + let floc = get_floc loc in + let (_, range) = floc#get_stackpointer_offset "pwr" in + if range#isTop then + sptop := !sptop + 1 + else + match range#singleton with + | Some _ -> () | _ -> sprange := !sprange + 1) + ~error:(fun e -> + log_error_result + ~tag:"get_pwr_stackpointer_metrics" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr)) in (!sptop, !sprange) diff --git a/CodeHawk/CHB/bchlibpower32/bCHTranslatePowerToCHIF.ml b/CodeHawk/CHB/bchlibpower32/bCHTranslatePowerToCHIF.ml index a76163f5c..9f3ccd34e 100644 --- a/CodeHawk/CHB/bchlibpower32/bCHTranslatePowerToCHIF.ml +++ b/CodeHawk/CHB/bchlibpower32/bCHTranslatePowerToCHIF.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-2026 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 @@ -265,7 +265,7 @@ let translate_pwr_instruction let (ctxtiaddr, instr) = codepc#get_next_instruction in let faddr = funloc#f in let finfo = get_function_info faddr in - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let invlabel = get_invariant_label loc in let invop = OPERATION {op_name = invlabel; op_args = []} in let bwdinvlabel = get_invariant_label ~bwd:true loc in @@ -336,8 +336,8 @@ let translate_pwr_instruction let transaction = package_transaction finfo blocklabel cmds in if finfo#has_associated_cc_setter ctxtiaddr then let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in - let testloc = ctxt_string_to_location faddr testiaddr in - let testaddr = (ctxt_string_to_location faddr testiaddr)#i in + let testloc = TR.tget_ok (ctxt_string_to_location faddr testiaddr) in + let testaddr = testloc#i in let testinstr = fail_tvalue (trerror_record From f728a6397ab81f11c338fae0c3fae3e032bc1e3a Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 9 Sep 2026 13:09:40 -0700 Subject: [PATCH 20/22] CHB:X86: add error handling for location context --- CodeHawk/CHB/bchlibx86/bCHAssemblyBlock.ml | 6 +- CodeHawk/CHB/bchlibx86/bCHAssemblyFunction.ml | 30 ++- .../CHB/bchlibx86/bCHAssemblyFunctions.ml | 72 ++++-- .../bCHAssemblyInstructionAnnotations.ml | 10 +- CodeHawk/CHB/bchlibx86/bCHDisassemble.ml | 215 +++++++++++++++--- CodeHawk/CHB/bchlibx86/bCHDisassembleELF.ml | 29 +-- CodeHawk/CHB/bchlibx86/bCHFnX86Dictionary.ml | 8 +- CodeHawk/CHB/bchlibx86/bCHPullData.ml | 14 +- CodeHawk/CHB/bchlibx86/bCHTranslateToCHIF.ml | 11 +- .../CHB/bchlibx86/bCHX86AnalysisResults.ml | 5 +- CodeHawk/CHB/bchlibx86/bCHX86Metrics.ml | 8 +- 11 files changed, 306 insertions(+), 102 deletions(-) diff --git a/CodeHawk/CHB/bchlibx86/bCHAssemblyBlock.ml b/CodeHawk/CHB/bchlibx86/bCHAssemblyBlock.ml index 83081c00e..0b5f0f915 100644 --- a/CodeHawk/CHB/bchlibx86/bCHAssemblyBlock.ml +++ b/CodeHawk/CHB/bchlibx86/bCHAssemblyBlock.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-2026 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,8 @@ open BCHAssemblyInstructionAnnotations open BCHAssemblyInstructions open BCHLibx86Types +module TR = CHTraceResult + class assembly_block_t ?(ctxt=[]) @@ -168,7 +170,7 @@ object (self) let pp = ref [] in let _ = self#itera (fun ctxtiaddr instr -> - let iloc = ctxt_string_to_location faddr ctxtiaddr in + let iloc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc iloc in let ann = create_annotation floc in pp := diff --git a/CodeHawk/CHB/bchlibx86/bCHAssemblyFunction.ml b/CodeHawk/CHB/bchlibx86/bCHAssemblyFunction.ml index 0c4a2ba04..be712d116 100644 --- a/CodeHawk/CHB/bchlibx86/bCHAssemblyFunction.ml +++ b/CodeHawk/CHB/bchlibx86/bCHAssemblyFunction.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -57,6 +57,7 @@ open BCHX86OpcodeRecords module H = Hashtbl module FFU = BCHFileFormatUtil +module TR = CHTraceResult class assembly_function_t @@ -136,10 +137,17 @@ object (self) let _ = self#iteri (fun faddr ctxtiaddr instr -> - let iloc = ctxt_string_to_location faddr ctxtiaddr in - let floc = get_floc iloc in - if instr#is_esp_manipulating floc then - result := ctxtiaddr :: !result) in + TR.tfold + ~ok:(fun iloc -> + let floc = get_floc iloc in + if instr#is_esp_manipulating floc then + result := ctxtiaddr :: !result) + ~error:(fun e -> + log_error_result + ~tag:"is_esp_manipulating" + ~msg:ctxtiaddr + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr)) in !result method get_stack_adjustment = @@ -148,7 +156,7 @@ object (self) let _ = self#iteri (fun faddr ctxtiaddr instr -> - let iloc = ctxt_string_to_location faddr ctxtiaddr in + let iloc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in if iloc#has_context then () else @@ -253,7 +261,7 @@ object (self) let _ = self#iteri (fun _ ctxtiaddr instr -> - let iloc = ctxt_string_to_location faddr ctxtiaddr in + let iloc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in match instr#get_opcode with | IndirectCall _ -> let floc = get_floc iloc in @@ -270,7 +278,7 @@ object (self) method populate_callgraph (callgraph:callgraph_int) = let finfo = get_function_info faddr in self#iteri (fun _ ctxtiaddr instr -> - let iloc = ctxt_string_to_location faddr ctxtiaddr in + let iloc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in match instr#get_opcode with DirectCall _ | IndirectCall _ | IndirectJmp _ -> let floc = get_floc iloc in @@ -341,7 +349,7 @@ object (self) method iter_calls (f:ctxt_iaddress_t -> floc_int -> unit) = self#iteri (fun _ ctxtiaddr instr -> - let iloc = ctxt_string_to_location faddr ctxtiaddr in + let iloc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in match instr#get_opcode with | DirectCall _ | IndirectCall _ -> f ctxtiaddr (get_floc iloc) | IndirectJmp _ @@ -485,7 +493,7 @@ let get_op_metrics (f:assembly_function_int) (finfo:function_info_int) = match ops with | [] -> () | _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in List.iter (fun (op:operand_int) -> match op#get_mode with @@ -503,7 +511,7 @@ let get_esp_metrics (f:assembly_function_int): (int * int) = let _ = f#iteri (fun _ ctxtiaddr _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in let (_, range) = floc#get_stackpointer_offset "x86" in if range#isTop then diff --git a/CodeHawk/CHB/bchlibx86/bCHAssemblyFunctions.ml b/CodeHawk/CHB/bchlibx86/bCHAssemblyFunctions.ml index c73a957b8..d7fe9bed5 100644 --- a/CodeHawk/CHB/bchlibx86/bCHAssemblyFunctions.ml +++ b/CodeHawk/CHB/bchlibx86/bCHAssemblyFunctions.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -216,11 +216,19 @@ object (self) method get_function_coverage = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"get_function_coverage" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let _ = List.iter (fun f -> f#iteri (fun faddr a _ -> add faddr a)) @@ -241,11 +249,17 @@ object (self) method add_functions_by_preamble = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"add_functions_by_preamble" __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let _ = List.iter (fun f -> f#iteri (fun faddr a _ -> add faddr a)) self#get_functions in @@ -291,11 +305,19 @@ object (self) method dark_matter_to_string = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"dark_matter_to_string" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let _ = List.iter (fun f -> f#iteri (fun faddr a _ -> add faddr a)) self#get_functions in @@ -306,11 +328,19 @@ object (self) method duplicates_to_string = let table = H.create 37 in let add faddr ctxta = - let a = (ctxt_string_to_location faddr ctxta)#i in - if H.mem table a#index then - H.replace table a#index ((H.find table a#index) + 1) - else - H.add table a#index 1 in + TR.tfold + ~ok:(fun loc -> + let a = loc#i in + if H.mem table a#index then + H.replace table a#index ((H.find table a#index) + 1) + else + H.add table a#index 1) + ~error:(fun e -> + log_error_result + ~tag:"duplicates_to_string" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxta) in let _ = List.iter (fun f -> f#iteri (fun faddr a _ -> add faddr a)) self#get_functions in diff --git a/CodeHawk/CHB/bchlibx86/bCHAssemblyInstructionAnnotations.ml b/CodeHawk/CHB/bchlibx86/bCHAssemblyInstructionAnnotations.ml index 81a63860f..347adc63b 100644 --- a/CodeHawk/CHB/bchlibx86/bCHAssemblyInstructionAnnotations.ml +++ b/CodeHawk/CHB/bchlibx86/bCHAssemblyInstructionAnnotations.ml @@ -251,8 +251,9 @@ let create_annotation_aux (floc:floc_int) = make_annotation Assignment (STR "nop") | Mov ( _, _,src) when src#is_function_argument -> - let (callSite, argIndex) = src#get_function_argument in - let callSiteFloc = get_floc (ctxt_string_to_location floc#fa callSite) in + let (callSite, argIndex) = src#get_function_argument in + let callSiteFloc = + get_floc (TR.tget_ok (ctxt_string_to_location floc#fa callSite)) in if callSiteFloc#has_call_target && callSiteFloc#get_call_target#is_signature_valid then let fintf = callSiteFloc#get_call_target#get_function_interface in @@ -1092,7 +1093,8 @@ let create_annotation_aux (floc:floc_int) = | Push (_, op) when op#is_function_argument -> let rhs = get_rhs op floc in let (callSite, argIndex) = op#get_function_argument in - let callSiteFloc = get_floc (ctxt_string_to_location floc#fa callSite) in + let callSiteFloc = + get_floc (TR.tget_ok (ctxt_string_to_location floc#fa callSite)) in if callSiteFloc#has_call_target && floc#get_call_target#is_signature_valid then let fintf = callSiteFloc#get_call_target#get_function_interface in @@ -1213,7 +1215,7 @@ let create_annotation_aux (floc:floc_int) = | Setcc (_, op) when floc#f#has_associated_cc_setter floc#cia -> let testIAddr = floc#f#get_associated_cc_setter floc#cia in - let testloc = ctxt_string_to_location floc#fa testIAddr in + let testloc = TR.tget_ok (ctxt_string_to_location floc#fa testIAddr) in let testAddr = testloc#i in let testopc = ((!assembly_instructions)#at_address testAddr)#get_opcode in let setopc = instr#get_opcode in diff --git a/CodeHawk/CHB/bchlibx86/bCHDisassemble.ml b/CodeHawk/CHB/bchlibx86/bCHDisassemble.ml index 8a6b08045..48360c356 100644 --- a/CodeHawk/CHB/bchlibx86/bCHDisassemble.ml +++ b/CodeHawk/CHB/bchlibx86/bCHDisassemble.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -89,6 +89,10 @@ let log_error (tag: string) (msg: string): tracelogspec_t = let pr_expr = xpr_formatter#pr_expr +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + + module DoublewordCollections = CHCollections.Make ( struct type t = doubleword_int @@ -1125,7 +1129,18 @@ let trace_block (faddr:doubleword_int) (baddr:doubleword_int) = | [] -> [(make_location {loc_faddr = faddr; loc_iaddr = returnsite})#ci] | l -> - List.map (fun s -> add_ctxt_to_ctxt_string faddr s ctxt) l in + List.map (fun s -> + let newctxtstr = add_ctxt_to_ctxt_string faddr s ctxt in + match newctxtstr with + | Ok ctxtstr -> ctxtstr + | Error e -> + begin + log_error_result + ~tag:"find_last_instruction" __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR s])) + end) l in make_ctxt_assembly_block ctxt b succ) fn#get_blocks in (Some [callsucc], va, inlinedblocks) else if !assembly_instructions#has_next_valid_instruction va then @@ -1148,7 +1163,20 @@ let trace_function (faddr:doubleword_int) = let workSet = new DoublewordCollections.set_t in (* toplevel only *) let doneSet = new DoublewordCollections.set_t in (* toplevel only *) let set_block_entry a = (!assembly_instructions#at_address a)#set_block_entry in - let get_iaddr s = (ctxt_string_to_location faddr s)#i in + let get_iaddr s = + TR.tfold + ~ok:(fun loc -> loc#i) + ~error:(fun e -> + begin + log_error_result + ~tag:"trace_function" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); faddr#toPretty; STR ": "; STR s])) + end) + (ctxt_string_to_location faddr s) in let add_to_workset l = List.iter (fun a -> if doneSet#has a then () else workSet#add a) l in let blocks = ref [] in @@ -1300,7 +1328,20 @@ let record_call_targets () = count := !count + 1; f#iteri (fun _ ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + match ctxt_string_to_location faddr ctxtiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"record_call_targets" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); + STR (String.concat "; " e)])) + end in let floc = get_floc loc in let iaddr = loc#i in match instr#get_opcode with @@ -1414,7 +1455,19 @@ let associate_condition_code_users () = let rec set l = match l with | [] -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + match ctxt_string_to_location faddr ctxtiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"associate_condition_code_users" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in disassembly_log#add "cc user without setter" (LBLOCK [ @@ -1425,9 +1478,16 @@ let associate_condition_code_users () = | [] -> set tl | flags_set -> if List.for_all (fun fUsed -> List.mem fUsed flags_set) flags_used then - let iloc = ctxt_string_to_location faddr ctxtiaddr in - let instrctxt = (make_i_location iloc instr#get_address)#ci in - finfo#connect_cc_user ctxtiaddr instrctxt + TR.tfold + ~ok:(fun iloc -> + let instrctxt = (make_i_location iloc instr#get_address)#ci in + finfo#connect_cc_user ctxtiaddr instrctxt) + ~error:(fun e -> + log_error_result + ~tag:"associate_condition_code_users" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr) else chlog#add "no flag setter" @@ -1471,14 +1531,38 @@ let associate_function_arguments_push () = let first = ref true in let compensateForPop = ref 0 in let valid = ref true in - let callloc = ctxt_string_to_location faddr callAddress in + let callloc = + match ctxt_string_to_location faddr callAddress with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"associate_function_arguments_push" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in block#itera ~high:callloc#i ~reverse:true (fun ctxtiaddr instr -> if !first then first := false (* skip the call itself *) else - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + match ctxt_string_to_location faddr ctxtiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"associate_function_arguments_push" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in if !valid && !active && !argNr < numParams then match instr#get_opcode with | Pop _ -> compensateForPop := !compensateForPop + 1 @@ -1519,7 +1603,19 @@ let associate_function_arguments_push () = let compensateForPop = ref false in let valid = ref true in let faddr = block#get_faddr in - let callloc = ctxt_string_to_location faddr callAddress in + let callloc = + match ctxt_string_to_location faddr callAddress with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"identify_arguments" + ~msg:callAddress + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in block#itera ~high:callloc#i ~reverse:true (fun _ctxtiaddr instr -> @@ -1555,7 +1651,19 @@ let associate_function_arguments_push () = (fun block -> block#itera (fun ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + match ctxt_string_to_location faddr ctxtiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"identify_arguments" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in let iaddr = loc#i in let floc = get_floc loc in match instr#get_opcode with @@ -1605,7 +1713,19 @@ let associate_function_arguments_mov () = let argumentsFound = ref [] in let maxIndex = ref 0 in let faddr = block#get_faddr in - let callloc = ctxt_string_to_location faddr callAddress in + let callloc = + match ctxt_string_to_location faddr callAddress with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"associate_function_arguments_mov" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in begin block#itera ~high:callloc#i ~reverse:true (fun _va instr -> @@ -1654,7 +1774,19 @@ let associate_function_arguments_mov () = let first = ref true in let argumentsFound = ref [] in let faddr = block#get_faddr in - let callloc = ctxt_string_to_location faddr callAddress in + let callloc = + match ctxt_string_to_location faddr callAddress with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"identify_arguments" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in begin block#itera ~high:callloc#i ~reverse:true (fun _va instr -> @@ -1697,7 +1829,19 @@ let associate_function_arguments_mov () = (fun block -> block#itera (fun ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = + match ctxt_string_to_location faddr ctxtiaddr with + | Ok loc -> loc + | Error e -> + begin + log_error_result + ~tag:"sanitize_arguments" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR (elocm __LINE__); STR (String.concat "; " e)])) + end in let floc = get_floc loc in match instr#get_opcode with | DirectCall op when @@ -1920,23 +2064,30 @@ let resolve_indirect_calls (f:assembly_function_int) = let _ = f#iteri (fun faddr ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in - match instr#get_opcode with - | IndirectCall op -> - let floc = get_floc loc in - if (not floc#has_call_target) - || floc#get_call_target#is_unknown then - let _ = - chlog#add - "attempt to resolve call" - (LBLOCK [ - floc#l#toPretty; - (if floc#get_call_target#is_unknown then - STR " (call target unknown)" - else - STR " (no call target)")]) in - set_call_address floc op - | _ -> ()) in + TR.tfold + ~ok:(fun loc -> + match instr#get_opcode with + | IndirectCall op -> + let floc = get_floc loc in + if (not floc#has_call_target) + || floc#get_call_target#is_unknown then + let _ = + chlog#add + "attempt to resolve call" + (LBLOCK [ + floc#l#toPretty; + (if floc#get_call_target#is_unknown then + STR " (call target unknown)" + else + STR " (no call target)")]) in + set_call_address floc op + | _ -> ()) + ~error:(fun e -> + log_error_result + ~tag:"resolve_indirect_calls" + ~msg:faddr#to_hex_string + __FILE__ __LINE__ e) + (ctxt_string_to_location faddr ctxtiaddr)) in () diff --git a/CodeHawk/CHB/bchlibx86/bCHDisassembleELF.ml b/CodeHawk/CHB/bchlibx86/bCHDisassembleELF.ml index e9a003e14..1fca4ab73 100644 --- a/CodeHawk/CHB/bchlibx86/bCHDisassembleELF.ml +++ b/CodeHawk/CHB/bchlibx86/bCHDisassembleELF.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -314,7 +314,7 @@ let resolve_pic_target floc instr = let resolve_pic_targets faddr f = f#iteri (fun _ ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in resolve_pic_target floc instr) @@ -700,7 +700,8 @@ let trace_block (faddr:doubleword_int) (baddr:doubleword_int) = | [] -> [(make_location {loc_faddr = faddr; loc_iaddr = returnsite})#ci] | l -> - List.map (fun s -> add_ctxt_to_ctxt_string faddr s ctxt) l in + List.map (fun s -> + TR.tget_ok (add_ctxt_to_ctxt_string faddr s ctxt)) l in make_ctxt_assembly_block ctxt b succ) fn#get_blocks in (Some [callsucc], va, inlinedblocks) else if !assembly_instructions#has_next_valid_instruction va then @@ -726,7 +727,7 @@ let trace_function (faddr:doubleword_int) = let workSet = new DoublewordCollections.set_t in let doneSet = new DoublewordCollections.set_t in let set_block_entry a = (!assembly_instructions#at_address a)#set_block_entry in - let get_iaddr s = (ctxt_string_to_location faddr s)#i in + let get_iaddr s = (TR.tget_ok (ctxt_string_to_location faddr s))#i in let add_to_workset l = List.iter (fun a -> if doneSet#has a then () else workSet#add a) l in let blocks = ref [] in @@ -802,7 +803,7 @@ let record_call_targets () = begin f#iteri (fun _ ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in match instr#get_opcode with (* | DirectCall op when @@ -859,7 +860,7 @@ let associate_condition_code_users () = let rec set l = match l with | [] -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in disassembly_log#add "cc user without setter" (LBLOCK [ @@ -871,7 +872,7 @@ let associate_condition_code_users () = | [] -> set tl | flags_set -> if List.for_all (fun fUsed -> List.mem fUsed flags_set) flags_used then - let iloc = ctxt_string_to_location faddr ctxtiaddr in + let iloc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let instrctxt = (make_i_location iloc instr#get_address)#ci in finfo#connect_cc_user ctxtiaddr instrctxt in set revInstrs in @@ -902,14 +903,14 @@ let associate_function_arguments_push () = let first = ref true in let compensateForPop = ref 0 in let valid = ref true in - let callloc = ctxt_string_to_location faddr callAddress in + let callloc = TR.tget_ok (ctxt_string_to_location faddr callAddress) in block#itera ~high:callloc#i ~reverse:true (fun ctxtiaddr instr -> if !first then first := false (* skip the call itself *) else - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in if !valid && !active && !argNr < numParams then match instr#get_opcode with | Pop _ -> compensateForPop := !compensateForPop + 1 @@ -949,7 +950,7 @@ let associate_function_arguments_push () = let compensateForPop = ref false in let valid = ref true in let faddr = block#get_faddr in - let callloc = ctxt_string_to_location faddr callAddress in + let callloc = TR.tget_ok (ctxt_string_to_location faddr callAddress) in block#itera ~high:callloc#i ~reverse:true @@ -986,7 +987,7 @@ let associate_function_arguments_push () = (fun block -> block#itera (fun ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in match instr#get_opcode with | DirectCall op when @@ -1028,7 +1029,7 @@ let associate_function_arguments_mov () = let argumentsFound = ref [] in let maxIndex = ref 0 in let faddr = block#get_faddr in - let callloc = ctxt_string_to_location faddr callAddress in + let callloc = TR.tget_ok (ctxt_string_to_location faddr callAddress) in begin block#itera ~high:callloc#i ~reverse:true (fun _va instr -> @@ -1076,7 +1077,7 @@ let associate_function_arguments_mov () = let first = ref true in let argumentsFound = ref [] in let faddr = block#get_faddr in - let callloc = ctxt_string_to_location faddr callAddress in + let callloc = TR.tget_ok (ctxt_string_to_location faddr callAddress) in begin block#itera ~high:callloc#i ~reverse:true (fun _va instr -> @@ -1120,7 +1121,7 @@ let associate_function_arguments_mov () = (fun block -> block#itera (fun ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in match instr#get_opcode with | DirectCall op when diff --git a/CodeHawk/CHB/bchlibx86/bCHFnX86Dictionary.ml b/CodeHawk/CHB/bchlibx86/bCHFnX86Dictionary.ml index f4146e8a6..0901ff0b6 100644 --- a/CodeHawk/CHB/bchlibx86/bCHFnX86Dictionary.ml +++ b/CodeHawk/CHB/bchlibx86/bCHFnX86Dictionary.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2021 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -60,6 +60,8 @@ open BCHOperand module B = Big_int_Z module H = Hashtbl +module TR = CHTraceResult + let x2p = xpr_formatter#pr_expr @@ -108,7 +110,7 @@ object (self) let rewrite_expr (x: xpr_t):xpr_t = floc#inv#rewrite_expr x in let rewrite_test_expr (csetter: ctxt_iaddress_t) (x: xpr_t): xpr_t = - let testloc = ctxt_string_to_location floc#fa csetter in + let testloc = TR.tget_ok (ctxt_string_to_location floc#fa csetter) in let testfloc = get_floc testloc in let xpr = testfloc#inv#rewrite_expr x in simplify_xpr xpr in @@ -534,7 +536,7 @@ object (self) (* ----------------------------------------------------------- Setcc -- *) | Setcc (_, op) when floc#f#has_associated_cc_setter floc#cia -> let testiaddr = floc#f#get_associated_cc_setter floc#cia in - let testloc = ctxt_string_to_location faddr testiaddr in + let testloc = TR.tget_ok (ctxt_string_to_location faddr testiaddr) in let testopc = ((!assembly_instructions)#at_address testloc#i)#get_opcode in let setopc = instr#get_opcode in diff --git a/CodeHawk/CHB/bchlibx86/bCHPullData.ml b/CodeHawk/CHB/bchlibx86/bCHPullData.ml index 716dbe25b..6494f8800 100644 --- a/CodeHawk/CHB/bchlibx86/bCHPullData.ml +++ b/CodeHawk/CHB/bchlibx86/bCHPullData.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-2026 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 @@ -76,7 +76,8 @@ let get_module_string (floc:floc_int) (xpr:xpr_t) = log_tfold (log_error "get_module_string" "invalid call site") ~ok:(fun callsite -> - let cFloc = get_floc (ctxt_string_to_location floc#fa callsite) in + let cFloc = + get_floc (TR.tget_ok (ctxt_string_to_location floc#fa callsite)) in match cFloc#get_call_args with | [(_, vxpr)] | [(_, vxpr); _; _] -> get_string_reference floc vxpr @@ -176,7 +177,8 @@ and get_decodepointer_target (floc:floc_int) = log_tfold (log_error "get_decodepointer_target" "invalid call site") ~ok:(fun callsite -> - let rfloc = get_floc (ctxt_string_to_location floc#fa callsite) in + let rfloc = + get_floc (TR.tget_ok (ctxt_string_to_location floc#fa callsite)) in get_rv_call_targets floc rfloc []) ~error:(fun _ -> []) (floc#env#get_call_site v) @@ -194,7 +196,8 @@ and get_encodepointer_target (floc:floc_int): call_target_t list = log_tfold (log_error "get_encodepointer_target" "invalid call site") ~ok:(fun callsite -> - let rfloc = get_floc (ctxt_string_to_location floc#fa callsite) in + let rfloc = + get_floc (TR.tget_ok (ctxt_string_to_location floc#fa callsite)) in get_rv_call_targets floc rfloc []) ~error:(fun _ -> []) (floc#env#get_call_site v) @@ -269,7 +272,8 @@ and extract_call_target log_tfold (log_error "extract_call_target" "invalid call target") ~ok:(fun callsite -> - let rfloc = get_floc (ctxt_string_to_location cfloc#fa callsite) in + let rfloc = + get_floc (TR.tget_ok (ctxt_string_to_location cfloc#fa callsite)) in get_rv_call_targets cfloc rfloc offsets) ~error:(fun _ -> []) (env#get_call_site v) diff --git a/CodeHawk/CHB/bchlibx86/bCHTranslateToCHIF.ml b/CodeHawk/CHB/bchlibx86/bCHTranslateToCHIF.ml index a6e98e1b3..7431e2dd8 100644 --- a/CodeHawk/CHB/bchlibx86/bCHTranslateToCHIF.ml +++ b/CodeHawk/CHB/bchlibx86/bCHTranslateToCHIF.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020-2021 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labss LLC + Copyright (c) 2021-2026 Aarno Labss 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 @@ -124,7 +124,7 @@ let is_invariant_opname (name:symbol_t) = name#getBaseName = "invariant" let is_eh_prolog (finfo:function_info_int) (iaddr:ctxt_iaddress_t) = - let loc = ctxt_string_to_location finfo#a iaddr in + let loc = TR.tget_ok (ctxt_string_to_location finfo#a iaddr) in let floc = get_floc loc in floc#has_call_target && floc#get_call_target#get_name = "_EH_prolog" @@ -436,7 +436,7 @@ let translate_instruction let _ = count_instruction () in let (ctxtiaddr,instruction) = code_pc#get_next_instruction in let faddr = function_location#f in - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let finfo = get_function_info faddr in let inv = finfo#iinv ctxtiaddr in let env = finfo#env in @@ -465,8 +465,9 @@ let translate_instruction let transaction = package_transaction finfo block_label cmds in if finfo#has_associated_cc_setter ctxtiaddr then let testIAddress = finfo#get_associated_cc_setter ctxtiaddr in - let testloc = ctxt_string_to_location faddr testIAddress in - let testAddress = (ctxt_string_to_location faddr testIAddress)#i in + let testloc = TR.tget_ok (ctxt_string_to_location faddr testIAddress) in + let testAddress = + (TR.tget_ok (ctxt_string_to_location faddr testIAddress))#i in let (nodes,edges) = make_condition ~jump_instruction:instruction diff --git a/CodeHawk/CHB/bchlibx86/bCHX86AnalysisResults.ml b/CodeHawk/CHB/bchlibx86/bCHX86AnalysisResults.ml index 688dfc735..652aacb6f 100644 --- a/CodeHawk/CHB/bchlibx86/bCHX86AnalysisResults.ml +++ b/CodeHawk/CHB/bchlibx86/bCHX86AnalysisResults.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -46,6 +46,7 @@ open BCHX86Dictionary open BCHX86OpcodeRecords module H = Hashtbl +module TR = CHTraceResult class fn_analysis_results_t (fn:assembly_function_int) = @@ -63,7 +64,7 @@ object (self) (node:xml_element_int) (ctxtiaddr:ctxt_iaddress_t) (instr:assembly_instruction_int) = - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in let espoffset = floc#get_stackpointer_offset "x86" in begin diff --git a/CodeHawk/CHB/bchlibx86/bCHX86Metrics.ml b/CodeHawk/CHB/bchlibx86/bCHX86Metrics.ml index 7a8eea12d..8ba693582 100644 --- a/CodeHawk/CHB/bchlibx86/bCHX86Metrics.ml +++ b/CodeHawk/CHB/bchlibx86/bCHX86Metrics.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2023 Henny B. Sipma - Copyright (c) 2024 Aarno Labs LLC + Copyright (c) 2024-2026 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 @@ -37,6 +37,8 @@ open BCHLibx86Types open BCHLoopStructure open BCHX86OpcodeRecords +module TR = CHTraceResult + let get_op_metrics (f:assembly_function_int) (finfo:function_info_int) = let faddr = f#get_address in @@ -67,7 +69,7 @@ let get_op_metrics (f:assembly_function_int) (finfo:function_info_int) = match ops with | [] -> () | _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in List.iter (fun (op:operand_int) -> match op#get_mode with @@ -85,7 +87,7 @@ let get_esp_metrics (f:assembly_function_int) (_finfo:function_info_int) = let _ = f#iteri (fun _ ctxtiaddr _ -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in let (_,range) = floc#get_stackpointer_offset "x86" in if range#isTop then From 8b5fea49ffc016c0b20b47eb27bdb6e037964483 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 9 Sep 2026 13:10:41 -0700 Subject: [PATCH 21/22] CHT: updates for error handling of location context --- .../bchlib_tests/txbchlib/bCHLocationTest.ml | 21 ++++++++++--------- .../tbchlibarm32/tCHBchlibarm32Utils.ml | 4 ++-- 2 files changed, 13 insertions(+), 12 deletions(-) diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHLocationTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHLocationTest.ml index 54f427430..a5dfdd798 100644 --- a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHLocationTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHLocationTest.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-2026 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 @@ -123,14 +123,14 @@ let loc_basic () = ~title:"ctxt-string-to-loc" (fun () -> let s = cloc#ci in - let loc = L.ctxt_string_to_location (make_dw faddr2) s in + let loc = TR.tget_ok (L.ctxt_string_to_location (make_dw faddr2) s) in A.equal_string loc#ci s); TS.add_simple_test ~title:"ctxt-string-to-loc-eq" (fun () -> let s = cloc#ci in - let loc = L.ctxt_string_to_location (make_dw faddr2) s in + let loc = TR.tget_ok (L.ctxt_string_to_location (make_dw faddr2) s) in BA.equal_location cloc loc); TS.add_simple_test @@ -138,13 +138,14 @@ let loc_basic () = (fun () -> let s = cloc#ci in let s2 = - L.add_ctxt_to_ctxt_string - (make_dw faddr2) - s - (FunctionContext - {ctxt_faddr = make_dw faddr3; - ctxt_callsite = make_dw iaddr31; - ctxt_returnsite = make_dw iaddr32}) in + TR.tget_ok ( + L.add_ctxt_to_ctxt_string + (make_dw faddr2) + s + (FunctionContext + {ctxt_faddr = make_dw faddr3; + ctxt_callsite = make_dw iaddr31; + ctxt_returnsite = make_dw iaddr32})) in A.equal_string s2 (fc [iaddr31; iaddr21; iaddr11])); TS.launch_tests () diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/tbchlibarm32/tCHBchlibarm32Utils.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/tbchlibarm32/tCHBchlibarm32Utils.ml index 5bddf5d4d..6b590b42b 100644 --- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/tbchlibarm32/tCHBchlibarm32Utils.ml +++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/tbchlibarm32/tCHBchlibarm32Utils.ml @@ -148,7 +148,7 @@ let get_instrxdata_xprs (fun _baddr block -> block#itera (fun ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in ignore (id#index_instr instr floc))) in let (_, xprs) = @@ -166,7 +166,7 @@ let get_instrxdata_tags (faddr: doubleword_int) (iaddr: doubleword_int) = (fun _baddr block -> block#itera (fun ctxtiaddr instr -> - let loc = ctxt_string_to_location faddr ctxtiaddr in + let loc = TR.tget_ok (ctxt_string_to_location faddr ctxtiaddr) in let floc = get_floc loc in ignore (id#index_instr instr floc))) in TR.tget_ok (testsupport#retrieve_instrx_tags iaddr#to_hex_string) From 3358a586c6613be406aac46af18071811a8ecad9 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 9 Sep 2026 13:12:50 -0700 Subject: [PATCH 22/22] CHB:disable reading back fragment membership --- CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 2 ++ CodeHawk/CHB/bchlib/bCHVersion.ml | 4 ++-- CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 2 +- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 0984ebad8..3f5f59c64 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -2722,8 +2722,10 @@ object (self) self#read_xml_test_variables (getc "test-variables")); (if hasc "test-expressions" then self#read_xml_test_expressions (getc "test-expressions")); + (* (if hasc "fragment-memberships" then self#read_xml_fragment_memberships (getc "fragment-memberships")); + *) (if hasc "format-strings" then self#read_xml_format_strings (getc "format-strings")); (if hasc "base-pointers" then diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index a6cb593a9..939115dc5 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_20260908" - ~date:"2026-0908" + ~version:"0.6.0_20260909" + ~date:"2026-0909" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index c57e0bd86..62f830006 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -4828,7 +4828,7 @@ object (self) let cfg = codegraph#to_cfg entryLabel exitLabel in let body = LF.mkCode [CFG (procname, cfg)] in let proc = LF.mkProcedure procname ~signature:[] ~bindings:[] ~scope ~body in - let _ = pr_debug [proc#toPretty; NL] in + (* let _ = pr_debug [proc#toPretty; NL] in *) arm_chif_system#add_arm_procedure proc end