Skip to content

Commit 6ce1a40

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. Changes included in this PR: - Fixed non-c-standard output produced by `expr2c` - Fixed the bugs that Crangler removes space in the annotated loop contracts.
1 parent 48e1063 commit 6ce1a40

File tree

15 files changed

+290
-30
lines changed

15 files changed

+290
-30
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 true\", \"loop 1 assigns result\,i\"\, \"loop 3 invariant true\"\, \"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
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/ansi-c/expr2c.cpp

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@ expr2c_configurationt expr2c_configurationt::default_configuration
4242
true,
4343
true,
4444
true,
45-
"TRUE",
46-
"FALSE",
45+
"true",
46+
"false",
4747
true,
4848
false,
4949
false
@@ -4012,9 +4012,10 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
40124012
{ID_isinf, "isinf"},
40134013
{ID_isnan, "isnan"},
40144014
{ID_isnormal, "isnormal"},
4015-
{ID_object_size, "OBJECT_SIZE"},
4016-
{ID_pointer_object, "POINTER_OBJECT"},
4017-
{ID_pointer_offset, "POINTER_OFFSET"},
4015+
{ID_object_size, CPROVER_PREFIX "OBJECT_SIZE"},
4016+
{ID_pointer_object, CPROVER_PREFIX "POINTER_OBJECT"},
4017+
{ID_pointer_offset, CPROVER_PREFIX "POINTER_OFFSET"},
4018+
{ID_loop_entry, CPROVER_PREFIX "loop_entry"},
40184019
{ID_saturating_minus, CPROVER_PREFIX "saturating_minus"},
40194020
{ID_saturating_plus, CPROVER_PREFIX "saturating_plus"},
40204021
{ID_r_ok, "R_OK"},

‎src/crangler/c_wrangler.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -486,19 +486,17 @@ static void mangle_function(
486486

487487
if(!assigns.empty())
488488
{
489-
out << ' ' << CPROVER_PREFIX << "assigns(" << defines(assigns) << ')';
489+
out << ' ' << CPROVER_PREFIX << "assigns(" << assigns << ')';
490490
}
491491

492492
if(!invariant.empty())
493493
{
494-
out << ' ' << CPROVER_PREFIX << "loop_invariant("
495-
<< defines(invariant) << ')';
494+
out << ' ' << CPROVER_PREFIX << "loop_invariant(" << invariant << ')';
496495
}
497496

498497
if(!decreases.empty())
499498
{
500-
out << ' ' << CPROVER_PREFIX << "decreases(" << defines(decreases)
501-
<< ')';
499+
out << ' ' << CPROVER_PREFIX << "decreases(" << decreases << ')';
502500
}
503501
}
504502
}

‎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: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
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 " + expr2c(simplify_expr(invariant_entry.second, ns), ns);
80+
loop_contracts_array.push_back(json_stringt(inv_string));
81+
82+
// Adding loop assigns
83+
const auto it_assigns = assigns_map.find(invariant_entry.first);
84+
if(it_assigns != assigns_map.end())
85+
{
86+
std::string assign_string =
87+
"loop " + std::to_string(invariant_entry.first.loop_number + 1) +
88+
" assigns ";
89+
90+
bool in_fisrt_iter = true;
91+
for(const auto &a : it_assigns->second)
92+
{
93+
if(!in_fisrt_iter)
94+
{
95+
assign_string += ",";
96+
}
97+
else
98+
{
99+
in_fisrt_iter = false;
100+
}
101+
assign_string += expr2c(simplify_expr(a, ns), ns);
102+
}
103+
loop_contracts_array.push_back(json_stringt(assign_string));
104+
}
105+
}
106+
107+
json_stream_objectt json_stream(out);
108+
json_stream.push_back("sources", json_sources);
109+
110+
// Initialize functions object.
111+
json_arrayt json_functions;
112+
json_objectt json_functions_object;
113+
for(const auto &loop_contracts : function_map)
114+
{
115+
json_functions_object[loop_contracts.first] = loop_contracts.second;
116+
}
117+
json_functions.push_back(json_functions_object);
118+
json_stream.push_back("functions", json_functions);
119+
120+
// Destination of the Crangler output.
121+
json_stringt json_output(json_output_str);
122+
json_stream.push_back("output", json_output);
123+
}

‎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
}

0 commit comments

Comments
 (0)