Skip to content

Commit 8cdb2b7

Browse files
qinhepingqinheping
committed
goto-synthesizer: Separate front-end for loop-contracts synthesizer
1 parent fc535f5 commit 8cdb2b7

11 files changed

+268
-1
lines changed

‎CMakeLists.txt

+3
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>"
@@ -232,6 +233,8 @@ cprover_default_properties(
232233
goto-instrument-lib
233234
goto-programs
234235
goto-symex
236+
goto-synthesizer
237+
goto-synthesizer-lib
235238
jsil
236239
json
237240
json-symtab-language

‎src/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -116,6 +116,7 @@ add_subdirectory(goto-instrument)
116116
add_subdirectory(goto-analyzer)
117117
add_subdirectory(goto-diff)
118118
add_subdirectory(goto-harness)
119+
add_subdirectory(goto-synthesizer)
119120
add_subdirectory(symtab2gb)
120121

121122
if(UNIX OR WITH_MEMORY_ANALYZER)

‎src/Makefile

+7-1
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

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
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})

‎src/goto-synthesizer/Makefile

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

‎src/goto-synthesizer/README.md

+8
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

+19
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

+27
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+
}

‎src/goto-synthesizer/goto_synthesizer_parse_options.cpp

+88
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
/*******************************************************************\
2+
Module: Parse Options Module
3+
Author: Michael Tautschnig
4+
\*******************************************************************/
5+
6+
/// \file
7+
/// Main Module
8+
9+
#include "goto_synthesizer_parse_options.h"
10+
11+
#include <util/config.h>
12+
#include <util/exit_codes.h>
13+
#include <util/version.h>
14+
15+
#include <goto-programs/read_goto_binary.h>
16+
17+
#include <iostream>
18+
19+
/// invoke main modules
20+
int goto_synthesizer_parse_optionst::doit()
21+
{
22+
if(cmdline.isset("version"))
23+
{
24+
std::cout << CBMC_VERSION << '\n';
25+
return CPROVER_EXIT_SUCCESS;
26+
}
27+
28+
if(cmdline.args.size() != 1 && cmdline.args.size() != 2)
29+
{
30+
help();
31+
return CPROVER_EXIT_USAGE_ERROR;
32+
}
33+
34+
messaget::eval_verbosity(
35+
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
36+
37+
register_languages();
38+
39+
get_goto_program();
40+
41+
// TODO
42+
// Migrate synthesizer and tests from goto-instrument to goto-synthesizer
43+
44+
help();
45+
return CPROVER_EXIT_USAGE_ERROR;
46+
}
47+
48+
void goto_synthesizer_parse_optionst::get_goto_program()
49+
{
50+
log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
51+
<< messaget::eom;
52+
53+
config.set(cmdline);
54+
55+
auto result = read_goto_binary(cmdline.args[0], ui_message_handler);
56+
57+
if(!result.has_value())
58+
throw 0;
59+
60+
goto_model = std::move(result.value());
61+
62+
config.set_from_symbol_table(goto_model.symbol_table);
63+
}
64+
65+
/// display command line help
66+
void goto_synthesizer_parse_optionst::help()
67+
{
68+
// clang-format off
69+
std::cout << '\n' << banner_string("Goto-synthesizer", CBMC_VERSION) << '\n'
70+
<< align_center_with_border("Copyright (C) 2021") << '\n'
71+
<< align_center_with_border("Qinheping Hu") << '\n'
72+
<< align_center_with_border("[email protected]") << '\n'
73+
<<
74+
"\n"
75+
"Usage: Purpose:\n"
76+
"\n"
77+
" goto-synthesizer [-?] [-h] [--help] show help\n"
78+
" goto-synthesizer in out synthesize and apply loop invariants.\n" // NOLINT(*)
79+
"\n"
80+
"Main options:\n"
81+
"\n"
82+
"Other options:\n"
83+
" --version show version and exit\n"
84+
" --xml-ui use XML-formatted output\n"
85+
" --json-ui use JSON-formatted output\n"
86+
"\n";
87+
// clang-format on
88+
}

‎src/goto-synthesizer/goto_synthesizer_parse_options.h

+46
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
/*******************************************************************\
2+
Module: Command Line Parsing
3+
Author: Michael Tautschnig
4+
\*******************************************************************/
5+
6+
/// \file
7+
/// Command Line Parsing
8+
9+
#ifndef CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
10+
#define CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H
11+
12+
#include <util/parse_options.h>
13+
14+
#include <goto-programs/goto_model.h>
15+
16+
// clang-format off
17+
#define GOTO_SYNTHESIZER_OPTIONS \
18+
"(verbosity):(version)(xml-ui)(json-ui)" \
19+
// empty last line
20+
21+
// clang-format on
22+
23+
class goto_synthesizer_parse_optionst : public parse_options_baset
24+
{
25+
public:
26+
int doit() override;
27+
void help() override;
28+
29+
goto_synthesizer_parse_optionst(int argc, const char **argv)
30+
: parse_options_baset(
31+
GOTO_SYNTHESIZER_OPTIONS,
32+
argc,
33+
argv,
34+
"goto-synthesizer")
35+
{
36+
}
37+
38+
protected:
39+
void register_languages() override;
40+
41+
void get_goto_program();
42+
43+
goto_modelt goto_model;
44+
};
45+
46+
#endif // CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H

‎src/goto-synthesizer/module_dependencies.txt

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
ansi-c
2+
cpp
3+
goto-checker
4+
goto-instrument
5+
goto-programs
6+
langapi
7+
util

0 commit comments

Comments
 (0)