Skip to content

Commit 531e768

Browse files
qinhepingqinheping
committed
Add dump-loop-contracts into loop-contracts synthesizer
Running the loop-contracts synthesizer with the flag `dump-loop-contracts` will output the synthesized contracts as a JSON file, which can be used to annotate back to the source code with Crangler.
1 parent d8b1c77 commit 531e768

File tree

13 files changed

+292
-20
lines changed

13 files changed

+292
-20
lines changed

‎doc/man/goto-synthesizer.1

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,12 @@ perform synthesis and loop-contracts transformation
1616
program transformation for the synthesized contracts, and then writes the
1717
resulting program as GOTO binary on disk.
1818
.SH OPTIONS
19+
.TP
20+
\fB\-\-dump\-loop\-contracts
21+
Dump the synthesized loop contracts as JSON.
22+
.TP
23+
\fB\-\-json-\output\fR \fIfile\fR
24+
Specify the output destination of the loop-contracts JSON.
1925
.SS "User-interface options:"
2026
.TP
2127
\fB\-\-xml\-ui\fR

‎regression/goto-synthesizer/chain.sh

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,10 @@ args=${*:6:$#-6}
1515
if [[ "$args" != *" _ "* ]]
1616
then
1717
args_inst=$args
18-
args_cbmc=""
18+
args_synthesizer=""
1919
else
2020
args_inst="${args%%" _ "*}"
21-
args_cbmc="${args#*" _ "}"
21+
args_synthesizer="${args#*" _ "}"
2222
fi
2323

2424
if [[ "${is_windows}" == "true" ]]; then
@@ -45,6 +45,10 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
4545
rm "${name}-mod.c"
4646
fi
4747
echo "Running goto-synthesizer: "
48-
$goto_synthesizer "${name}-mod.gb" "${name}-mod-2.gb"
49-
echo "Running CBMC: "
50-
$cbmc "${name}-mod-2.gb" ${args_cbmc}
48+
if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
49+
$goto_synthesizer ${args_synthesizer} "${name}-mod.gb"
50+
else
51+
$goto_synthesizer "${name}-mod.gb" "${name}-mod-2.gb"
52+
echo "Running CBMC: "
53+
$cbmc "${name}-mod-2.gb"
54+
fi

‎regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--pointer-check _ --dump-loop-contracts --json-output main.c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\"sources"\: \[ \"main\.c\" \]
7+
\"main\"\: \[ \"loop 1 invariant 1\", \"loop 1 assigns result\,i\"\, \"loop 3 invariant 1\"\, \"loop 3 assigns result\,i\" \]
8+
\"output\"\: \"main\.c\"
9+
--
10+
This test case checks if synthesized contracts are correctly dumped.

‎regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check _ --dump-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\"sources"\: \[ \"main\.c\" \]
7+
\"main\"\: \[ \"loop 1 invariant i \>\= 80u \|\| \_\_CPROVER\_POINTER\_OFFSET\(array\)
8+
--
9+
This test case checks if synthesized contracts are correctly dumped.

‎regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check _ --dump-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\"sources"\: \[ \"main\.c\" \]
7+
\"main\"\: \[ \"loop 1 invariant array \=\= end
8+
--
9+
This test case checks if synthesized contracts are correctly dumped.

‎regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--pointer-check _ --dump-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\"sources"\: \[ \"main\.c\" \]
7+
i \=\= .*j.*loop 1 assigns
8+
--
9+
This test case checks if synthesized contracts are correctly dumped.

‎regression/goto-synthesizer/loop_contracts_synthesis_05/test_dump.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--pointer-check _ --dump-loop-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
assigns \_\_CPROVER\_POINTER\_OBJECT\(b\-\>data\)
7+
--
8+
This test case checks if synthesized contracts are correctly dumped.

‎src/goto-synthesizer/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
SRC = cegis_verifier.cpp \
2+
dump_loop_contracts.cpp \
23
enumerative_loop_contracts_synthesizer.cpp \
34
expr_enumerator.cpp \
45
goto_synthesizer_languages.cpp \

‎src/goto-synthesizer/dump_loop_contracts.cpp

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,128 @@
1+
/*******************************************************************\
2+
3+
Module: Dump Loop Contracts as JSON
4+
5+
Author: Qinheping Hu, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Dump Loop Contracts as JSON
11+
12+
#include "dump_loop_contracts.h"
13+
14+
#include <util/json_stream.h>
15+
#include <util/simplify_expr.h>
16+
17+
#include <ansi-c/expr2c.h>
18+
19+
void dump_loop_contracts(
20+
goto_modelt &goto_model,
21+
const std::map<loop_idt, exprt> &invariant_map,
22+
const std::map<loop_idt, std::set<exprt>> &assigns_map,
23+
const std::string &json_output_str,
24+
std::ostream &out)
25+
{
26+
// {
27+
// "source" : [SOURCE_NAME_ARRAY],
28+
// "functions" : [{
29+
// FUN_NAME_1 : [LOOP_CONTRACTS_ARRAY],
30+
// FUN_NAME_2 : [LOOP_CONTRACTS_ARRAY],
31+
// ...
32+
// }],
33+
// "output" : OUTPUT
34+
// }
35+
36+
INVARIANT(!invariant_map.empty(), "No synthesized loop contracts to dump");
37+
38+
namespacet ns(goto_model.symbol_table);
39+
40+
// Set of names of source files.
41+
std::set<std::string> sources_set;
42+
43+
// Map from function name to LOOP_CONTRACTS_ARRAY json array of the function.
44+
std::map<std::string, json_arrayt> function_map;
45+
46+
json_arrayt json_sources;
47+
48+
for(const auto &invariant_entry : invariant_map)
49+
{
50+
const auto head = get_loop_head(
51+
invariant_entry.first.loop_number,
52+
goto_model.goto_functions
53+
.function_map[invariant_entry.first.function_id]);
54+
55+
const auto source_file = id2string(head->source_location().get_file());
56+
// Add source files.
57+
if(sources_set.insert(source_file).second)
58+
json_sources.push_back(json_stringt(source_file));
59+
60+
// Get the LOOP_CONTRACTS_ARRAY for the function from the map.
61+
auto it_function =
62+
function_map.find(id2string(head->source_location().get_function()));
63+
if(it_function == function_map.end())
64+
{
65+
std::string function_name =
66+
id2string(head->source_location().get_function());
67+
68+
// New LOOP_CONTRACTS_ARRAY
69+
json_arrayt loop_contracts_array;
70+
it_function =
71+
function_map.emplace(function_name, loop_contracts_array).first;
72+
}
73+
json_arrayt &loop_contracts_array = it_function->second;
74+
75+
// Adding loop invariants
76+
// The loop number in Crangler is 1-indexed instead of 0-indexed.
77+
std::string inv_string =
78+
"loop " + std::to_string(invariant_entry.first.loop_number + 1) +
79+
" invariant " +
80+
expr2c(
81+
simplify_expr(invariant_entry.second, ns),
82+
ns,
83+
expr2c_configurationt::clean_configuration);
84+
loop_contracts_array.push_back(json_stringt(inv_string));
85+
86+
// Adding loop assigns
87+
const auto it_assigns = assigns_map.find(invariant_entry.first);
88+
if(it_assigns != assigns_map.end())
89+
{
90+
std::string assign_string =
91+
"loop " + std::to_string(invariant_entry.first.loop_number + 1) +
92+
" assigns ";
93+
94+
bool in_fisrt_iter = true;
95+
for(const auto &a : it_assigns->second)
96+
{
97+
if(!in_fisrt_iter)
98+
{
99+
assign_string += ",";
100+
}
101+
else
102+
{
103+
in_fisrt_iter = false;
104+
}
105+
assign_string += expr2c(
106+
simplify_expr(a, ns), ns, expr2c_configurationt::clean_configuration);
107+
}
108+
loop_contracts_array.push_back(json_stringt(assign_string));
109+
}
110+
}
111+
112+
json_stream_objectt json_stream(out);
113+
json_stream.push_back("sources", json_sources);
114+
115+
// Initialize functions object.
116+
json_arrayt json_functions;
117+
json_objectt json_functions_object;
118+
for(const auto &loop_contracts : function_map)
119+
{
120+
json_functions_object[loop_contracts.first] = loop_contracts.second;
121+
}
122+
json_functions.push_back(json_functions_object);
123+
json_stream.push_back("functions", json_functions);
124+
125+
// Destination of the Crangler output.
126+
json_stringt json_output(json_output_str);
127+
json_stream.push_back("output", json_output);
128+
}

‎src/goto-synthesizer/dump_loop_contracts.h

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
/*******************************************************************\
2+
3+
Module: Dump Loop Contracts as JSON
4+
5+
Author: Qinheping Hu, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Dump Loop Contracts as JSON
11+
12+
#ifndef CPROVER_GOTO_SYNTHESIZER_DUMP_LOOP_CONTRACTS_H
13+
#define CPROVER_GOTO_SYNTHESIZER_DUMP_LOOP_CONTRACTS_H
14+
15+
#include "synthesizer_utils.h"
16+
17+
#include <iosfwd>
18+
#include <string>
19+
20+
void dump_loop_contracts(
21+
goto_modelt &goto_model,
22+
const std::map<loop_idt, exprt> &invariant_map,
23+
const std::map<loop_idt, std::set<exprt>> &assigns_map,
24+
const std::string &json_output_str,
25+
std::ostream &out);
26+
27+
#define OPT_DUMP_LOOP_CONTRACTS "(json-output):(dump-loop-contracts)"
28+
29+
// clang-format off
30+
#define HELP_DUMP_LOOP_CONTRACTS \
31+
" --dump-loop-contracts dump synthesized loop contracts as JSON\n" /* NOLINT(whitespace/line_length) */ \
32+
" --json-output <file> specify the output destination of the dumped loop contracts\n" // NOLINT(*)
33+
34+
// clang-format on
35+
36+
#endif // CPROVER_GOTO_SYNTHESIZER_DUMP_LOOP_CONTRACTS_H

‎src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -424,8 +424,8 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
424424
return_cex = verifier.verify();
425425
}
426426

427-
log.result() << "result : " << log.green << "PASS" << messaget::eom
428-
<< log.reset;
427+
log.result() << "result : " << log.green << "PASS" << log.reset
428+
<< messaget::eom;
429429

430430
return combined_invariant;
431431
}

‎src/goto-synthesizer/goto_synthesizer_parse_options.cpp

Lines changed: 62 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,13 @@ Author: Qinheping Hu
2121

2222
#include "enumerative_loop_contracts_synthesizer.h"
2323

24+
#include <fstream>
2425
#include <iostream>
2526

27+
#ifdef _MSC_VER
28+
# include <util/unicode.h>
29+
#endif
30+
2631
/// invoke main modules
2732
int goto_synthesizer_parse_optionst::doit()
2833
{
@@ -47,22 +52,65 @@ int goto_synthesizer_parse_optionst::doit()
4752
if(result_get_goto_program != CPROVER_EXIT_SUCCESS)
4853
return result_get_goto_program;
4954

50-
// TODO
51-
// Migrate synthesizer and tests from goto-instrument to goto-synthesizer
55+
// Synthesize loop invariants and annotate them into `goto_model`
56+
enumerative_loop_contracts_synthesizert synthesizer(goto_model, log);
57+
const auto &invariant_map = synthesizer.synthesize_all();
58+
const auto &assigns_map = synthesizer.get_assigns_map();
5259

60+
if(cmdline.isset("dump-loop-contracts"))
5361
{
54-
// Synthesize loop invariants and annotate them into `goto_model`
55-
enumerative_loop_contracts_synthesizert synthesizer(goto_model, log);
56-
annotate_invariants(synthesizer.synthesize_all(), goto_model);
57-
annotate_assigns(synthesizer.get_assigns_map(), goto_model);
58-
59-
// Apply loop contracts.
60-
std::set<std::string> to_exclude_from_nondet_static(
61-
cmdline.get_values("nondet-static-exclude").begin(),
62-
cmdline.get_values("nondet-static-exclude").end());
63-
code_contractst contracts(goto_model, log);
64-
contracts.apply_loop_contracts(to_exclude_from_nondet_static);
62+
// Default output destination is stdout.
63+
// Crangler will print the result to screen when the output destination
64+
// is "stdout".
65+
std::string json_output_str = "stdout";
66+
if(cmdline.isset("json-output"))
67+
{
68+
json_output_str = cmdline.get_value("json-output");
69+
}
70+
71+
namespacet ns(goto_model.symbol_table);
72+
// Output file specified
73+
if(cmdline.args.size() == 2)
74+
{
75+
#ifdef _MSC_VER
76+
std::ofstream out(widen(cmdline.args[1]));
77+
#else
78+
std::ofstream out(cmdline.args[1]);
79+
#endif
80+
if(!out)
81+
{
82+
log.error() << "failed to write to '" << cmdline.args[1] << "'";
83+
return CPROVER_EXIT_CONVERSION_FAILED;
84+
}
85+
dump_loop_contracts(
86+
goto_model, invariant_map, assigns_map, json_output_str, out);
87+
}
88+
// No output file specified. Print synthesized contracts with std::cout
89+
else
90+
{
91+
dump_loop_contracts(
92+
goto_model, invariant_map, assigns_map, json_output_str, std::cout);
93+
}
94+
95+
return CPROVER_EXIT_SUCCESS;
6596
}
97+
else if(cmdline.isset("json-output"))
98+
{
99+
throw invalid_command_line_argument_exceptiont(
100+
"Incompatible option detected",
101+
"--json-output must be used with --dump-loop-contracts");
102+
}
103+
104+
// Annotate loop contracts.
105+
annotate_invariants(invariant_map, goto_model);
106+
annotate_assigns(assigns_map, goto_model);
107+
108+
// Apply loop contracts.
109+
std::set<std::string> to_exclude_from_nondet_static(
110+
cmdline.get_values("nondet-static-exclude").begin(),
111+
cmdline.get_values("nondet-static-exclude").end());
112+
code_contractst contracts(goto_model, log);
113+
contracts.apply_loop_contracts(to_exclude_from_nondet_static);
66114

67115
// recalculate numbers, etc.
68116
goto_model.goto_functions.update();
@@ -134,6 +182,7 @@ void goto_synthesizer_parse_optionst::help()
134182
" goto-synthesizer in out synthesize and apply loop invariants.\n" // NOLINT(*)
135183
"\n"
136184
"Main options:\n"
185+
HELP_DUMP_LOOP_CONTRACTS
137186
"\n"
138187
"Other options:\n"
139188
" --version show version and exit\n"

‎src/goto-synthesizer/goto_synthesizer_parse_options.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,11 @@ Author: Qinheping Hu
1313

1414
#include <goto-programs/goto_model.h>
1515

16+
#include "dump_loop_contracts.h"
17+
1618
// clang-format off
1719
#define GOTO_SYNTHESIZER_OPTIONS \
20+
OPT_DUMP_LOOP_CONTRACTS \
1821
"(verbosity):(version)(xml-ui)(json-ui)" \
1922
// empty last line
2023

0 commit comments

Comments
 (0)