Skip to content

Commit ab826a0

Browse files
sipmasipma
committed
CHC: add outputparameter proof obligations insertion and checking
1 parent f6cb7b6 commit ab826a0

9 files changed

+336
-5
lines changed

‎CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.ml‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2025 Aarno Labs LLC
8+
9+
Permission is hereby granted, free of charge, to any person obtaining a copy
10+
of this software and associated documentation files (the "Software"), to deal
11+
in the Software without restriction, including without limitation the rights
12+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13+
copies of the Software, and to permit persons to whom the Software is
14+
furnished to do so, subject to the following conditions:
15+
16+
The above copyright notice and this permission notice shall be included in all
17+
copies or substantial portions of the Software.
18+
19+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
25+
SOFTWARE.
26+
============================================================================= *)
27+
28+
(* cchlib *)
29+
open CCHBasicTypes
30+
31+
(* cchpre *)
32+
open CCHPreTypes
33+
34+
(* cchanalyze *)
35+
open CCHAnalysisTypes
36+
37+
38+
let x2p = XprToPretty.xpr_formatter#pr_expr
39+
let p2s = CHPrettyUtil.pretty_to_string
40+
let _x2s x = p2s (x2p x)
41+
let _e2s e = p2s (CCHTypesToPretty.exp_to_pretty e)
42+
43+
44+
let _fenv = CCHFileEnvironment.file_environment
45+
46+
47+
class locally_initialized_checker_t
48+
(_poq: po_query_int)
49+
(vinfo: varinfo)
50+
(_lval: lval)
51+
(_invs: invariant_int list) =
52+
object
53+
54+
method private vinfo = vinfo
55+
56+
method check_safe = false
57+
58+
method check_violation = false
59+
60+
end
61+
62+
63+
let check_locally_initialized (poq:po_query_int) (vinfo: varinfo) (lval:lval) =
64+
let invs = poq#get_invariants 1 in
65+
let _ = poq#set_diagnostic_invariants 1 in
66+
let checker = new locally_initialized_checker_t poq vinfo lval invs in
67+
checker#check_safe || checker#check_violation

‎CodeHawk/CHC/cchanalyze/cCHPOCheckLocallyInitialized.mli‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2025 Aarno Labs LLC
8+
9+
Permission is hereby granted, free of charge, to any person obtaining a copy
10+
of this software and associated documentation files (the "Software"), to deal
11+
in the Software without restriction, including without limitation the rights
12+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13+
copies of the Software, and to permit persons to whom the Software is
14+
furnished to do so, subject to the following conditions:
15+
16+
The above copyright notice and this permission notice shall be included in all
17+
copies or substantial portions of the Software.
18+
19+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
25+
SOFTWARE.
26+
============================================================================= *)
27+
28+
(* cchlib *)
29+
open CCHBasicTypes
30+
31+
(* cchanalyze *)
32+
open CCHAnalysisTypes
33+
34+
35+
(** [check_locally_initialized poq lval] returns true if the invariants supplied by
36+
[poq] imply the initialization of [lval] within the function.
37+
38+
An lval is guaranteed to be locally initialized if
39+
- if it has been assigned within the function, or
40+
- if the expression is the dereferencing of the address of a variable, and the
41+
variable is initialized, or
42+
- if the lval contains an embedded null dereference; null dereference is
43+
checked for separately, or
44+
- if the lval can be shown to be distinct from the memory region pointed to
45+
by the vinfo (the targeted output parameter)
46+
*)
47+
val check_locally_initialized: po_query_int -> varinfo -> lval -> bool

