Skip to content

Commit b6ff03d

Browse files
karkhazkarkhaz
authored
Merge pull request #4790 from mmuesly/feature_dump_type_header
Feature dump-c-type-header flag
2 parents cd70727 + 004cd60 commit b6ff03d

File tree

18 files changed

+630
-45
lines changed

18 files changed

+630
-45
lines changed

‎regression/extract_type_header/Makefile

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
default: tests.log
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
is_windows=true
9+
else
10+
exe=../../../src/goto-cc/goto-cc
11+
is_windows=false
12+
endif
13+
14+
test:
15+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc ./../../../scripts/extract_type_header.py $(is_windows)'
16+
17+
tests.log:
18+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc ./../../../scripts/extract_type_header.py $(is_windows)'
19+
20+
show:
21+
@for dir in *; do \
22+
if [ -d "$$dir" ]; then \
23+
vim -o "$$dir/*.c" "$$dir/*.out"; \
24+
fi; \
25+
done;
26+
27+
clean:
28+
@for dir in *; do \
29+
$(RM) tests.log; \
30+
if [ -d "$$dir" ]; then \
31+
cd "$$dir"; \
32+
$(RM) *.out *.gb; \
33+
cd ..; \
34+
fi \
35+
done

‎regression/extract_type_header/c_file_with_defines/main.c

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
struct A
2+
{
3+
int a;
4+
int b;
5+
};
6+
7+
typedef struct A myStruct;
8+
9+
#define address a
10+
11+
#define bucket(X, Y, Z) \
12+
if(X) \
13+
{ \
14+
Z = get_b(X) == Y; \
15+
} \
16+
else \
17+
{ \
18+
Z = get_default() == Y; \
19+
}
20+
21+
#ifndef address
22+
# define address 1
23+
#endif
24+
25+
int get_b(myStruct *s)
26+
{
27+
return s->b;
28+
}
29+
30+
int get_default()
31+
{
32+
return 0;
33+
}
34+
35+
int main()
36+
{
37+
myStruct aStruct = {123, 456};
38+
__CPROVER_assert(aStruct.address == 123, "address");
39+
int z;
40+
bucket(&aStruct, 456, z);
41+
__CPROVER_assert(z, "bucket");
42+
}

‎regression/extract_type_header/c_file_with_defines/test.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
#define address a
7+
#define bucket\(X, Y, Z\)
8+
if\(X\)
9+
Z = get_b\(X\) == Y;
10+
else
11+
Z = get_default\(\) == Y;
12+
#ifndef address
13+
# define address 1
14+
#endif
15+
--

