From 189c352d7a79b82fc6294c1ec3ed18cc50811d42 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 10 Mar 2026 15:38:51 -0700 Subject: [PATCH 1/5] CHB:extend proof obligations to ARM --- .../CHB/bchlib/bCHCallSemanticsRecorder.ml | 24 ++++++++++++- .../CHB/bchlib/bCHCallSemanticsRecorder.mli | 2 +- CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml | 4 +-- CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli | 2 +- CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml | 9 ++++- CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli | 2 +- CodeHawk/CHB/bchlib/bCHPostcondition.mli | 2 +- CodeHawk/CHB/bchlib/bCHProofObligations.ml | 36 ++++++++++++++++++- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +-- .../CHB/bchlibarm32/bCHARMAnalysisResults.ml | 8 +++-- .../CHB/bchlibarm32/bCHARMAnalysisResults.mli | 2 +- CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml | 4 +-- CodeHawk/CHB/bchlibarm32/bCHARMOperand.mli | 2 +- 13 files changed, 84 insertions(+), 17 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml index c4347122..bc244d75 100644 --- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.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 @@ -233,6 +233,12 @@ object (self) method record_precondition (pre: xxpredicate_t) = let xpo = xxp_to_xpo_predicate self#termev self#loc pre in let status = self#simplify_precondition xpo in + let _ = + log_diagnostics_result + ~tag:"record_precondition" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["pre: " ^ (p2s (xxpredicate_to_pretty pre))] in match status with | Discharged _ -> self#add_po xpo status | _ -> @@ -279,6 +285,12 @@ object (self) | _ -> () method private add_po (xpo: xpo_predicate_t) (status: po_status_t) = + let _ = + log_diagnostics_result + ~tag:"add_po" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + ["po: " ^ (p2s (xpo_predicate_to_pretty xpo))] in self#finfo#proofobligations#add_proofobligation self#loc#ci xpo status method private add_gpo (dw: doubleword_int) (xxp: xxpredicate_t) = @@ -339,6 +351,16 @@ object (self) (LBLOCK [self#loc#toPretty; STR ": "; (xpo_predicate_to_pretty xpo)]) method record_callsemantics = + let _ = + log_diagnostics_result + ~tag:"record_callsemantics" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + ["call target: " ^ (p2s self#calltargetinfo#toPretty); + "preconditions: " + ^ ((String.concat ", " + (List.map (fun p -> (p2s (xxpredicate_to_pretty p))) + self#calltargetinfo#get_preconditions)))] in begin List.iter self#record_precondition self#calltargetinfo#get_preconditions; List.iter self#record_sideeffect self#calltargetinfo#get_sideeffects; diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.mli b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.mli index 2885e219..43cdf9b5 100644 --- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.mli +++ b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.mli @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023 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 diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml index c58de637..cc947401 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.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 @@ -549,7 +549,7 @@ object (self) ~tag:"duplicate stack slot" ~msg:("Stack slot at offset " ^ (string_of_int offset) - ^ "already exists") + ^ " already exists") __FILE__ __LINE__ []; Ok (H.find stackslots offset) end diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli index e0cc6d16..04ae91d9 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml index c8104cd5..55ed5696 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.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 @@ -364,6 +364,13 @@ object (self) ~(var_r: variable_t traceresult) ~(size: int) ~(vtype: btype_t) = + let _ = + log_diagnostics_result + ~tag:"record_load_r" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + ["addr: " ^ (TR.tfold_default x2s "?" addr_r); + "var: " ^ (TR.tfold_default (fun v -> p2s v#toPretty) "?" var_r)] in TR.tfold ~ok:(fun var -> if self#env#is_stack_variable var then diff --git a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli index ef71b582..e658f1d6 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli +++ b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHPostcondition.mli b/CodeHawk/CHB/bchlib/bCHPostcondition.mli index 015aae90..bf67c3e4 100644 --- a/CodeHawk/CHB/bchlib/bCHPostcondition.mli +++ b/CodeHawk/CHB/bchlib/bCHPostcondition.mli @@ -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 diff --git a/CodeHawk/CHB/bchlib/bCHProofObligations.ml b/CodeHawk/CHB/bchlib/bCHProofObligations.ml index a7644878..2b8ecc48 100644 --- a/CodeHawk/CHB/bchlib/bCHProofObligations.ml +++ b/CodeHawk/CHB/bchlib/bCHProofObligations.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2022 Henny B. Sipma - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-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,19 +27,46 @@ SOFTWARE. ============================================================================= *) +(* chlib *) +open CHPretty + (* chutil *) +open CHLogger open CHXmlDocument (* bchlib *) +open BCHExternalPredicate open BCHLibTypes open BCHLocation +open BCHXPOPredicate module H = Hashtbl +let p2s = CHPrettyUtil.pretty_to_string + + let id = BCHInterfaceDictionary.interface_dictionary +let po_status_to_pretty (s: po_status_t): pretty_t = + match s with + | Discharged s -> LBLOCK [STR "discharged("; STR s; STR ")"] + | Delegated x -> LBLOCK [STR "delegated("; xxpredicate_to_pretty x; STR ")"] + | Requested (dw, x) -> + LBLOCK [ + STR "requested("; dw#toPretty; STR ", "; xxpredicate_to_pretty x; STR ")"] + | DelegatedGlobal (dw, x) -> + LBLOCK [ + STR "delegated_global("; + dw#toPretty; + STR ", "; + xxpredicate_to_pretty x; + STR ")"] + | Violated s -> LBLOCK [STR "violated("; STR s; STR ")"] + | Open -> STR "open" + + let write_xml_po_status (node: xml_element_int) (s: po_status_t) = match s with | Discharged s -> @@ -104,6 +131,13 @@ object (self) (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 diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index fef02570..ab01884e 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_20260225" - ~date:"2026-02-25" + ~version:"0.6.0_20260310" + ~date:"2026-03-10" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index e61e3541..705db6cf 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.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 @@ -213,6 +213,8 @@ object (self) let dNode = xmlElement "instr-dictionary" in let iiNode = xmlElement "instructions" in let sfNode = xmlElement "stackframe" in + let xpodNode = xmlElement "xpodictionary" in + let poNode = xmlElement "proofobligations" in let grNode = xmlElement "global-references" in (* let bNode = xmlElement "btypes" in *) begin @@ -223,7 +225,9 @@ object (self) mmap#write_xml_references faddr vard grNode; (* self#write_xml_btypes bNode; *) id#write_xml dNode; - append [cNode; dNode; iiNode; jjNode; sfNode; grNode] + finfo#proofobligations#write_xml poNode; + finfo#xpod#write_xml xpodNode; + append [cNode; dNode; iiNode; jjNode; sfNode; grNode; xpodNode; poNode] end method write_xml_register_types diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.mli b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.mli index ed2a9511..16088b73 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.mli @@ -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 diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml index 078a3491..d7e112ce 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.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 @@ -603,7 +603,7 @@ object (self:'a) ^ " not yet supported"]) in begin log_diagnostics_result - ~msg:(p2s self#toPretty) + ~msg:(p2s floc#l#toPretty) ~tag:"to_variable:scaledoffset" __FILE__ __LINE__ ["operand: " ^ (p2s self#toPretty); diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.mli b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.mli index 2b963cb6..6e4fd1fd 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.mli @@ -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 From 702c6f59dbbbc06e0d0d4552567b822c0228906f Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 10 Mar 2026 16:40:14 -0700 Subject: [PATCH 2/5] CHT: add unit test for smallest-wrapped-constant --- .../tbchlib/tCHBchlibAssertion.ml | 14 +++++++++ .../tbchlib/tCHBchlibAssertion.mli | 11 ++++++- .../bchlib_tests/txbchlib/bCHXprUtilTest.ml | 31 +++++++++++++++++-- 3 files changed, 53 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.ml index df51cc1d..b2ee3d43 100644 --- a/CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.ml +++ b/CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.ml @@ -84,6 +84,20 @@ let equal_numerical received +let equal_numerical_pair + ?(msg="") + ~(expected: numerical_t * numerical_t) + ~(received: numerical_t * numerical_t) + () = + A.make_equal + (fun (num11, num12) (num21, num22) -> + (num11#equal num21) && (num12#equal num22)) + (fun (num1, num2) -> "(" ^ num1#toString ^ ", " ^ num2#toString ^ ")") + ~msg + expected + received + + let equal_doubleword_result ?(msg="") (dw: doubleword_int) (dwr: doubleword_result) = if Result.is_error dwr then diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.mli b/CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.mli index bc6cafea..63061273 100644 --- a/CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.mli +++ b/CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.mli @@ -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 @@ -61,6 +61,15 @@ val equal_numerical: -> unit -> unit + +val equal_numerical_pair: + ?msg:string + -> expected:(numerical_t * numerical_t) + -> received:(numerical_t * numerical_t) + -> unit + -> unit + + val equal_doubleword_result: ?msg:string -> doubleword_int -> doubleword_result -> unit diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml index b8862c51..e57f4ab0 100644 --- a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml @@ -5,7 +5,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - 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 @@ -42,7 +42,7 @@ module TS = TCHTestSuite module X = BCHXprUtil let testname = "bCHXprUtilTest" -let lastupdated = "2024-12-25" +let lastupdated = "2026-03-10" let largest_constant_term_test () = @@ -109,6 +109,32 @@ let smallest_constant_term_test() = end +let smallest_wrapped_constant_term_test () = + begin + TS.new_testsuite (testname ^ "_smallest_wrapped_constant_term") lastupdated; + + TS.add_simple_test + ~title: "constant" + (fun () -> + XBA.equal_numerical_pair + ~expected:((mkNumerical 0x500000, mkNumerical 0x500000)) + ~received:(X.smallest_wrapped_constant_term + (Xprt.int_constant_expr 0x500000)) + ()); + + TS.add_simple_test + ~title: "wrap-around" + (fun () -> + XBA.equal_numerical_pair + ~expected:((mkNumerical 0xffffed64, mkNumerical (-(4764)))) + ~received:(X.smallest_wrapped_constant_term + (Xprt.int_constant_expr 0xffffed64)) + ()); + + TS.launch_tests () + end + + let array_index_offset_test () = let xv = XVar (XG.mk_var "v") in let xzero = Xprt.int_constant_expr 0 in @@ -259,6 +285,7 @@ let () = TS.new_testfile testname lastupdated; largest_constant_term_test (); smallest_constant_term_test (); + smallest_wrapped_constant_term_test (); array_index_offset_test (); TS.exit_file () end From 49fde10a000be318dacb554a3f0e814f14c90f41 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Tue, 10 Mar 2026 17:25:47 -0700 Subject: [PATCH 3/5] CHB: fix stackpointer wrap-around issue --- CodeHawk/CHB/bchlib/bCHFloc.ml | 79 +++++++++++++------- CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml | 4 +- 2 files changed, 54 insertions(+), 29 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 0d576a6a..835bf2ca 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -1341,6 +1341,40 @@ object (self) method get_fts_parameter_expr (_p: fts_parameter_t) = None + method private get_globalvar_at_gv_address + ?(size=None) + ?(btype=t_unknown) + (gvaddr: doubleword_int) + (xoff: xpr_t): variable_t traceresult = + let cxoff_r = self#xpr_to_cxpr xoff in (* should we have this call? *) + if memmap#has_location gvaddr then + let gloc = memmap#get_location gvaddr in + let var_r = + TR.tmap + ~msg:(eloc __LINE__) + (fun offset -> self#f#env#mk_gloc_variable gloc offset) + (TR.tbind + (fun xoff -> + gloc#address_offset_memory_offset + ~tgtsize:size ~tgtbtype:btype self#l xoff) + cxoff_r) in + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_var_at_address: addressofvar global" + __FILE__ __LINE__ + ["varresult: " + ^ (TR.tfold_default (fun v -> p2s v#toPretty) "error" var_r); + "gloc: " ^ gloc#name] in + var_r + + else + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Global location at address " + ^ gvaddr#to_hex_string + ^ " not found"] + method get_var_at_address ?(size=None) ?(btype=t_unknown) @@ -1372,44 +1406,20 @@ object (self) ^ " not found"]) gvaddr_r | XOp ((Xf "addressofvar"), [XVar v]) -> Ok v + | XOp (XPlus, [XOp ((Xf "addressofvar"), [XVar v]); xoff]) when self#f#env#is_global_variable v -> let gvaddr_r = self#f#env#get_global_variable_address v in - let cxoff_r = self#xpr_to_cxpr xoff in (* **should we have this call? *) TR.tbind ~msg:(eloc __LINE__) (fun gvaddr -> - if memmap#has_location gvaddr then - let gloc = memmap#get_location gvaddr in - let var_r = - TR.tmap - ~msg:(eloc __LINE__) - (fun offset -> self#f#env#mk_gloc_variable gloc offset) - (TR.tbind - (fun xoff -> - gloc#address_offset_memory_offset - ~tgtsize:size ~tgtbtype:btype self#l xoff) - cxoff_r) in - let _ = - log_diagnostics_result - ~msg:(p2s self#l#toPretty) - ~tag:"get_var_at_address: addressofvar global" - __FILE__ __LINE__ - ["varresult: " - ^ (TR.tfold_default (fun v -> p2s v#toPretty) "error" var_r); - "gloc: " ^ gloc#name] in - var_r - - else - Error [(elocm __LINE__); - (p2s self#l#toPretty); - "Global location at address " - ^ gvaddr#to_hex_string - ^ " not found"]) + self#get_globalvar_at_gv_address ~size ~btype gvaddr xoff) gvaddr_r + | _ -> match memmap#xpr_containing_location addrvalue with | Some gloc -> + (* within existing global location *) (TR.tmap ~msg:(eloc __LINE__) (fun offset -> self#f#env#mk_gloc_variable gloc offset) @@ -1418,6 +1428,7 @@ object (self) | _ -> match self#f#stackframe#xpr_containing_stackslot addrvalue with | Some stackslot -> + (* within existing stackslot *) let stackoffset_r = self#get_stackpointer_offset_xpr addrvalue in (TR.tmap ~msg:(eloc __LINE__) @@ -2445,12 +2456,24 @@ object (self) let memoff_r = match offset with | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset + | XConst (IntConst n) when n#gt (mkNumerical 0xffff0000) -> + let n = n#sub (mkNumerical 0x100000000) in + Ok (ConstantOffset (n, NoOffset)) | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | _ -> Error [(elocm __LINE__); (p2s self#l#toPretty); "base: " ^ (p2s base#toPretty); "offset expr: " ^ (x2s offset)] in + let _ = + log_diagnostics_result + ~tag:"decompose_memaddr:one-known-base" + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["x: " ^ (x2s x); + "base: " ^ (p2s base#toPretty); + "memoff: " + ^ (TR.tfold_default memory_offset_to_string "?" memoff_r)] in (memref_r, memoff_r) (* no known pointers, have to find a base *) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml index cc947401..8c18fc2e 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml @@ -157,7 +157,9 @@ object (self) simplify_xpr (XOp (XMinus, [xpr; int_constant_expr self#offset])) in let xoff = match xoff with - | XOp (XPlus, [_; XConst (IntConst n)]) when n#geq (mkNumerical 0x100000000) -> + | XConst (IntConst n) + | XOp (XPlus, [_; XConst (IntConst n)]) + when n#geq (mkNumerical 0x100000000) -> let rresult = simplify_xpr (XOp (XMinus, [xoff; int_constant_expr 0x100000000])) in begin From c6d84971d1c55127ad32c1ca40cb2c0f70f827c6 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 11 Mar 2026 12:27:39 -0700 Subject: [PATCH 4/5] CHB: avoid 1-byte buffer sizes --- .../CHB/bchlib/bCHCallSemanticsRecorder.ml | 35 ++++++++++++++----- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +-- 2 files changed, 29 insertions(+), 10 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml index bc244d75..cd4431c3 100644 --- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml @@ -268,17 +268,23 @@ object (self) | XPOBuffer (ty, addr, size) -> (match self#termev#xpr_local_stack_address addr with | Some offset -> - let _ = - ch_diagnostics_log#add - "record blockread" - (LBLOCK [loc#toPretty; STR ": "; - STR "offset: "; - INT offset]) in let csize = match size with | XConst (IntConst n) -> Some n#toInt | _ -> - TR.tfold_default (fun s -> Some s) None (size_of_btype ty) in + TR.tfold_default + (fun s -> if s >= 4 then Some s else None) + None + (size_of_btype ty) in + let _ = + log_diagnostics_result + ~tag:"record_blockreads" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpo: " ^ (p2s (xpo_predicate_to_pretty xpo)); + "offset: " ^ (string_of_int offset); + "size: " ^ + (match csize with Some s -> string_of_int s | _ -> "")] in self#finfo#stackframe#add_block_read ~offset:(-offset) ~size:csize ~typ:(Some ty) self#loc#ci | _ -> ()) @@ -314,10 +320,23 @@ object (self) match size with | XConst (IntConst n) -> Some n#toInt | _ -> - TR.tfold_default (fun s -> Some s) None (size_of_btype ty) in + TR.tfold_default + (fun s -> if s > 3 then Some s else None) + None + (size_of_btype ty) in let sevalue = self#finfo#env#mk_stack_sideeffect_value ~btype:(Some ty) self#loc#ci numoffset (bterm_to_string taddr) in + let _ = + log_diagnostics_result + ~tag:"record_sideeffect" + ~msg:(p2s loc#toPretty) + __FILE__ __LINE__ + ["xpo: " ^ (p2s (xpo_predicate_to_pretty xpo)); + "size: " + ^ (match csize with Some s -> string_of_int s | _ -> "?"); + "offset: " ^ (string_of_int offset); + "value: " ^ (p2s sevalue#toPretty)] in self#finfo#stackframe#add_block_write ~offset:(-offset) ~size:csize diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index ab01884e..e5a5b15e 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_20260310" - ~date:"2026-03-10" + ~version:"0.6.0_20260311" + ~date:"2026-03-11" ~licensee: None ~maxfilesize: None () From 883af86da14827087c3a1a6bb75fcc9582f44264 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Wed, 11 Mar 2026 12:43:04 -0700 Subject: [PATCH 5/5] CHB: fix Makefile dependency --- CodeHawk/CHB/bchlib/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CodeHawk/CHB/bchlib/Makefile b/CodeHawk/CHB/bchlib/Makefile index 4b38fc08..de0f24a8 100644 --- a/CodeHawk/CHB/bchlib/Makefile +++ b/CodeHawk/CHB/bchlib/Makefile @@ -100,13 +100,13 @@ MLIS := \ bCHSystemInfo \ bCHXPODictionary \ bCHCallTargetInfo \ + bCHXPOPredicate \ bCHProofObligations \ bCHFunctionStackframe \ bCHFunctionInfo \ bCHMakeCallTargetInfo \ bCHGlobalState \ bCHMemoryRecorder \ - bCHXPOPredicate \ bCHCallSemanticsRecorder \ bCHFloc \ bCHCallgraph \ @@ -192,13 +192,13 @@ SOURCES := \ bCHSystemInfo \ bCHXPODictionary \ bCHCallTargetInfo \ + bCHXPOPredicate \ bCHProofObligations \ bCHFunctionStackframe \ bCHFunctionInfo \ bCHMakeCallTargetInfo \ bCHGlobalState \ bCHMemoryRecorder \ - bCHXPOPredicate \ bCHCallSemanticsRecorder \ bCHFloc \ bCHCallgraph \ @@ -232,7 +232,7 @@ clean: rm -f *.cmxa rm -f *.ml~ rm -f *.mli~ - rm -f Makefile~ + rm -f Makefile~ rm -f bchlib.cmxa rm -rf doc