Skip to content

Commit ae74413

Browse files
tautschnigtautschnig
committed
Annotate loop unwinding bounds via pragma
Enable users to specify loop unwinding information directly in source code via `#pragma CPROVER unwind N` with some number `N`. This should be less susceptible to code changes than unwindsets that use loop numbers: those loop numbers may change when code outside the named loop is modified, e.g., when adding or removing other loops.
1 parent 6752c40 commit ae74413

File tree

7 files changed

+110
-20
lines changed

7 files changed

+110
-20
lines changed

‎regression/cbmc/pragma_cprover_loop1/main.c

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
int main()
2+
{
3+
#pragma CPROVER unwind 2
4+
for(int i = 0; i < 5; ++i)
5+
{
6+
if(i < 2)
7+
continue;
8+
9+
for(int j = 0; j < 10; ++j)
10+
++j;
11+
}
12+
13+
#pragma CPROVER unwind 1
14+
do
15+
{
16+
int x = 42;
17+
} while(0);
18+
19+
#pragma CPROVER unwind 10
20+
while(1)
21+
{
22+
int x = 42;
23+
}
24+
25+
__CPROVER_assert(0, "false");
26+
}

‎regression/cbmc/pragma_cprover_loop1/test.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+
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎src/ansi-c/ansi_c_parser.cpp

Lines changed: 32 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -188,21 +188,37 @@ void ansi_c_parsert::pragma_cprover_add_check(
188188
if(pragma_cprover_stack.empty())
189189
pragma_cprover_push();
190190

191-
pragma_cprover_stack.back()[name] = enabled;
191+
pragma_cprover_stack.back()[name] = enabled ? 1 : 0;
192+
}
193+
194+
void ansi_c_parsert::pragma_cprover_add_unwind(size_t bound)
195+
{
196+
if(pragma_cprover_stack.empty())
197+
pragma_cprover_push();
198+
199+
pragma_cprover_stack.back()["unwind"] = bound;
200+
}
201+
202+
void ansi_c_parsert::pragma_cprover_consume_unwind()
203+
{
204+
for(auto &map : pragma_cprover_stack)
205+
map.erase("unwind");
206+
207+
set_pragma_cprover();
192208
}
193209

194210
bool ansi_c_parsert::pragma_cprover_clash(const irep_idt &name, bool enabled)
195211
{
196212
auto top = pragma_cprover_stack.back();
197213
auto found = top.find(name);
198-
return found != top.end() && found->second != enabled;
214+
return found != top.end() && found->second != (enabled ? 1 : 0);
199215
}
200216

201217
void ansi_c_parsert::set_pragma_cprover()
202218
{
203219
// handle enable/disable shadowing
204220
// by bottom-to-top flattening
205-
std::map<irep_idt, bool> flattened;
221+
std::map<irep_idt, size_t> flattened;
206222

207223
for(const auto &pragma_set : pragma_cprover_stack)
208224
for(const auto &pragma : pragma_set)
@@ -212,9 +228,18 @@ void ansi_c_parsert::set_pragma_cprover()
212228

213229
for(const auto &pragma : flattened)
214230
{
215-
std::string check_name = id2string(pragma.first);
216-
std::string full_name =
217-
(pragma.second ? "enable:" : "disable:") + check_name;
218-
source_location.add_pragma(full_name);
231+
if(pragma.first == "unwind")
232+
{
233+
std::string unwind_info =
234+
id2string(pragma.first) + ":" + std::to_string(pragma.second);
235+
source_location.add_pragma(unwind_info);
236+
}
237+
else
238+
{
239+
std::string check_name = id2string(pragma.first);
240+
std::string full_name =
241+
(pragma.second == 1 ? "enable:" : "disable:") + check_name;
242+
source_location.add_pragma(full_name);
243+
}
219244
}
220245
}

‎src/ansi-c/ansi_c_parser.h

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,12 +153,18 @@ class ansi_c_parsert:public parsert
153153
/// is already present at top of the stack
154154
bool pragma_cprover_clash(const irep_idt &name, bool enabled);
155155

156+
/// \brief Adds an unwinding bound to the CPROVER pragma stack
157+
void pragma_cprover_add_unwind(size_t bound);
158+
159+
/// \brief Remove unwinding bounds from the CPROVER pragma stack
160+
void pragma_cprover_consume_unwind();
161+
156162
/// \brief Tags \ref source_location with
157163
/// the current CPROVER pragma stack
158164
void set_pragma_cprover();
159165

160166
private:
161-
std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
167+
std::list<std::map<const irep_idt, size_t>> pragma_cprover_stack;
162168
};
163169

164170
void ansi_c_scanner_init(ansi_c_parsert &);

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -415,6 +415,7 @@ void c_typecheck_baset::typecheck_expression(codet &code)
415415