‎regression/extract_type_header/chain.sh

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
goto_cc=$1
6+
goto_instrument=$2
7+
cbmc=$3
8+
python_script=$4
9+
is_windows=$5
10+
11+
name=${*:$#}
12+
name=${name%.c}
13+
14+
args=${*:6:$#-6}
15+
16+
if [[ "${is_windows}" == "true" ]]; then
17+
$goto_cc "${name}.c"
18+
mv "${name}.exe" "${name}.gb"
19+
else
20+
$goto_cc -o "${name}.gb" "${name}.c"
21+
fi
22+
23+
export PATH=$PATH:"$(pwd)../../../src/goto-instrument/"
24+
$python_script "${name}.gb" "${name}.c" "header.h"
25+
cat "header.h"
26+
rm -f "header.h"

‎regression/goto-instrument/chain.sh

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,9 @@ rm -f "${name}-mod.gb"
2323
$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
2424
if [ ! -e "${name}-mod.gb" ] ; then
2525
cp "$name.gb" "${name}-mod.gb"
26+
elif echo $args | grep -q -- "--dump-c-type-header" ; then
27+
cat "${name}-mod.gb"
28+
mv "${name}.gb" "${name}-mod.gb"
2629
elif echo $args | grep -q -- "--dump-c" ; then
2730
mv "${name}-mod.gb" "${name}-mod.c"
2831

‎regression/goto-instrument/dump-type-header-exclude-non-module-var/data_structure.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
struct A
2+
{
3+
int a;
4+
int b;
5+
};
6+
7+
struct A default_config = {5, 6};

‎regression/goto-instrument/dump-type-header-exclude-non-module-var/main.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include "main.h"
2+
3+
struct B
4+
{
5+
int t;
6+
int g;
7+
};
8+
9+
#define temperature(x) x.t
10+
11+
int main()
12+
{
13+
struct B aStruct = {3, 8};
14+
__CPROVER_assert(my_config.a == 7, "Should be valid");
15+
my_config.a = nondet_int();
16+
17+
__CPROVER_assert(!(my_config.a == 4), "Should be nondet now");
18+
__CPROVER_assert(aStruct.t, "Should not be null");
19+
__CPROVER_assert(temperature(aStruct) == 3, "Trying the macro");
20+
}

‎regression/goto-instrument/dump-type-header-exclude-non-module-var/main.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#include "data_structure.h"
2+
3+
struct A my_config = {7, 8};

‎regression/goto-instrument/dump-type-header-exclude-non-module-var/test.desc

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE
2+
main.c
3+
--dump-c-type-header main
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
struct B
7+
// t
8+
signed int t;
9+
// g
10+
signed int g;
11+
Should be valid: SUCCESS
12+
Should be nondet now: FAILURE
13+
Should not be null: SUCCESS
14+
Trying the macro: SUCCESS
15+
#include "data_structure.h"
16+
--
17+
^warning: ignoring
18+
struct A default_config = \{5, 6\};
19+
struct A my_config=\{ .a=7, .b=8 \};

‎regression/goto-instrument/dump-type-header/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
struct A
2+
{
3+
int a;
4+
int b;
5+
};
6+
7+
int main()
8+
{
9+
struct A my_struct = {0};
10+
__CPROVER_assert(my_struct.a == 0, "Must be true");
11+
return 0;
12+
}

‎regression/goto-instrument/dump-type-header/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--dump-c-type-header main
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
struct A
7+
// a
8+
signed int a;
9+
// b
10+
signed int b;
11+
--
12+
^warning: ignoring

‎scripts/extract_type_header.py

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
#!/usr/bin/env python3
2+
#
3+
# Dump type header for private types in c modules.
4+
#
5+
# Author: Malte Mues <[email protected]>
6+
7+
import os
8+
import re
9+
import shutil
10+
import subprocess
11+
import sys
12+
import textwrap
13+
from tempfile import TemporaryDirectory
14+
15+
DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)")
16+
17+
18+
19+
def collect_defines(c_file):
20+
"""Collects all defines in a c module.
21+
22+
This function should collect all defines inside a c module.
23+
Than the script will add these defines to the type header file.
24+
This allows to use the defines in the harness as well. Because preprocessing
25+
eliminates them before compiling the goto binary,
26+
it is not possible to extract them from the goto binary.
27+
28+
We assume that a define is either a single define. For example
29+
#define my_macro 0
30+
31+
or eventually guarded by an ifdef, ifndef or if. For example:
32+
#ifdef another_macro
33+
#define my_macro
34+
#endif
35+
36+
Any opening if* is expected to be close by an #endif.
37+
Further, it is expected that #if and #endif pairs are not nested.
38+
39+
The third group of defines that this script tries to catch are multiline
40+
macros:
41+
42+
#define aMacro( X ) \
43+
if( ( X )->A == 1 ) \
44+
{ \
45+
( X )->B = 2; \
46+
}
47+
48+
The assumption is that '\' is the last character in the line.
49+
"""
50+
51+
collector_result = ""
52+
with open(c_file, "r") as in_file:
53+
continue_define = False
54+
in_potential_def_scope = ""
55+
potential_define = False
56+
potential_define_confirmed = False
57+
for line in in_file:
58+
matched = DEFINE_REGEX_HEADER.match(line)
59+
if line.strip().startswith("#if"):
60+
potential_define = True
61+
in_potential_def_scope += line
62+
elif line.strip().startswith("#endif") and potential_define:
63+
if potential_define_confirmed:
64+
in_potential_def_scope += line
65+
collector_result += in_potential_def_scope
66+
in_potential_def_scope = ""
67+
potential_define = False
68+
potential_define_confirmed = False
69+
elif matched and potential_define:
70+
potential_define_confirmed = True
71+
in_potential_def_scope += line
72+
elif matched or continue_define:
73+
continue_define = line.strip("\n").endswith("\\")
74+
collector_result += line
75+
elif potential_define:
76+
in_potential_def_scope += line
77+
return collector_result
78+
79+
80+
def get_module_name(c_file):
81+
base = os.path.basename(c_file)
82+
return base.split(".")[0]
83+
84+
85+
def make_header_file(goto_binary, c_file, header_out=None):
86+
with TemporaryDirectory() as tmpdir:
87+
module = get_module_name(c_file)
88+
89+
header_file = module + "_datastructure.h"
90+
91+
drop_header_cmd = ["goto-instrument",
92+
"--dump-c-type-header",
93+
module,
94+
goto_binary,
95+
header_file]
96+
subprocess.run(drop_header_cmd,
97+
stdout=subprocess.PIPE,
98+
stderr=subprocess.STDOUT,
99+
check=False,
100+
universal_newlines=True,
101+
cwd=tmpdir,
102+
shell=False)
103+
104+
header_file = os.path.normpath(os.path.join(tmpdir, header_file))
105+
with open(header_file, "a") as out:
106+
print(collect_defines(c_file), file=out)
107+
108+
if header_out:
109+
absolut_header_target = os.path.normpath(
110+
os.path.abspath(header_out))
111+
shutil.move(header_file, absolut_header_target)
112+
else:
113+
with open(header_file, "r") as header:
114+
print("".join(header.readlines()))
115+
116+
117+
def print_usage_and_exit():
118+
print(textwrap.dedent("""\
119+
This script extracts a type header for local types in a c file.
120+
It expects a goto binary compiled from the c file
121+
along with the original c file.
122+
123+
extract_type_header.py my_goto_binary the_c_file [header_output]
124+
125+
The header_output is an optional parameter specifying a target output
126+
file. Otherwise, the script is going to print the header to stdout.
127+
"""))
128+
sys.exit(1)
129+
130+
if __name__ == '__main__':
131+
TARGET = None
132+
if len(sys.argv) < 3 or len(sys.argv) > 4:
133+
print_usage_and_exit()
134+
BINARY = sys.argv[1]
135+
if not os.path.isabs(BINARY):
136+
BINARY = os.path.normpath(os.path.join(os.getcwd(), BINARY))
137+
FILE = sys.argv[2]
138+
if not os.path.isabs(FILE):
139+
FILE = os.path.normpath(os.path.join(os.getcwd(), FILE))
140+
if len(sys.argv) == 4:
141+
TARGET = sys.argv[3]
142+
if not os.path.isabs(TARGET):
143+
TARGET= os.path.normpath(os.path.join(os.getcwd(), TARGET))
144+
make_header_file(BINARY, FILE, TARGET)

0 commit comments

Comments
 (0)