Skip to content

Commit f4fd908

Browse files
committed
Add integration test of JSON <-> GOTO
Tests the full workflow of reading and writing JSON.
1 parent 44abbcb commit f4fd908

File tree

5 files changed

+322
-0
lines changed

5 files changed

+322
-0
lines changed

CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -225,6 +225,7 @@ option(WITH_MEMORY_ANALYZER
225225
add_subdirectory(src)
226226
add_subdirectory(regression)
227227
add_subdirectory(unit)
228+
add_subdirectory(integration)
228229

229230
cprover_default_properties(
230231
analyses

integration/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
add_subdirectory(json-symtab)
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
if(NOT EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/test.sh)
2+
configure_file(
3+
${CMAKE_CURRENT_SOURCE_DIR}/test.sh.in
4+
${CMAKE_CURRENT_SOURCE_DIR}/test.sh
5+
@ONLY
6+
)
7+
endif()
8+
9+
add_test(
10+
NAME json-symtab-integration
11+
COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/test.sh
12+
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
13+
)

integration/json-symtab/Makefile

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
default: test
2+
3+
test:
4+
@echo "Running JSON symtab integration tests"
5+
@chmod +x test.sh
6+
@./test.sh
7+
8+
clean:
9+
@echo "Cleaning up temporary files"
10+
@rm -f *.gb *.json
11+
12+
.PHONY: default test clean

integration/json-symtab/test.sh.in

Lines changed: 295 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,295 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
# Path to the symtab2gb binary
6+
SYMTAB2GB="@CMAKE_BINARY_DIR@/bin/symtab2gb"
7+
8+
# Create a temporary directory for our test files
9+
TEMP_DIR=$(mktemp -d)
10+
trap 'rm -rf $TEMP_DIR' EXIT
11+
12+
# Function to check if a command succeeded
13+
check_result() {
14+
if [ $? -ne 0 ]; then
15+
echo "Test failed: $1"
16+
exit 1
17+
fi
18+
}
19+
20+
# Test 1: Basic JSON symbol table and goto functions
21+
echo "Test 1: Basic JSON symbol table and goto functions"
22+
23+
# Create a simple JSON symbol table
24+
cat > $TEMP_DIR/symbols.json << EOF
25+
{
26+
"symbols": {
27+
"main": {
28+
"name": "main",
29+
"type": {
30+
"id": "code",
31+
"return_type": {
32+
"id": "signedbv",
33+
"width": 32
34+
},
35+
"parameters": []
36+
},
37+
"value": null,
38+
"is_lvalue": false,
39+
"is_static_lifetime": false,
40+
"is_thread_local": false,
41+
"is_file_local": false,
42+
"is_parameter": false,
43+
"is_auxiliary": false,
44+
"is_macro": false,
45+
"mode": "C"
46+
}
47+
}
48+
}
49+
EOF
50+
51+
# Create a simple JSON goto functions
52+
cat > $TEMP_DIR/functions.json << EOF
53+
{
54+
"functions": {
55+
"main": {
56+
"body": {
57+
"instructions": [
58+
{
59+
"type": "SKIP",
60+
"location": {
61+
"file": "test.c",
62+
"line": 1
63+
}
64+
},
65+
{
66+
"type": "END_FUNCTION",
67+
"location": {
68+
"file": "test.c",
69+
"line": 2
70+
}
71+
}
72+
]
73+
},
74+
"parameter_identifiers": []
75+
}
76+
}
77+
}
78+
EOF
79+
80+
# Generate a goto binary from the JSON files
81+
$SYMTAB2GB --symbols $TEMP_DIR/symbols.json --functions $TEMP_DIR/functions.json --output $TEMP_DIR/test1.gb
82+
check_result "Failed to generate goto binary from valid JSON files"
83+
84+
# Verify the generated binary contains the expected function
85+
$SYMTAB2GB --show-symbol-table $TEMP_DIR/test1.gb | grep -q "main"
86+
check_result "Generated binary does not contain the expected symbol"
87+
88+
# Test 2: Complex JSON symbol table and goto functions
89+
echo "Test 2: Complex JSON symbol table and goto functions"
90+
91+
# Create a more complex JSON symbol table
92+
cat > $TEMP_DIR/complex_symbols.json << EOF
93+
{
94+
"symbols": {
95+
"main": {
96+
"name": "main",
97+
"type": {
98+
"id": "code",
99+
"return_type": {
100+
"id": "signedbv",
101+
"width": 32
102+
},
103+
"parameters": []
104+
},
105+
"value": null,
106+
"is_lvalue": false,
107+
"is_static_lifetime": false,
108+
"is_thread_local": false,
109+
"is_file_local": false,
110+
"is_parameter": false,
111+
"is_auxiliary": false,
112+
"is_macro": false,
113+
"mode": "C"
114+
},
115+
"x": {
116+
"name": "x",
117+
"type": {
118+
"id": "signedbv",
119+
"width": 32
120+
},
121+
"value": {
122+
"id": "constant",
123+
"value": "42"
124+
},
125+
"is_lvalue": true,
126+
"is_static_lifetime": true,
127+
"is_thread_local": false,
128+
"is_file_local": false,
129+
"is_parameter": false,
130+
"is_auxiliary": false,
131+
"is_macro": false,
132+
"mode": "C"
133+
}
134+
}
135+
}
136+
EOF
137+
138+
# Create a more complex JSON goto functions
139+
cat > $TEMP_DIR/complex_functions.json << EOF
140+
{
141+
"functions": {
142+
"main": {
143+
"body": {
144+
"instructions": [
145+
{
146+
"type": "ASSIGN",
147+
"code": {
148+
"id": "code",
149+
"statement": "assign",
150+
"lhs": {
151+
"id": "symbol",
152+
"identifier": "x"
153+
},
154+
"rhs": {
155+
"id": "constant",
156+
"value": "10"
157+
}
158+
},
159+
"location": {
160+
"file": "test.c",
161+
"line": 1
162+
}
163+
},
164+
{
165+
"type": "GOTO",
166+
"targets": [2],
167+
"guard": {
168+
"id": "gt",
169+
"op0": {
170+
"id": "symbol",
171+
"identifier": "x"
172+
},
173+
"op1": {
174+
"id": "constant",
175+
"value": "0"
176+
}
177+
},
178+
"location": {
179+
"file": "test.c",
180+
"line": 2
181+
}
182+
},
183+
{
184+
"type": "SKIP",
185+
"location": {
186+
"file": "test.c",
187+
"line": 3
188+
}
189+
},
190+
{
191+
"type": "END_FUNCTION",
192+
"location": {
193+
"file": "test.c",
194+
"line": 4
195+
}
196+
}
197+
]
198+
},
199+
"parameter_identifiers": []
200+
}
201+
}
202+
}
203+
EOF
204+
205+
# Generate a goto binary from the complex JSON files
206+
$SYMTAB2GB --symbols $TEMP_DIR/complex_symbols.json --functions $TEMP_DIR/complex_functions.json --output $TEMP_DIR/test2.gb
207+
check_result "Failed to generate goto binary from complex JSON files"
208+
209+
# Verify the generated binary contains the expected symbols
210+
$SYMTAB2GB --show-symbol-table $TEMP_DIR/test2.gb | grep -q "main"
211+
check_result "Generated binary does not contain the main symbol"
212+
$SYMTAB2GB --show-symbol-table $TEMP_DIR/test2.gb | grep -q "x"
213+
check_result "Generated binary does not contain the x symbol"
214+
215+
# Test 3: Error handling - Invalid JSON symbol table
216+
echo "Test 3: Error handling - Invalid JSON symbol table"
217+
218+
# Create an invalid JSON symbol table (missing closing brace)
219+
cat > $TEMP_DIR/invalid_symbols.json << EOF
220+
{
221+
"symbols": {
222+
"main": {
223+
"name": "main",
224+
"type": {
225+
"id": "code",
226+
"return_type": {
227+
"id": "signedbv",
228+
"width": 32
229+
},
230+
"parameters": []
231+
}
232+
233+
EOF
234+
235+
# Try to generate a goto binary from the invalid JSON files
236+
if $SYMTAB2GB --symbols $TEMP_DIR/invalid_symbols.json --functions $TEMP_DIR/functions.json --output $TEMP_DIR/test3.gb 2>/dev/null; then
237+
echo "Test failed: Expected error for invalid JSON symbol table"
238+
exit 1
239+
fi
240+
241+
# Test 4: Error handling - Invalid JSON goto functions
242+
echo "Test 4: Error handling - Invalid JSON goto functions"
243+
244+
# Create an invalid JSON goto functions (invalid instruction type)
245+
cat > $TEMP_DIR/invalid_functions.json << EOF
246+
{
247+
"functions": {
248+
"main": {
249+
"body": {
250+
"instructions": [
251+
{
252+
"type": "INVALID_TYPE",
253+
"location": {
254+
"file": "test.c",
255+
"line": 1
256+
}
257+
},
258+
{
259+
"type": "END_FUNCTION",
260+
"location": {
261+
"file": "test.c",
262+
"line": 2
263+
}
264+
}
265+
]
266+
},
267+
"parameter_identifiers": []
268+
}
269+
}
270+
}
271+
EOF
272+
273+
# Try to generate a goto binary from the invalid JSON files
274+
if $SYMTAB2GB --symbols $TEMP_DIR/symbols.json --functions $TEMP_DIR/invalid_functions.json --output $TEMP_DIR/test4.gb 2>/dev/null; then
275+
echo "Test failed: Expected error for invalid JSON goto functions"
276+
exit 1
277+
fi
278+
279+
# Test 5: Error handling - Missing required files
280+
echo "Test 5: Error handling - Missing required files"
281+
282+
# Try to generate a goto binary without specifying the symbol table
283+
if $SYMTAB2GB --functions $TEMP_DIR/functions.json --output $TEMP_DIR/test5.gb 2>/dev/null; then
284+
echo "Test failed: Expected error for missing symbol table"
285+
exit 1
286+
fi
287+
288+
# Try to generate a goto binary without specifying the goto functions
289+
if $SYMTAB2GB --symbols $TEMP_DIR/symbols.json --output $TEMP_DIR/test5.gb 2>/dev/null; then
290+
echo "Test failed: Expected error for missing goto functions"
291+
exit 1
292+
fi
293+
294+
echo "All tests passed!"
295+
exit 0

0 commit comments

Comments
 (0)