Skip to content

Commit c140bee

Browse files
sipmasipma
committed
CHT:CHC: add unit tests for PLocallyInitialized
1 parent 953c96f commit c140bee

20 files changed

+317
-24
lines changed

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/tcchanalyze/tCHCchanalyzeAssertion.ml‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,3 +53,30 @@ let expect_safe_detail
5353
A.fail_msg
5454
("Received proof obligation with status "
5555
^ (CCHPreSumTypeSerializer.po_status_mfts#ts s))
56+
57+
58+
let expect_violation_detail
59+
?(msg="")
60+
~(po: CCHPreTypes.proof_obligation_int)
61+
~(xdetail: string)
62+
~(expl: string)
63+
() =
64+
match po#get_status with
65+
| Red ->
66+
(match po#get_explanation with
67+
| Some x ->
68+
let dmatch = (expl = "") || (expl = x.smsg_msg) in
69+
if not dmatch then
70+
A.equal_string ~msg:"Explanation is different" expl x.smsg_msg
71+
else
72+
(match x.smsg_loc with
73+
| Some ocode ->
74+
A.equal_string ~msg xdetail ocode.ocode_detail
75+
| _ ->
76+
A.fail_msg "Received explanation without location detail")
77+
| _ ->
78+
A.fail_msg "Received proof obligation without explanation")
79+
| s ->
80+
A.fail_msg
81+
("Received proof obligation with status "
82+
^ (CCHPreSumTypeSerializer.po_status_mfts#ts s))

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/tcchanalyze/tCHCchanalyzeAssertion.mli‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,3 +34,12 @@ val expect_safe_detail:
3434
-> expl:string
3535
-> unit
3636
-> unit
37+
38+
39+
val expect_violation_detail:
40+
?msg:string
41+
-> po:CCHPreTypes.proof_obligation_int
42+
-> xdetail:string
43+
-> expl:string
44+
-> unit
45+
-> unit

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/tcchanalyze/tCHCchanalyzeUtils.ml‎

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,9 @@ let default_domains = [
4848
]
4949

5050

51-
let unpack_tar_gz (filename: string) =
52-
let targzname = Filename.concat "testinputs" (filename ^ ".cch.tar.gz") in
51+
let unpack_tar_gz (predicate: string) (filename: string) =
52+
let subdir = Filename.concat "testinputs" predicate in
53+
let targzname = Filename.concat subdir (filename ^ ".cch.tar.gz") in
5354
let cchdirname = filename ^ ".cch" in
5455
let rmcmd = Filename.quote_command "rm" ["-rf"; cchdirname] in
5556
let xtarcmd = Filename.quote_command "tar" ["xfz"; targzname] in
@@ -58,19 +59,30 @@ let unpack_tar_gz (filename: string) =
5859
()
5960

6061

61-
let analysis_setup ?(domains=default_domains) (filename: string) =
62+
let analysis_setup ?(domains=default_domains) (predicate: string) (filename: string) =
6263
begin
63-
unpack_tar_gz filename;
64+
unpack_tar_gz predicate filename;
6465
system_settings#set_projectname filename;
6566
system_settings#set_cfilename filename;
66-
CCHCreatePrimaryProofObligations.primary_process_file ();
67+
(if system_settings#is_output_parameter_analysis then
68+
CCHCreateOutputParameterPOs.output_parameter_po_process_file ()
69+
else
70+
CCHCreatePrimaryProofObligations.primary_process_file ());
6771
CCHProofScaffolding.proof_scaffolding#reset;
6872
CCHGenerateAndCheck.generate_and_check_process_file domains
6973
end
7074

7175

76+
let analysis_take_down (filename: string) =
77+
let cchdirname = filename ^ ".cch" in
78+
let rmcmd = Filename.quote_command "rm" ["-rf"; cchdirname] in
79+
let _ = Sys.command rmcmd in
80+
()
81+
82+
7283
let exp_to_string (exp: exp) = p2s (exp_to_pretty exp)
7384

85+
7486
let located_po_to_string (po: proof_obligation_int) =
7587
let loc = po#get_location in
7688
"("

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/tcchanalyze/tCHCchanalyzeUtils.mli‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,11 @@
2727
============================================================================= *)
2828

2929

30-
val analysis_setup: ?domains:string list -> string -> unit
30+
val analysis_setup: ?domains:string list -> string -> string -> unit
31+
32+
33+
val analysis_take_down: string -> unit
34+
3135

3236
val select_target_po:
3337
?reqargs:string list

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/Makefile‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ SOURCES := \
5858

5959
OBJECTS := $(addprefix cmx/,$(SOURCES:%=%.cmx))
6060

61-
all: make_dirs cCHPOCheckInitializedTest
61+
all: make_dirs cCHPOCheckInitializedTest cCHPOCheckLocallyInitializedTest
6262

6363
doc:
6464

@@ -69,8 +69,12 @@ make_dirs:
6969
cCHPOCheckInitializedTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa cmi/cCHPOCheckInitializedTest.cmi cmx/cCHPOCheckInitializedTest.cmx
7070
$(CAMLLINK) -o cCHPOCheckInitializedTest $(OBJECTS) cmx/cCHPOCheckInitializedTest.cmx
7171

72-
run: cCHPOCheckInitializedTest
72+
cCHPOCheckLocallyInitializedTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa cmi/cCHPOCheckLocallyInitializedTest.cmi cmx/cCHPOCheckLocallyInitializedTest.cmx
73+
$(CAMLLINK) -o cCHPOCheckLocallyInitializedTest $(OBJECTS) cmx/cCHPOCheckLocallyInitializedTest.cmx
74+
75+
run: cCHPOCheckInitializedTest cCHPOCheckLocallyInitializedTest
7376
./cCHPOCheckInitializedTest
77+
./cCHPOCheckLocallyInitializedTest
7478

7579
cmi/%.cmi: %.mli
7680
$(CAMLC) -o $@ -c -opaque $<
@@ -93,3 +97,4 @@ clean:
9397
rm -f *.mli~
9498
rm -f Makefile~
9599
rm -f cCHPOCheckInitializedTest
100+
rm -f cCHPOCheckLocallyInitializedTest

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckInitializedTest.ml‎

Lines changed: 48 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ module CA = TCHCchanalyzeAssertion
3535
module CU = TCHCchanalyzeUtils
3636

3737

38-
let testname = "bCHPOCheckInitializedTest"
38+
let testname = "cCHPOCheckInitializedTest"
3939
let lastupdated = "2025-11-10"
4040

4141

@@ -111,6 +111,18 @@ let po_filter (po: proof_obligation_int): proof_obligation_int option =
111111
return i;
112112
}
113113
114+
Test gl-inv-xpr-001:
115+
====================
116+
int gl_inv_xpr_001(void) {
117+
118+
int i = 5;
119+
120+
int *p = &i;
121+
122+
return *p;
123+
}
124+
125+
114126
*)
115127
let check_safe () =
116128
let tests = [
@@ -125,7 +137,28 @@ let check_safe () =
125137
("gl-inv-003",
126138
"gl_inv_003", "gl_inv_003",
127139
[], 14, -1,
128-
"inv_implies_safe", "")
140+
"inv_implies_safe", "");
141+
("gl-inv-xpr-001",
142+
"gl_inv_xpr_001", "gl_inv_xpr_001",
143+
["(*p)"], -1, -1,
144+
"inv_xpr_implies_safe", "variable (*p) has the value 5");
145+
("gl-inv-xpr-002",
146+
"gl_inv_xpr_002", "gl_inv_xpr_002",
147+
["(*p)"], -1, -1,
148+
"inv_xpr_implies_safe", "variable (*p) has the value 8");
149+
("gl-inv-xpr-003",
150+
"gl_inv_xpr_003", "gl_inv_xpr_003",
151+
[], 11, -1,
152+
"inv_xpr_implies_safe", "variable i has the value 8");
153+
("gl-inv-bounded-xpr-001",
154+
"gl_inv_bounded_xpr_001", "gl_inv_bounded_xpr_001",
155+
["(*p)"], 14, -1,
156+
"inv_bounded_xpr_implies_safe", "variable (*p) is bounded by LB: 3 and UB: 5");
157+
("gl-stackvar-001",
158+
"gl_stackvar_001", "gl_stackvar_001",
159+
["(*p)"], 14, -1,
160+
"memlval_vinv_memref_stackvar_implies_safe",
161+
"assignment(s) to i: assignedAt#11_xx_assignedAt#9")
129162
] in
130163
begin
131164
TS.new_testsuite (testname ^ "_check_safe") lastupdated;
@@ -136,19 +169,23 @@ let check_safe () =
136169
TS.add_simple_test
137170
~title
138171
(fun () ->
139-
let _ = CU.analysis_setup filename in
172+
let _ = CCHSettings.system_settings#set_undefined_behavior_analysis in
173+
let _ = CU.analysis_setup "PInitialized" filename in
140174
let po_s = proof_scaffolding#get_proof_obligations funname in
141175
let po_s = List.filter_map po_filter po_s in
142176
let (tgtpo_o, other_po_s) =
143177
CU.select_target_po ~reqargs ~line ~byte po_s in
144-
match tgtpo_o with
145-
| Some po -> CA.expect_safe_detail ~po ~xdetail ~expl ()
146-
| _ ->
147-
A.fail_msg
148-
("Unable to uniquely select target proof obligation: "
149-
^ "["
150-
^ (String.concat "; " other_po_s)
151-
^ "]")
178+
begin
179+
CU.analysis_take_down filename;
180+
match tgtpo_o with
181+
| Some po -> CA.expect_safe_detail ~po ~xdetail ~expl ()
182+
| _ ->
183+
A.fail_msg
184+
("Unable to uniquely select target proof obligation: "
185+
^ "["
186+
^ (String.concat "; " other_po_s)
187+
^ "]")
188+
end
152189
)
153190
) tests;
154191

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/txcchanalyze/cCHPOCheckLocallyInitializedTest.ml‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
1+
(* =============================================================================
2+
CodeHawk Unit Testing Framework
3+
Author: Henny Sipma
4+
Adapted from: Kaputt (https://kaputt.x9c.fr/index.html)
5+
------------------------------------------------------------------------------
6+
The MIT License (MIT)
7+
8+
Copyright (c) 2025 Aarno Labs LLC
9+
10+
Permission is hereby granted, free of charge, to any person obtaining a copy
11+
of this software and associated documentation files (the "Software"), to deal
12+
in the Software without restriction, including without limitation the rights
13+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
14+
copies of the Software, and to permit persons to whom the Software is
15+
furnished to do so, subject to the following conditions:
16+
17+
The above copyright notice and this permission notice shall be included in all
18+
copies or substantial portions of the Software.
19+
20+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
21+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
22+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
23+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
24+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
25+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
26+
SOFTWARE.
27+
============================================================================= *)
28+
29+
open CCHPreTypes
30+
open CCHProofScaffolding
31+
32+
module A = TCHAssertion
33+
module TS = TCHTestSuite
34+
module CA = TCHCchanalyzeAssertion
35+
module CU = TCHCchanalyzeUtils
36+
37+
38+
let testname = "cCHPOCheckLocallyInitializedTest"
39+
let lastupdated = "2025-11-12"
40+
41+
42+
let po_filter (po: proof_obligation_int): proof_obligation_int option =
43+
match po#get_predicate with
44+
| PLocallyInitialized _ -> Some po
45+
| _ -> None
46+
47+
48+
(* Test specifications contain the following information:
49+
title: name of the test
50+
51+
- file/function identification
52+
------------------------------
53+
filename: name of the c-file to be loaded
54+
funname: name of the function to be checked
55+
56+
- selection of proof obligation to check
57+
----------------------------------------
58+
reqargs: list of strings that represent the arguments to the
59+
proof obligation predicate; this may be an empty list or a list
60+
that has the right length, but individual arguments may be omitted
61+
by specifying the empty string ("")
62+
line: the line number to which the proof obligation applies (can be
63+
left unspecified by giving -1)
64+
byte: the byte number at which the proof obligation is located (can
65+
be left unspecified by giving -1)
66+
67+
- check that proof obligation is discharged as expected
68+
-------------------------------------------------------
69+
xdetail: identification of the discharge method in the checker
70+
expl: explanation given for the discharge (can be left unspecified
71+
by giving the empty string)
72+
*)
73+
let check_safe () =
74+
let tests = [
75+
("gl-inv-001",
76+
"locally_initialized_gl_inv_001", "gl_inv_001",
77+
[], -1, -1,
78+
"inv_implies_safe", "local assignment(s): assignedAt#4")
79+
] in
80+
begin
81+
TS.new_testsuite (testname ^ "_check_safe") lastupdated;
82+
CHTiming.disable_timing ();
83+
84+
List.iter
85+
(fun (title, filename, funname, reqargs, line, byte, xdetail, expl) ->
86+
TS.add_simple_test
87+
~title
88+
(fun () ->
89+
let _ = CCHSettings.system_settings#set_output_parameter_analysis in
90+
let _ = CU.analysis_setup "PLocallyInitialized" filename in
91+
let po_s = proof_scaffolding#get_proof_obligations funname in
92+
let po_s = List.filter_map po_filter po_s in
93+
let (tgtpo_o, other_po_s) =
94+
CU.select_target_po ~reqargs ~line ~byte po_s in
95+
begin
96+
CU.analysis_take_down filename;
97+
match tgtpo_o with
98+
| Some po -> CA.expect_safe_detail ~po ~xdetail ~expl ()
99+
| _ ->
100+
A.fail_msg
101+
("Unable to uniquely select target proof obligation: "
102+
^ "["
103+
^ (String.concat "; " other_po_s)
104+
^ "]")
105+
end
106+
)
107+
) tests;
108+
109+
TS.launch_tests()
110+
end
111+
112+
113+
let check_violation () =
114+
let tests = [
115+
("rl-xpr-001",
116+
"locally_initialized_rl_xpr_001", "rl_xpr_001",
117+
[], -1, -1,
118+
"xpr_implies_violation",
119+
"value of (*p) is obtained from dereferencing parameter p");
120+
("rl-xpr-002",
121+
"locally_initialized_rl_xpr_002", "rl_xpr_002",
122+
[], -1, -1,
123+
"xpr_implies_violation",
124+
"value of (*p) is obtained from dereferencing parameter p");
125+
] in
126+
begin
127+
TS.new_testsuite (testname ^ "_check_violation") lastupdated;
128+
CHTiming.disable_timing ();
129+
130+
List.iter
131+
(fun (title, filename, funname, reqargs, line, byte, xdetail, expl) ->
132+
TS.add_simple_test
133+
~title
134+
(fun () ->
135+
let _ = CCHSettings.system_settings#set_output_parameter_analysis in
136+
let _ = CU.analysis_setup "PLocallyInitialized" filename in
137+
let po_s = proof_scaffolding#get_proof_obligations funname in
138+
let po_s = List.filter_map po_filter po_s in
139+
let (tgtpo_o, other_po_s) =
140+
CU.select_target_po ~reqargs ~line ~byte po_s in
141+
begin
142+
CU.analysis_take_down filename;
143+
match tgtpo_o with
144+
| Some po -> CA.expect_violation_detail ~po ~xdetail ~expl ()
145+
| _ ->
146+
A.fail_msg
147+
("Unable to uniquely select target proof obligation: "
148+
^ "["
149+
^ (String.concat "; " other_po_s)
150+
^ "]")
151+
end
152+
)
153+
) tests;
154+
155+
TS.launch_tests()
156+
end
157+
158+
let () =
159+
begin
160+
TS.new_testfile testname lastupdated;
161+
check_safe ();
162+
check_violation ();
163+
TS.exit_file ()
164+
end

0 commit comments

Comments
 (0)