Skip to content

Commit 7724092

Browse files
NlightNFotisNlightNFotis
committed
Adding initial version of goto-inspect.
This allows to inspect a goto-binary (this means showing the goto-functions, for now at least). The reason this binary is helpful is that different tools (CBMC, goto-instrument, etc) perform instrumentation before showing the goto-functions, and there's a need to be able to inspect certain properties of a goto-binary without doing instrumentation.
1 parent 68af7a4 commit 7724092

File tree

18 files changed

+336
-2
lines changed

18 files changed

+336
-2
lines changed

‎CMakeLists.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -158,6 +158,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
158158
"$<TARGET_FILE:goto-cc>"
159159
"$<TARGET_FILE:goto-diff>"
160160
"$<TARGET_FILE:goto-instrument>"
161+
"$<TARGET_FILE:goto-inspect>"
161162
"$<TARGET_FILE:goto-synthesizer>"
162163
"$<TARGET_FILE:janalyzer>"
163164
"$<TARGET_FILE:jbmc>"
@@ -230,6 +231,7 @@ cprover_default_properties(
230231
goto-checker
231232
goto-diff
232233
goto-diff-lib
234+
goto-inspect
233235
goto-harness
234236
goto-instrument
235237
goto-instrument-lib

‎CODEOWNERS‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@
5353
/src/goto-harness/ @martin-cs @chris-ryder @peterschrammel
5454
/src/goto-instrument/ @martin-cs @chris-ryder @peterschrammel @tautschnig @kroening
5555
/src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000
56+
/src/goto-inspect/ @diffblue/diffblue-opensource
5657
/src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
5758
/src/goto-diff/ @tautschnig @peterschrammel
5859
/src/jsil/ @kroening @tautschnig

‎doc/man/goto-inspect.1‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
.TH GOTO-INSPECT "2" "May 2023" "goto-inspect-5.81.0" "User Commands"
2+
.SH NAME
3+
goto\-inspect \- Inspect goto-binaries.
4+
.SH SYNOPSIS
5+
.TP
6+
.B goto\-inspect [\-?] [\-h] [\-\-help]
7+
show help
8+
.TP
9+
.B goto\-inspect \-\-version
10+
show version and exit
11+
.TP
12+
.B goto\-inspect [options] \fIin\fR
13+
Inspect (show properties, goto-functions, etc of) given goto-binary.
14+
.SH DESCRIPTION
15+
\fBgoto-inspect\fR reads a GOTO binary, and shows goto-functions, properties,
16+
and other attributes associated with the goto-program.
17+
.SH OPTIONS
18+
.SS "User-interface options:"
19+
.TP
20+
\fB\-\-show\-goto\-functions\fR
21+
print the goto-program instructions for the functions contained by the binary.
22+
.SH ENVIRONMENT
23+
All tools honor the TMPDIR environment variable when generating temporary
24+
files and directories.
25+
.SH BUGS
26+
If you encounter a problem please create an issue at
27+
.B https://github.com/diffblue/cbmc/issues
28+
.SH SEE ALSO
29+
.BR cbmc (1),
30+
.BR goto-cc (1)
31+
.BR goto-instrument (1)
32+
.SH COPYRIGHT
33+
2023, Diffblue Ltd.

‎regression/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ add_subdirectory(goto-instrument-chc)
4646
add_subdirectory(goto-instrument-json)
4747
add_subdirectory(goto-instrument-wmm-core)
4848
add_subdirectory(goto-instrument-typedef)
49+
add_subdirectory(goto-inspect)
4950
add_subdirectory(smt2_solver)
5051
add_subdirectory(smt2_strings)
5152
add_subdirectory(strings)

‎regression/goto-inspect/CMakeLists.txt‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
2+
set(is_windows true)
3+
set(exclude_win_broken_tests -X winbug)
4+
else()
5+
set(is_windows false)
6+
set(exclude_win_broken_tests "")
7+
endif()
8+
9+
add_test_pl_tests(
10+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-inspect> ${is_windows}" ${exclude_win_broken_tests}
11+
)

‎regression/goto-inspect/chain.sh‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
# A test instruction passed to this `chain.sh` file looks like this:
6+
#
7+
# build/bin/goto-cc build/bin/goto-inspect --show-goto-functions main.c
8+
#
9+
# This allows us to safely assume for now (as long as we're operating
10+
# goto-inspect with one binary and one inspection option, which seems
11+
# to be the case for now) that the option is going to be at $4.
12+
# If this is no longer the case in the future, this script will need
13+
# to be made significantly more sophisticated in terms of handling
14+
# a variable number of options for the goto-inspect binary.
15+
16+
goto_cc_exe=$1
17+
goto_inspect_exe=$2
18+
is_windows=$3
19+
20+
name=${*:$#}
21+
name=${name%.c}
22+
23+
# We need to dispatch to the appropriate platform executable because
24+
# they accept different options.
25+
if [[ "${is_windows}" == "true" ]]; then
26+
$goto_cc_exe "${name}.c" "/Fe${name}.gb"
27+
else
28+
$goto_cc_exe -o "${name}.gb" "${name}.c"
29+
fi
30+
31+
$goto_inspect_exe $4 "${name}.gb"

‎regression/goto-inspect/show-goto-functions/main.c‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
int main(int argc, char *argv[])
2+
{
3+
int arr[] = {0, 1, 2, 3, 4};
4+
__CPROVER_assert(arr[0] != 0, "Expected failure: 0 == 0");
5+
}

‎regression/goto-inspect/show-goto-functions/negative.desc‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
CORE winbug
2+
main.c
3+
" "
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
--
7+
DECL main::1::arr : signedbv\[32\]\[5\]
8+
ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \}
9+
ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0
10+
DEAD main::1::arr
11+
SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1"
12+
END_FUNCTION
13+
--
14+
This is testing the behaviour of the goto-inspect binary in case a binary
15+
is present, but no inspection option is present.
16+
17+
This is labelled `winbug` to avoid running on windows because of issues with
18+
the empty string in line 3 (simulating the lack of an option) not working as
19+
it should (it is contrary to the behaviour of unix systems). The behaviour
20+
has been verified manually on a machine as working as expected, but getting
21+
the test to run automatically is a lot more involved, so we're opting to
22+
skipping this on that platform for now.

‎regression/goto-inspect/show-goto-functions/positive.desc‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--show-goto-functions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main
7+
DECL main::1::arr : signedbv\[32\]\[5\]
8+
ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \}
9+
ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0
10+
DEAD main::1::arr
11+
SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1"
12+
END_FUNCTION
13+
--
14+
--

‎src/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,7 @@ add_subdirectory(xmllang)
9898
add_subdirectory(goto-checker)
9999
add_subdirectory(goto-programs)
100100
add_subdirectory(goto-symex)
101+
add_subdirectory(goto-inspect)
101102
add_subdirectory(jsil)
102103
add_subdirectory(json)
103104
add_subdirectory(json-symtab-language)

0 commit comments

Comments
 (0)