Skip to content

Commit 4aceefd

Browse files
qinhepingqinheping
authored
Merge pull request #7415 from qinheping/goto-synthesizer
goto-synthesizer: Separate front-end for loop-contracts synthesizer
2 parents de504f5 + b03d870 commit 4aceefd

13 files changed

+320
-1
lines changed

‎CMakeLists.txt‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -157,6 +157,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
157157
"$<TARGET_FILE:goto-cc>"
158158
"$<TARGET_FILE:goto-diff>"
159159
"$<TARGET_FILE:goto-instrument>"
160+
"$<TARGET_FILE:goto-synthesizer>"
160161
"$<TARGET_FILE:janalyzer>"
161162
"$<TARGET_FILE:jbmc>"
162163
"$<TARGET_FILE:jdiff>"
@@ -233,6 +234,8 @@ cprover_default_properties(
233234
goto-instrument-lib
234235
goto-programs
235236
goto-symex
237+
goto-synthesizer
238+
goto-synthesizer-lib
236239
jsil
237240
json
238241
json-symtab-language

‎CODEOWNERS‎

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

‎doc/man/goto-synthesizer.1‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
.TH GOTO-SYNTHESIZER "1" "December 2022" "goto-synthesizer-5.59.0" "User Commands"
2+
.SH NAME
3+
goto\-synthesizer \- Synthesize and apply loop contracts of goto binaries.
4+
.SH SYNOPSIS
5+
.TP
6+
.B goto\-synthesizer [\-?] [\-h] [\-\-help]
7+
show help
8+
.TP
9+
.B goto\-synthesizer \-\-version
10+
show version and exit
11+
.TP
12+
.B goto\-synthesizer [options] \fIin\fR [\fIout\fR]
13+
perform synthesis and loop-contracts transformation
14+
.SH DESCRIPTION
15+
\fBgoto-synthesis\fR reads a GOTO binary, performs loop-contracts synthesis and
16+
program transformation for the synthesized contracts, and then writes the
17+
resulting program as GOTO binary on disk.
18+
.SH OPTIONS
19+
.SS "User-interface options:"
20+
.TP
21+
\fB\-\-xml\-ui\fR
22+
use XML\-formatted output
23+
.TP
24+
\fB\-\-json\-ui\fR
25+
use JSON\-formatted output
26+
.TP
27+
\fB\-\-verbosity\fR \fIn\fR
28+
verbosity level
29+
.SH ENVIRONMENT
30+
All tools honor the TMPDIR environment variable when generating temporary
31+
files and directories.
32+
.SH BUGS
33+
If you encounter a problem please create an issue at
34+
.B https://github.com/diffblue/cbmc/issues
35+
.SH SEE ALSO
36+
.BR cbmc (1),
37+
.BR goto-cc (1)
38+
.BR goto-instrument (1)
39+
.SH COPYRIGHT
40+
2022, Qinheping Hu

‎src/CMakeLists.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ add_subdirectory(goto-instrument)
117117
add_subdirectory(goto-analyzer)
118118
add_subdirectory(goto-diff)
119119
add_subdirectory(goto-harness)
120+
add_subdirectory(goto-synthesizer)
120121
add_subdirectory(symtab2gb)
121122

122123
if(UNIX OR WITH_MEMORY_ANALYZER)

‎src/Makefile‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ DIRS = analyses \
1414
goto-harness \
1515
goto-programs \
1616
goto-symex \
17+
goto-synthesizer \
1718
jsil \
1819
json \
1920
json-symtab-language \
@@ -36,6 +37,7 @@ all: cbmc.dir \
3637
goto-diff.dir \
3738
goto-instrument.dir \
3839
goto-harness.dir \
40+
goto-synthesizer.dir \
3941
symtab2gb.dir \
4042
# Empty last line
4143

@@ -104,6 +106,10 @@ memory-analyzer.dir: util.dir goto-programs.dir langapi.dir linking.dir \
104106
symtab2gb.dir: util.dir goto-programs.dir langapi.dir linking.dir \
105107
json.dir json-symtab-language.dir ansi-c.dir
106108

109+
goto-synthesizer.dir: languages util.dir goto-programs.dir langapi.dir \
110+
json.dir goto-checker.dir \
111+
goto-instrument.dir
112+
107113
# building for a particular directory
108114

109115
$(patsubst %, %.dir, $(DIRS)):
@@ -180,7 +186,7 @@ doc :
180186
install: all
181187
for b in \
182188
cbmc crangler \
183-
goto-analyzer goto-cc goto-diff goto-instrument goto-harness \
189+
goto-analyzer goto-cc goto-diff goto-instrument goto-harness goto-synthesizer \
184190
symtab2gb ; do \
185191
cp $$b/$$b $(PREFIX)/bin/ ; \
186192
cp ../doc/man/$$b.1 $(PREFIX)/doc/man/man1/ ; \

‎src/goto-synthesizer/CMakeLists.txt‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
# Library
2+
file(GLOB_RECURSE sources "*.cpp" "*.h")
3+
list(REMOVE_ITEM sources
4+
${CMAKE_CURRENT_SOURCE_DIR}/goto_synthesizer_main.cpp
5+
)
6+
add_library(goto-synthesizer-lib ${sources})
7+
8+
generic_includes(goto-synthesizer-lib)
9+
10+
target_link_libraries(goto-synthesizer-lib
11+
ansi-c
12+
cpp
13+
big-int
14+
goto-checker
15+
goto-instrument-lib
16+
goto-programs
17+
langapi
18+
util
19+
json
20+
)
21+
22+
# Executable
23+
add_executable(goto-synthesizer goto_synthesizer_main.cpp)
24+
target_link_libraries(goto-synthesizer goto-synthesizer-lib)
25+
install(TARGETS goto-synthesizer DESTINATION ${CMAKE_INSTALL_BINDIR})
26+
27+
# Man page
28+
if(NOT WIN32)
29+
install(
30+
DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/
31+
DESTINATION ${CMAKE_INSTALL_MANDIR}/man1
32+
FILES_MATCHING PATTERN "goto-synthesizer*")
33+
endif()

‎src/goto-synthesizer/Makefile‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
SRC = goto_synthesizer_languages.cpp \
2+
goto_synthesizer_main.cpp \
3+
goto_synthesizer_parse_options.cpp \
4+
# Empty last line
5+
6+
OBJ += ../ansi-c/ansi-c$(LIBEXT) \
7+
../cpp/cpp$(LIBEXT) \
8+
../linking/linking$(LIBEXT) \
9+
../big-int/big-int$(LIBEXT) \
10+
../goto-checker/goto-checker$(LIBEXT) \
11+
../goto-programs/goto-programs$(LIBEXT) \
12+
../langapi/langapi$(LIBEXT) \
13+
../util/util$(LIBEXT) \
14+
../json/json$(LIBEXT) \
15+
# Empty last line
16+
17+
INCLUDES= -I ..
18+
19+
LIBS =
20+
21+
CLEANFILES = goto-synthesizer$(EXEEXT) goto-synthesizer$(LIBEXT)
22+
23+
include ../config.inc
24+
include ../common
25+
26+
all: goto-synthesizer$(EXEEXT)
27+
28+
###############################################################################
29+
30+
goto-synthesizer$(EXEEXT): $(OBJ)
31+
$(LINKBIN)
32+
33+
.PHONY: goto-synthesizer-mac-signed
34+
35+
goto-synthesizer-mac-signed: goto-synthesizer$(EXEEXT)
36+
codesign -v -s $(OSX_IDENTITY) goto-synthesizer$(EXEEXT)

‎src/goto-synthesizer/README.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
\ingroup module_hidden
2+
\defgroup goto-synthesizer goto-synthesizer
3+
4+
# Folder goto-synthesizer
5+
6+
\author Qinheping Hu
7+
8+
The `goto-synthesizer/` contains all processing of loop-contracts synthesizer.

‎src/goto-synthesizer/goto_synthesizer_languages.cpp‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
/*******************************************************************\
2+
Module: Language Registration
3+
Author: Qinheping Hu
4+
\*******************************************************************/
5+
6+
/// \file
7+
/// Language Registration
8+
9+
#include <ansi-c/ansi_c_language.h>
10+
#include <cpp/cpp_language.h>
11+
#include <langapi/mode.h>
12+
13+
#include "goto_synthesizer_parse_options.h"
14+
15+
void goto_synthesizer_parse_optionst::register_languages()
16+
{
17+
register_language(new_ansi_c_language);
18+
register_language(new_cpp_language);
19+
}

‎src/goto-synthesizer/goto_synthesizer_main.cpp‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
/*******************************************************************\
2+
Module: Main Module
3+
Author: Qinheping Hu
4+
\*******************************************************************/
5+
6+
/// \file
7+
/// Main Module
8+
9+
#ifdef _MSC_VER
10+
# include <util/unicode.h>
11+
#endif
12+
13+
#include "goto_synthesizer_parse_options.h"
14+
15+
#ifdef _MSC_VER
16+
int wmain(int argc, const wchar_t **argv_wide)
17+
{
18+
auto vec = narrow_argv(argc, argv_wide);
19+
auto narrow = to_c_str_array(std::begin(vec), std::end(vec));
20+
auto argv = narrow.data();
21+
#else
22+
int main(int argc, const char **argv)
23+
{
24+
#endif
25+
goto_synthesizer_parse_optionst parse_options(argc, argv);
26+
return parse_options.main();
27+
}

0 commit comments

Comments
 (0)