Skip to content

Propagation #230

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sipma merged 5 commits into from
Mar 12, 2026
Merged

Propagation #230

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
189c352
CHB:extend proof obligations to ARM
sipma Mar 10, 2026
702c6f5
CHT: add unit test for smallest-wrapped-constant
sipma Mar 10, 2026
49fde10
CHB: fix stackpointer wrap-around issue
sipma Mar 11, 2026
c6d8497
CHB: avoid 1-byte buffer sizes
sipma Mar 11, 2026
883af86
CHB: fix Makefile dependency
sipma Mar 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions CodeHawk/CHB/bchlib/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,13 +100,13 @@ MLIS := \
bCHSystemInfo \
bCHXPODictionary \
bCHCallTargetInfo \
bCHXPOPredicate \
bCHProofObligations \
bCHFunctionStackframe \
bCHFunctionInfo \
bCHMakeCallTargetInfo \
bCHGlobalState \
bCHMemoryRecorder \
bCHXPOPredicate \
bCHCallSemanticsRecorder \
bCHFloc \
bCHCallgraph \
Expand Down Expand Up @@ -192,13 +192,13 @@ SOURCES := \
bCHSystemInfo \
bCHXPODictionary \
bCHCallTargetInfo \
bCHXPOPredicate \
bCHProofObligations \
bCHFunctionStackframe \
bCHFunctionInfo \
bCHMakeCallTargetInfo \
bCHGlobalState \
bCHMemoryRecorder \
bCHXPOPredicate \
bCHCallSemanticsRecorder \
bCHFloc \
bCHCallgraph \
Expand Down Expand Up @@ -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

Expand Down
59 changes: 50 additions & 9 deletions CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
| _ ->
Expand Down Expand Up @@ -262,23 +268,35 @@ 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
| _ -> ())
| _ -> ()

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) =
Expand All @@ -302,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
Expand Down Expand Up @@ -339,6 +370,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;
Expand Down
2 changes: 1 addition & 1 deletion CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
79 changes: 51 additions & 28 deletions CodeHawk/CHB/bchlib/bCHFloc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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__)
Expand Down Expand Up @@ -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 *)
Expand Down
8 changes: 5 additions & 3 deletions CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -549,7 +551,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
Expand Down
2 changes: 1 addition & 1 deletion CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 8 additions & 1 deletion CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion CodeHawk/CHB/bchlib/bCHPostcondition.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading