Skip to content

Commit dc96c4c

Browse files
sipmasipma
committed
CHT:CHC: add unit test infrastructure for PO checkers
1 parent 9b893c6 commit dc96c4c

File tree

15 files changed

+623
-0
lines changed

15 files changed

+623
-0
lines changed

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/tcchanalyze/Makefile‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
CODEHAWK = ../../../..
2+
CH = $(CODEHAWK)/CH
3+
CHT = $(CODEHAWK)/CHT
4+
5+
ZARITHLIB = $(shell ocamlfind query zarith)
6+
7+
CHLIB = $(CODEHAWK)/CH/chlib
8+
EXTLIB = $(shell ocamlfind query extlib)
9+
ZIPLIB = $(shell ocamlfind query zip)
10+
CHUTIL = $(CODEHAWK)/CH/chutil
11+
XPRLIB = $(CODEHAWK)/CH/xprlib
12+
CCHLIB = $(CODEHAWK)/CHC/cchlib
13+
CCHPRE = $(CODEHAWK)/CHC/cchpre
14+
CCHANALYZE = $(CODEHAWK)/CHC/cchanalyze
15+
TESTLIB = $(CHT)/tchlib
16+
17+
CAMLDOC := ocamldoc
18+
19+
CAMLC := ocamlopt -I str -I cmi -I cmx \
20+
-I $(EXTLIB) \
21+
-I $(ZIPLIB) \
22+
-I $(ZARITHLIB) \
23+
-I $(CHLIB)/cmi \
24+
-I $(CHUTIL)/cmi \
25+
-I $(XPRLIB)/cmi \
26+
-I $(CCHLIB)/cmi \
27+
-I $(CCHPRE)/cmi \
28+
-I $(CCHANALYZE)/cmi \
29+
-I $(TESTLIB)/cmi \
30+
31+
CAMLLINK := ocamlopt \
32+
33+
MLIS := \
34+
tCHCchanalyzeAssertion \
35+
tCHCchanalyzeUtils \
36+
37+
CMIS := $(addprefix cmi/,$(MLIS:%=%.cmi))
38+
39+
SOURCES := \
40+
tCHCchanalyzeAssertion \
41+
tCHCchanalyzeUtils \
42+
43+
OBJECTS := $(addprefix cmx/,$(SOURCES:%=%.cmx))
44+
45+
all: make_dirs tcchanalyze
46+
47+
doc:
48+
49+
make_dirs:
50+
@mkdir -p cmx
51+
@mkdir -p cmi
52+
53+
tcchanalyze: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(ZIPLIB)/zip.cmxa $(CHUTIL)/chutil.cmxa $(XPRLIB)/xpr.cmxa $(CCHLIB)/cchlib.cmxa $(CCHPRE)/cchpre.cmxa $(CCHANALYZE)/cchanalyze.cmxa $(TESTLIB)/tchlib.cmxa
54+
$(CAMLLINK) -a -o tcchanalyze.cmxa $(OBJECTS)
55+
56+
cmi/%.cmi: %.mli
57+
$(CAMLC) -o $@ -c -opaque $<
58+
59+
cmx/%.cmx: %.ml $(CMIS)
60+
$(CAMLC) -o $@ -c $<
61+
62+
doc: $(CMIS) $(OBJECTS)
63+
rm -rf doc
64+
mkdir doc
65+
$(CAMLDOC) -I cmi -I cmx -warn-error -d doc -html -I $(CHUTIL) $(MLIS:%=%.mli)
66+
67+
clean:
68+
rm -f cmx/*.cm*
69+
rm -f cmi/*.cmi
70+
rm -f cmx/*.o
71+
rm -f *.a
72+
rm -f *.cmxa
73+
rm -f *.ml~
74+
rm -f *.mli~
75+
rm -f Makefile~
76+
rm -rf doc

‎CodeHawk/CHT/CHC_tests/cchanalyze_tests/tcchanalyze/dune‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
(library
2+
(name tcchanalyze)
3+
(libraries chlib chutil cchlib cchpre cchanalyze tchlib)
4+
(public_name codehawk.tcchanalyze)
5+
(wrapped false))

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

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
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+
module A = TCHAssertion
30+
31+
let expect_safe_detail
32+
?(msg="")
33+
~(po: CCHPreTypes.proof_obligation_int)
34+
~(xdetail: string)
35+
~(expl: string)
36+
() =
37+
match po#get_status with
38+
| Green ->
39+
(match po#get_explanation with
40+
| Some x ->
41+
let dmatch = (expl = "") || (expl = x.smsg_msg) in
42+
if not dmatch then
43+
A.equal_string ~msg:"Explanation is different" expl x.smsg_msg
44+
else
45+
(match x.smsg_loc with
46+
| Some ocode ->
47+
A.equal_string ~msg xdetail ocode.ocode_detail
48+
| _ ->
49+
A.fail_msg "Received explanation without location detail")
50+
| _ ->
51+
A.fail_msg "Received proof obligation without explanation")
52+
| s ->
53+
A.fail_msg
54+
("Received proof obligation with status "
55+
^ (CCHPreSumTypeSerializer.po_status_mfts#ts s))

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

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
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+
30+
val expect_safe_detail:
31+
?msg:string
32+
-> po:CCHPreTypes.proof_obligation_int
33+
-> xdetail:string
34+
-> expl:string
35+
-> unit
36+
-> unit

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

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
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+
(* cchlib *)
30+
open CCHBasicTypes
31+
open CCHSettings
32+
open CCHTypesToPretty
33+
34+
(* cchpre *)
35+
open CCHPreTypes
36+
37+
38+
let p2s = CHPrettyUtil.pretty_to_string
39+
40+
41+
let default_domains = [
42+
CCHInvariantFact.linear_equalities_domain;
43+
CCHInvariantFact.pepr_domain;
44+
CCHInvariantFact.valueset_domain;
45+
CCHInvariantFact.intervals_domain;
46+
CCHInvariantFact.symbolic_sets_domain;
47+
CCHInvariantFact.sym_pointersets_domain
48+
]
49+
50+
51+
let unpack_tar_gz (filename: string) =
52+
let targzname = Filename.concat "testinputs" (filename ^ ".cch.tar.gz") in
53+
let cchdirname = filename ^ ".cch" in
54+
let rmcmd = Filename.quote_command "rm" ["-rf"; cchdirname] in
55+
let xtarcmd = Filename.quote_command "tar" ["xfz"; targzname] in
56+
let _ = Sys.command rmcmd in
57+
let _ = Sys.command xtarcmd in
58+
()
59+
60+
61+
let analysis_setup ?(domains=default_domains) (filename: string) =
62+
begin
63+
unpack_tar_gz filename;
64+
system_settings#set_projectname filename;
65+
system_settings#set_cfilename filename;
66+
CCHCreatePrimaryProofObligations.primary_process_file ();
67+
CCHProofScaffolding.proof_scaffolding#reset;
68+
CCHGenerateAndCheck.generate_and_check_process_file domains
69+
end
70+
71+
72+
let exp_to_string (exp: exp) = p2s (exp_to_pretty exp)
73+
74+
let located_po_to_string (po: proof_obligation_int) =
75+
let loc = po#get_location in
76+
"("
77+
^ (string_of_int loc.line)
78+
^ ", "
79+
^ (string_of_int loc.byte)
80+
^ ") "
81+
^ (p2s (CCHPOPredicate.po_predicate_to_pretty po#get_predicate))
82+
^ ": "
83+
^ (match po#get_explanation with
84+
| Some smsg -> smsg.smsg_msg | _ -> "no explanation")
85+
86+
87+
let select_target_po
88+
?(reqargs:string list = [])
89+
?(line:int = -1)
90+
?(byte:int = -1)
91+
(po_s: proof_obligation_int list):
92+
(proof_obligation_int option * string list) =
93+
let (po_match, po_no_match) =
94+
List.fold_left (fun (po_match, po_no_match) po ->
95+
let p = po#get_predicate in
96+
let p_args = CCHPOPredicate.collect_indexed_predicate_expressions p in
97+
let p_args = List.map snd p_args in
98+
let p_args = List.map exp_to_string p_args in
99+
let reqargs =
100+
match reqargs with
101+
| [] -> List.init (List.length p_args) (fun _ -> "")
102+
| _ -> reqargs in
103+
let pomatch =
104+
List.fold_left2
105+
(fun acc actual req -> acc && (req = "" || actual = req))
106+
true p_args reqargs in
107+
let pomatch = pomatch && (line = (-1) || line = po#get_location.line) in
108+
let pomatch = pomatch && (byte = (-1) || byte = po#get_location.byte) in
109+
if pomatch then
110+
(po :: po_match, po_no_match)
111+
else
112+
(po_match, po :: po_no_match)) ([], []) po_s in
113+
match po_match with
114+
| [po] -> (Some po, List.map located_po_to_string po_no_match)
115+
| _ -> (None, List.map located_po_to_string po_s)

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

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
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+
30+
val analysis_setup: ?domains:string list -> string -> unit
31+
32+
val select_target_po:
33+
?reqargs:string list
34+
-> ?line:int
35+
-> ?byte:int
36+
-> CCHPreTypes.proof_obligation_int list
37+
-> (CCHPreTypes.proof_obligation_int option * string list)

0 commit comments

Comments
 (0)