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

0 commit comments

Comments
 (0)