‎CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterInitialized.ml‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2025 Aarno Labs LLC
8+
9+
Permission is hereby granted, free of charge, to any person obtaining a copy
10+
of this software and associated documentation files (the "Software"), to deal
11+
in the Software without restriction, including without limitation the rights
12+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13+
copies of the Software, and to permit persons to whom the Software is
14+
furnished to do so, subject to the following conditions:
15+
16+
The above copyright notice and this permission notice shall be included in all
17+
copies or substantial portions of the Software.
18+
19+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
25+
SOFTWARE.
26+
============================================================================= *)
27+
28+
(* cchlib *)
29+
open CCHBasicTypes
30+
31+
(* cchpre *)
32+
open CCHPreTypes
33+
34+
(* cchanalyze *)
35+
open CCHAnalysisTypes
36+
37+
38+
let x2p = XprToPretty.xpr_formatter#pr_expr
39+
let p2s = CHPrettyUtil.pretty_to_string
40+
let _x2s x = p2s (x2p x)
41+
let _e2s e = p2s (CCHTypesToPretty.exp_to_pretty e)
42+
43+
44+
let _fenv = CCHFileEnvironment.file_environment
45+
46+
47+
class outputparameter_initialized_checker_t
48+
(_poq: po_query_int)
49+
(vinfo: varinfo)
50+
(_invs: invariant_int list) =
51+
object
52+
53+
method private vinfo = vinfo
54+
55+
method check_safe = false
56+
57+
method check_violation = false
58+
59+
end
60+
61+
62+
let check_outputparameter_initialized (poq:po_query_int) (vinfo: varinfo) =
63+
let invs = poq#get_invariants 1 in
64+
let _ = poq#set_diagnostic_invariants 1 in
65+
let checker = new outputparameter_initialized_checker_t poq vinfo invs in
66+
checker#check_safe || checker#check_violation

‎CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterInitialized.mli‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2025 Aarno Labs LLC
8+
9+
Permission is hereby granted, free of charge, to any person obtaining a copy
10+
of this software and associated documentation files (the "Software"), to deal
11+
in the Software without restriction, including without limitation the rights
12+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13+
copies of the Software, and to permit persons to whom the Software is
14+
furnished to do so, subject to the following conditions:
15+
16+
The above copyright notice and this permission notice shall be included in all
17+
copies or substantial portions of the Software.
18+
19+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
25+
SOFTWARE.
26+
============================================================================= *)
27+
28+
(* cchlib *)
29+
open CCHBasicTypes
30+
31+
(* cchanalyze *)
32+
open CCHAnalysisTypes
33+
34+
35+
val check_outputparameter_initialized: po_query_int -> varinfo -> bool

‎CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterUnaltered.ml‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2025 Aarno Labs LLC
8+
9+
Permission is hereby granted, free of charge, to any person obtaining a copy
10+
of this software and associated documentation files (the "Software"), to deal
11+
in the Software without restriction, including without limitation the rights
12+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13+
copies of the Software, and to permit persons to whom the Software is
14+
furnished to do so, subject to the following conditions:
15+
16+
The above copyright notice and this permission notice shall be included in all
17+
copies or substantial portions of the Software.
18+
19+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
25+
SOFTWARE.
26+
============================================================================= *)
27+
28+
(* cchlib *)
29+
open CCHBasicTypes
30+
31+
(* cchpre *)
32+
open CCHPreTypes
33+
34+
(* cchanalyze *)
35+
open CCHAnalysisTypes
36+
37+
38+
let x2p = XprToPretty.xpr_formatter#pr_expr
39+
let p2s = CHPrettyUtil.pretty_to_string
40+
let _x2s x = p2s (x2p x)
41+
let _e2s e = p2s (CCHTypesToPretty.exp_to_pretty e)
42+
43+
44+
let _fenv = CCHFileEnvironment.file_environment
45+
46+
47+
class outputparameter_unaltered_checker_t
48+
(_poq: po_query_int)
49+
(vinfo: varinfo)
50+
(_invs: invariant_int list) =
51+
object
52+
53+
method private vinfo = vinfo
54+
55+
method check_safe = false
56+
57+
method check_violation = false
58+
59+
end
60+
61+
62+
let check_outputparameter_unaltered (poq:po_query_int) (vinfo: varinfo) =
63+
let invs = poq#get_invariants 1 in
64+
let _ = poq#set_diagnostic_invariants 1 in
65+
let checker = new outputparameter_unaltered_checker_t poq vinfo invs in
66+
checker#check_safe || checker#check_violation

‎CodeHawk/CHC/cchanalyze/cCHPOCheckOutputParameterUnaltered.mli‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
(* =============================================================================
2+
CodeHawk C Analyzer
3+
Author: Henny Sipma
4+
------------------------------------------------------------------------------
5+
The MIT License (MIT)
6+
7+
Copyright (c) 2025 Aarno Labs LLC
8+
9+
Permission is hereby granted, free of charge, to any person obtaining a copy
10+
of this software and associated documentation files (the "Software"), to deal
11+
in the Software without restriction, including without limitation the rights
12+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13+
copies of the Software, and to permit persons to whom the Software is
14+
furnished to do so, subject to the following conditions:
15+
16+
The above copyright notice and this permission notice shall be included in all
17+
copies or substantial portions of the Software.
18+
19+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
25+
SOFTWARE.
26+
============================================================================= *)
27+
28+
(* cchlib *)
29+
open CCHBasicTypes
30+
31+
(* cchanalyze *)
32+
open CCHAnalysisTypes
33+
34+
35+
val check_outputparameter_unaltered: po_query_int -> varinfo -> bool

