Skip to content

Commit bf2b0a3

Browse files
sipmasipma
committed
CHT: add tests for decomposing array expressions
1 parent 8563f0c commit bf2b0a3

File tree

11 files changed

+803
-5
lines changed

11 files changed

+803
-5
lines changed

‎CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/dune‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
(library
22
(name tbchlib)
3-
(libraries bchlib chlib chutil tchlib)
3+
(libraries bchlib chlib chutil xprlib tchlib)
44
(public_name codehawk.tbchlib)
55
(wrapped false))

‎CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.ml‎

Lines changed: 75 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,10 +30,14 @@
3030

3131
(* chlib *)
3232
open CHLanguage
33+
open CHNumerical
3334

3435
(* chutil *)
3536
open CHTraceResult
3637

38+
(* xprlib *)
39+
open XprTypes
40+
3741
(* bchlib *)
3842
open BCHARMFunctionInterface
3943
open BCHBCTypePretty
@@ -42,6 +46,7 @@ open BCHBCTypeUtil
4246
open BCHCPURegisters
4347
open BCHFtsParameter
4448
open BCHLibTypes
49+
open BCHMemoryReference
4550

4651
module A = TCHAssertion
4752

@@ -57,8 +62,9 @@ let e31 = e15 * e16
5762
let e32 = e16 * e16
5863

5964

60-
let string_printer = CHPrettyUtil.string_printer
61-
let p2s = string_printer#print
65+
let p2s = CHPrettyUtil.string_printer#print
66+
let x2p = XprToPretty.xpr_formatter#pr_expr
67+
let x2s x = p2s (x2p x)
6268

6369

6470
let equal_doubleword =
@@ -117,6 +123,73 @@ let equal_string_imm_result_string
117123
A.equal_string expected (TR.tget_ok immr)#to_string
118124

119125