416416
void c_typecheck_baset::typecheck_for(codet &code)
417417
{
418+
warning() << code.pretty() << eom;
418419
if(code.operands().size()!=4)
419420
{
420421
error().source_location = code.source_location();
@@ -771,6 +772,7 @@ void c_typecheck_baset::typecheck_switch(codet &code)
771772

772773
void c_typecheck_baset::typecheck_while(code_whilet &code)
773774
{
775+
warning() << code.pretty() << eom;
774776
if(code.operands().size()!=2)
775777
{
776778
error().source_location = code.source_location();
@@ -817,6 +819,7 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
817819

818820
void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
819821
{
822+
warning() << code.pretty() << eom;
820823
if(code.operands().size()!=2)
821824
{
822825
error().source_location = code.source_location();

‎src/ansi-c/parser.y

Lines changed: 19 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2495,25 +2495,31 @@ declaration_or_expression_statement:
24952495

24962496
iteration_statement:
24972497
TOK_WHILE '(' comma_expression_opt ')'
2498+
{
2499+
PARSER.pragma_cprover_consume_unwind();
2500+
}
24982501
cprover_contract_assigns_opt
24992502
cprover_contract_loop_invariant_list_opt
25002503
cprover_contract_decreases_opt
25012504
statement
25022505
{
25032506
$$=$1;
25042507
statement($$, ID_while);
2505-
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8)));
2506-
2507-
if(!parser_stack($5).operands().empty())
2508-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($5).operands());
2508+
parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($9)));
25092509

25102510
if(!parser_stack($6).operands().empty())
2511-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
2511+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($6).operands());
25122512

25132513
if(!parser_stack($7).operands().empty())
2514-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands());
2514+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($7).operands());
2515+
2516+
if(!parser_stack($8).operands().empty())
2517+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($8).operands());
25152518
}
25162519
| TOK_DO
2520+
{
2521+
PARSER.pragma_cprover_consume_unwind();
2522+
}
25172523
cprover_contract_assigns_opt
25182524
cprover_contract_loop_invariant_list_opt
25192525
cprover_contract_decreases_opt
@@ -2522,16 +2528,16 @@ iteration_statement:
25222528
{
25232529
$$=$1;
25242530
statement($$, ID_dowhile);
2525-
parser_stack($$).add_to_operands(std::move(parser_stack($8)), std::move(parser_stack($5)));
2526-
2527-
if(!parser_stack($2).operands().empty())
2528-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($2).operands());
2531+
parser_stack($$).add_to_operands(std::move(parser_stack($9)), std::move(parser_stack($6)));
25292532

25302533
if(!parser_stack($3).operands().empty())
2531-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($3).operands());
2534+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($3).operands());
25322535

25332536
if(!parser_stack($4).operands().empty())
2534-
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($4).operands());
2537+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($4).operands());
2538+
2539+
if(!parser_stack($5).operands().empty())
2540+
static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($5).operands());
25352541
}
25362542
| TOK_FOR
25372543
{
@@ -2541,6 +2547,7 @@ iteration_statement:
25412547
unsigned prefix=++PARSER.current_scope().compound_counter;
25422548
PARSER.new_scope(std::to_string(prefix)+"::");
25432549
}
2550+
PARSER.pragma_cprover_consume_unwind();
25442551
}
25452552
'(' declaration_or_expression_statement
25462553
comma_expression_opt ';'

‎src/ansi-c/scanner.l

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ static int isatty(int) { return 0; }
2929
#endif
3030

3131
#include <util/string_constant.h>
32+
#include <util/string2int.h>
3233
#include <util/unicode.h>
3334

3435
#include "preprocessor_line.h"
@@ -443,6 +444,20 @@ enable_or_disable ("enable"|"disable")
443444
PARSER.set_pragma_cprover();
444445
}
445446

447+
<CPROVER_PRAGMA>{ws}"unwind"{ws}{integer} {
448+
std::string tmp(yytext);
449+
std::string::size_type p = tmp.rfind('d') + 1;
450+
auto bound = string2optional_size_t(tmp.substr(p));
451+
if(!bound.has_value())
452+
{
453+
ansi_c_parser->parse_error(
454+
"Found invalid loop unwinding annotation " + tmp, "");
455+
return TOK_SCANNER_ERROR;
456+
}
457+
PARSER.pragma_cprover_add_unwind(*bound);
458+
PARSER.set_pragma_cprover();
459+
}
460+
446461
<CPROVER_PRAGMA>. {
447462
yyansi_cerror("Unsupported #pragma CPROVER");
448463
return TOK_SCANNER_ERROR;

0 commit comments

Comments
 (0)