‎CodeHawk/CHC/cchanalyze/cCHPOChecker.ml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ open CCHPOCheckStackAddressEscape
5959
open CCHPOCheckIndexLowerBound
6060
open CCHPOCheckIndexUpperBound
6161
open CCHPOCheckInitialized
62+
open CCHPOCheckLocallyInitialized
6263
open CCHPOCheckInitializedRange
6364
open CCHPOCheckIntOverflow
6465
open CCHPOCheckIntUnderflow
@@ -71,6 +72,8 @@ open CCHPOCheckNotZero
7172
open CCHPOCheckNonNegative
7273
open CCHPOCheckWidthOverflow
7374
open CCHPOCheckNullTerminated
75+
open CCHPOCheckOutputParameterInitialized
76+
open CCHPOCheckOutputParameterUnaltered
7477
open CCHPOCheckPointerCast
7578
open CCHPOCheckPreservedAllMemory
7679
open CCHPOCheckPtrLowerBound
@@ -148,6 +151,7 @@ object
148151
| PIndexLowerBound e -> check_index_lower_bound poq e
149152
| PIndexUpperBound (e1,e2) -> check_index_upper_bound poq e1 e2
150153
| PInitialized lval -> check_initialized poq lval
154+
| PLocallyInitialized (vinfo, lval) -> check_locally_initialized poq vinfo lval
151155
| PInitializedRange (e1,e2) -> check_initialized_range poq e1 e2
152156
| PIntOverflow (op,e1,e2,k) -> check_signed_int_overflow poq op e1 e2 k
153157
| PUIntOverflow (op,e1,e2,k) -> check_unsigned_int_overflow poq op e1 e2 k
@@ -182,6 +186,8 @@ object
182186
| PValueConstraint e -> check_value_constraint poq e
183187
| PValuePreserved e -> check_value_preserved poq e
184188
| PPreservedAllMemory -> check_preserved_all_memory poq
189+
| POutputParameterInitialized v -> check_outputparameter_initialized poq v
190+
| POutputParameterUnaltered v -> check_outputparameter_unaltered poq v
185191
| _ -> false
186192

187193
end

‎CodeHawk/CHC/cchcmdline/cCHVersion.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -62,5 +62,5 @@ object (self)
6262
end
6363

6464
let version = new version_info_t
65-
~version:"0.2.0"
66-
~date:"May 20, 2024"
65+
~version:"0.3.0"
66+
~date:"2025-10-28"

‎CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml‎

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -61,8 +61,8 @@ let _ = CHPretty.set_trace_level 0
6161
let cmds = [
6262
"version";
6363
"gc";
64-
"primary";
65-
"secondary";
64+
"undefined-behavior-primary";
65+
"outputparameters-primary";
6666
"localinvs";
6767
"globalinvs";
6868
"check";
@@ -176,7 +176,7 @@ let main () =
176176
exit 0
177177
end
178178

179-
else if !cmd = "primary" then
179+
else if !cmd = "undefined-behavior-primary" then
180180
begin
181181
primary_process_file ();
182182
log_info "primary proof obligations generated [%s:%d]" __FILE__ __LINE__;
@@ -185,6 +185,15 @@ let main () =
185185
"primary proof obligations log files saved [%s:%d]" __FILE__ __LINE__
186186
end
187187

188+
else if !cmd = "outputparameters-primary" then
189+
begin
190+
CCHCreateOutputParameterPOs.output_parameter_po_process_file ();
191+
log_info "primary proof obligations generated [%s:%d]" __FILE__ __LINE__;
192+
save_log_files "primary";
193+
log_info
194+
"primary proof obligations log files saved [%s:%d]" __FILE__ __LINE__
195+
end
196+
188197
else if !cmd = "localinvs" then
189198
begin
190199
invariants_process_file (List.rev !domains);

0 commit comments

Comments
 (0)