126+
let equal_array_index_offset
127+
?(msg="")
128+
~(expected: (xpr_t * numerical_t) option)
129+
~(received: (xpr_t * numerical_t) option)
130+
() =
131+
let pri (x, n) = "(" ^ (x2s x) ^ ", " ^ n#toString ^ ")" in
132+
match (expected, received) with
133+
| (None, None) -> ()
134+
| (Some x, None) ->
135+
A.fail_msg ("Expected Some " ^ (pri x) ^ ", but received None")
136+
| (None, Some x) ->
137+
A.fail_msg ("Expected None, but received Some " ^ (pri x))
138+
| (Some x1, Some x2) ->
139+
A.make_equal
140+
(fun (x1, n1) (x2, n2) -> ((x2s x1) = (x2s x2)) && n1#equal n2)
141+
(fun (x, n) -> "(" ^ (x2s x) ^ ", " ^ n#toString ^ ")")
142+
~msg
143+
x1
144+
x2
145+
146+
147+
let equal_memory_offset
148+
?(msg="")
149+
~(expected: memory_offset_t)
150+
~(received: memory_offset_t)
151+
() =
152+
match (expected, received) with
153+
| (UnknownOffset, UnknownOffset) -> ()
154+
| (m, UnknownOffset) ->
155+
A.fail_msg
156+
("Expected a known offset " ^ (memory_offset_to_string m)
157+
^ ", but received UnknownOffset")
158+
| (UnknownOffset, m) ->
159+
A.fail_msg
160+
("Expected UnknownOffset but received " ^ (memory_offset_to_string m))
161+
| _ ->
162+
A.make_equal
163+
(fun m1 m2 -> (memory_offset_compare m1 m2) = 0)
164+
memory_offset_to_string
165+
~msg
166+
expected
167+
received
168+
169+
170+
let equal_opt_meminfo
171+
?(msg="")
172+
~(expected: (memory_reference_int * memory_offset_t) option)
173+
~(received: (memory_reference_int * memory_offset_t) option)
174+
() =
175+
let pri (m, o) =
176+
"(" ^ (p2s m#toPretty) ^ ", " ^ (memory_offset_to_string o) ^ ")" in
177+
match (expected, received) with
178+
| (None, None) -> ()
179+
| (Some x, None) ->
180+
A.fail_msg ("Expected Some " ^ (pri x) ^ ", but received None")
181+
| (None, Some x) ->
182+
A.fail_msg ("Expected None, but received Some " ^ (pri x))
183+
| (Some x1, Some x2) ->
184+
A.make_equal
185+
(fun (m1, o1) (m2, o2) ->
186+
(m1#compare m2) = 0 && (memory_offset_compare o1 o2) = 0)
187+
pri
188+
~msg
189+
x1
190+
x2
191+
192+
120193
let equal_assignments
121194
?(msg="")
122195
(finfo: function_info_int)

‎CodeHawk/CHT/CHB_tests/bchlib_tests/tbchlib/tCHBchlibAssertion.mli‎

Lines changed: 29 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
88
Copyright (c) 2005-2019 Kestrel Technology LLC
99
Copyright (c) 2020-2021 Henny Sipma
10-
Copyright (c) 2022-2023 Aarno Labs LLC
10+
Copyright (c) 2022-2024 Aarno Labs LLC
1111
1212
Permission is hereby granted, free of charge, to any person obtaining a copy
1313
of this software and associated documentation files (the "Software"), to deal
@@ -30,10 +30,14 @@
3030

3131
(* chlib *)
3232
open CHLanguage
33+
open CHNumerical
3334

3435
(* chutil *)
3536
open CHTraceResult
3637

38+
(* xprlib *)
39+
open XprTypes
40+
3741
(* bchlib *)
3842
open BCHARMFunctionInterface
3943
open BCHBCTypes
@@ -73,6 +77,30 @@ val equal_string_imm_result_string:
7377
?msg:string -> string -> immediate_result -> unit
7478

7579

80+
val equal_array_index_offset:
81+
?msg:string
82+
-> expected:(xpr_t * numerical_t) option
83+
-> received:(xpr_t * numerical_t) option
84+
-> unit
85+
-> unit
86+
87+
88+
val equal_memory_offset:
89+
?msg:string
90+
-> expected: memory_offset_t
91+
-> received: memory_offset_t
92+
-> unit
93+
-> unit
94+
95+
96+
val equal_opt_meminfo:
97+
?msg:string
98+
-> expected:(memory_reference_int * memory_offset_t) option
99+
-> received:(memory_reference_int * memory_offset_t) option
100+
-> unit
101+
-> unit
102+
103+
76104
val equal_assignments:
77105
?msg:string
78106
-> function_info_int

‎CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/Makefile‎

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ XPRLIB = $(CODEHAWK)/CH/xprlib
1313
BCHCIL = $(CODEHAWK)/CHB/bchcil
1414
BCHLIB = $(CODEHAWK)/CHB/bchlib
1515
TESTLIB = $(CHT)/tchlib
16+
XTESTLIB = $(CHT)/CH_tests/xprlib_tests/txprlib
1617
BCHLIBTESTLIB = $(CHT)/CHB_tests/bchlib_tests/tbchlib
1718

1819
CAMLDOC := ocamldoc
@@ -27,6 +28,7 @@ CAMLC := ocamlopt -I str -I cmi -I cmx \
2728
-I $(BCHLIB)/cmi \
2829
-I $(BCHCIL)/cmi \
2930
-I $(TESTLIB)/cmi \
31+
-I $(XTESTLIB)/cmi \
3032
-I $(BCHLIBTESTLIB)/cmi \
3133

3234
CAMLLINK := ocamlopt str.cmxa unix.cmxa \
@@ -43,6 +45,7 @@ CAMLLINK := ocamlopt str.cmxa unix.cmxa \
4345
$(BCHLIB)/bchlib.cmxa \
4446
$(BCHCIL)/bchcil.cmxa \
4547
$(TESTLIB)/tchlib.cmxa \
48+
$(XTESTLIB)/txprlib.cmxa \
4649
$(BCHLIBTESTLIB)/tbchlib.cmxa \
4750

4851
MLIS := \
@@ -53,7 +56,7 @@ SOURCES := \
5356

5457
OBJECTS := $(addprefix cmx/,$(SOURCES:%=%.cmx))
5558

56-
all: make_dirs bCHDoublewordTest bCHImmediateTest bCHLocationTest bCHStreamWrapperTest bCHFunctionInterfaceTest bCHARMFunctionInterfaceTest bCHTypeConstraintStoreTest
59+
all: make_dirs bCHDoublewordTest bCHImmediateTest bCHLocationTest bCHStreamWrapperTest bCHXprUtilTest bCHMemoryReferenceTest bCHFunctionInterfaceTest bCHARMFunctionInterfaceTest bCHFlocTest bCHTypeConstraintStoreTest
5760

5861
doc:
5962

@@ -73,13 +76,23 @@ bCHLocationTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(
7376
bCHStreamWrapperTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(BCHLIBTESTLIB)/tbchlib.cmxa cmi/bCHStreamWrapperTest.cmi cmx/bCHStreamWrapperTest.cmx
7477
$(CAMLLINK) -o bCHStreamWrapperTest $(OBJECTS) cmx/bCHStreamWrapperTest.cmx
7578

79+
bCHXprUtilTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(XPRLIB)/xpr.cmxa $(TESTLIB)/tchlib.cmxa $(BCHLIBTESTLIB)/tbchlib.cmxa cmi/bCHXprUtilTest.cmi cmx/bCHXprUtilTest.cmx
80+
$(CAMLLINK) -o bCHXprUtilTest $(OBJECTS) cmx/bCHXprUtilTest.cmx
81+
82+
bCHMemoryReferenceTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CHUTIL)/chutil.cmxa $(TESTLIB)/tchlib.cmxa $(BCHLIBTESTLIB)/tbchlib.cmxa cmi/bCHMemoryReferenceTest.cmi cmx/bCHMemoryReferenceTest.cmx
83+
$(CAMLLINK) -o bCHMemoryReferenceTest $(OBJECTS) cmx/bCHMemoryReferenceTest.cmx
84+
7685
bCHFunctionInterfaceTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CIL)/goblintCil.cmxa $(CHUTIL)/chutil.cmxa $(BCHCIL)/bchcil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(BCHLIBTESTLIB)/tbchlib.cmxa cmi/bCHFunctionInterfaceTest.cmi cmx/bCHFunctionInterfaceTest.cmx
7786
$(CAMLLINK) -o bCHFunctionInterfaceTest $(OBJECTS) cmx/bCHFunctionInterfaceTest.cmx
7887

7988
bCHARMFunctionInterfaceTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CIL)/goblintCil.cmxa $(CHUTIL)/chutil.cmxa $(BCHCIL)/bchcil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(BCHLIBTESTLIB)/tbchlib.cmxa cmi/bCHARMFunctionInterfaceTest.cmi cmx/bCHARMFunctionInterfaceTest.cmx
8089
$(CAMLLINK) -o bCHARMFunctionInterfaceTest $(OBJECTS) cmx/bCHARMFunctionInterfaceTest.cmx
8190

8291

92+
bCHFlocTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CIL)/goblintCil.cmxa $(CHUTIL)/chutil.cmxa $(BCHCIL)/bchcil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(BCHLIBTESTLIB)/tbchlib.cmxa cmi/bCHFlocTest.cmi cmx/bCHFlocTest.cmx
93+
$(CAMLLINK) -o bCHFlocTest $(OBJECTS) cmx/bCHFlocTest.cmx
94+
95+
8396
bCHTypeConstraintStoreTest: $(OBJECTS) $(CMIS) $(CHLIB)/chlib.cmxa $(CIL)/goblintCil.cmxa $(CHUTIL)/chutil.cmxa $(BCHCIL)/bchcil.cmxa $(ZIPLIB)/zip.cmxa $(TESTLIB)/tchlib.cmxa $(BCHLIBTESTLIB)/tbchlib.cmxa cmi/bCHTypeConstraintStoreTest.cmi cmx/bCHTypeConstraintStoreTest.cmx
8497
$(CAMLLINK) -o bCHTypeConstraintStoreTest $(OBJECTS) cmx/bCHTypeConstraintStoreTest.cmx
8598

@@ -88,9 +101,12 @@ run: bCHDoublewordTest bCHImmediateTest bCHLocationTest bCHStreamWrapperTest
88101
./bCHImmediateTest
89102
./bCHLocationTest
90103
./bCHStreamWrapperTest
104+
./bCHXprUtilTest
105+
./bCHMemoryReferenceTest
91106
./bCHFunctionInterfaceTest
92107
./bCHARMFunctionInterfaceTest
93108
./bCHTypeConstraintStoreTest
109+
./bCHFlocTest
94110

95111
cmi/%.cmi: %.mli
96112
$(CAMLC) -o $@ -c -opaque $<
@@ -115,6 +131,11 @@ clean:
115131
rm -f bCHDoublewordTest
116132
rm -f bCHImmediateTest
117133
rm -f bCHLocationTest
134+
rm -f bCHStreamWrapperTest
135+
rm -f bCHXprUtilTest
136+
rm -f bCHMemoryReferenceTest
118137
rm -f bCHFunctionInterfaceTest
119138
rm -f bCHTypeConstraintStoreTest
139+
rm -f bCHARMFunctionInterfaceTest
140+
rm -f bCHFlocTest
120141
rm -rf doc

0 commit comments

Comments
 (0)