From 1b7b347f034db0f208e029701a70876df84a81ef Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 16 May 2019 20:27:38 +0000 Subject: [PATCH] Make sure pragmas propagate to all source locations The previous fix would still fail for assignments with side effects as those expressions are broken up, and the inner assignment would not have had the pragma annotated. Instead, store the pragmas in the parser's source location, which is copied to all expressions. --- regression/cbmc/pragma_cprover2/main.c | 4 +- src/analyses/goto_check.cpp | 53 ++++++++++++-------------- src/ansi-c/ansi_c_parser.h | 13 ++++++- src/ansi-c/c_typecheck_code.cpp | 9 ----- src/ansi-c/c_typecheck_expr.cpp | 4 -- src/ansi-c/expr2c.cpp | 27 +++++++++++-- src/ansi-c/parser.y | 32 ---------------- src/ansi-c/scanner.l | 17 ++++----- src/util/irep_ids.def | 1 + src/util/source_location.h | 10 +++++ 10 files changed, 80 insertions(+), 90 deletions(-) diff --git a/regression/cbmc/pragma_cprover2/main.c b/regression/cbmc/pragma_cprover2/main.c index 14f1d8ee805..1a10fb48fa0 100644 --- a/regression/cbmc/pragma_cprover2/main.c +++ b/regression/cbmc/pragma_cprover2/main.c @@ -5,12 +5,12 @@ int foo(int x) int main() { - int n; + int m, n; #pragma CPROVER check push #pragma CPROVER check disable "signed-overflow" // do not generate assertions for the following statements - int x = n + n; + int x = m = n + n; ++n; n++; n += 1; diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 99a28ebfaad..7b1a9996359 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -29,7 +29,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -1805,35 +1804,31 @@ void goto_checkt::goto_check( goto_programt::instructiont &i=*it; flag_resett flag_resetter; - if(!i.source_location.get_comment().empty()) + const auto &pragmas = i.source_location.get_pragmas(); + for(const auto &d : pragmas) { - auto disabled_checks = split_string( - id2string(i.source_location.get_comment()), ',', true, true); - for(const auto &d : disabled_checks) - { - if(d == "disable:bounds-check") - flag_resetter.set_flag(enable_bounds_check, false); - else if(d == "disable:pointer-check") - flag_resetter.set_flag(enable_pointer_check, false); - else if(d == "disable:memory-leak-check") - flag_resetter.set_flag(enable_memory_leak_check, false); - else if(d == "disable:div-by-zero-check") - flag_resetter.set_flag(enable_div_by_zero_check, false); - else if(d == "disable:signed-overflow-check") - flag_resetter.set_flag(enable_signed_overflow_check, false); - else if(d == "disable:unsigned-overflow-check") - flag_resetter.set_flag(enable_unsigned_overflow_check, false); - else if(d == "disable:pointer-overflow-check") - flag_resetter.set_flag(enable_pointer_overflow_check, false); - else if(d == "disable:float-overflow-check") - flag_resetter.set_flag(enable_float_overflow_check, false); - else if(d == "disable:conversion-check") - flag_resetter.set_flag(enable_conversion_check, false); - else if(d == "disable:undefined-shift-check") - flag_resetter.set_flag(enable_undefined_shift_check, false); - else if(d == "disable:nan-check") - flag_resetter.set_flag(enable_nan_check, false); - } + if(d.first == "disable:bounds-check") + flag_resetter.set_flag(enable_bounds_check, false); + else if(d.first == "disable:pointer-check") + flag_resetter.set_flag(enable_pointer_check, false); + else if(d.first == "disable:memory-leak-check") + flag_resetter.set_flag(enable_memory_leak_check, false); + else if(d.first == "disable:div-by-zero-check") + flag_resetter.set_flag(enable_div_by_zero_check, false); + else if(d.first == "disable:signed-overflow-check") + flag_resetter.set_flag(enable_signed_overflow_check, false); + else if(d.first == "disable:unsigned-overflow-check") + flag_resetter.set_flag(enable_unsigned_overflow_check, false); + else if(d.first == "disable:pointer-overflow-check") + flag_resetter.set_flag(enable_pointer_overflow_check, false); + else if(d.first == "disable:float-overflow-check") + flag_resetter.set_flag(enable_float_overflow_check, false); + else if(d.first == "disable:conversion-check") + flag_resetter.set_flag(enable_conversion_check, false); + else if(d.first == "disable:undefined-shift-check") + flag_resetter.set_flag(enable_undefined_shift_check, false); + else if(d.first == "disable:nan-check") + flag_resetter.set_flag(enable_nan_check, false); } new_code.clear(); diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index b68fd6a80dd..a822c4ee32b 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANSI_C_ANSI_C_PARSER_H #include +#include #include #include @@ -69,7 +70,7 @@ class ansi_c_parsert:public parsert unsigned parenthesis_counter; std::string string_literal; std::list pragma_pack; - std::list pragma_cprover; + std::list> pragma_cprover; typedef configt::ansi_ct::flavourt modet; modet mode; @@ -145,6 +146,16 @@ class ansi_c_parsert:public parsert lookup(base_name, identifier, false, true); return identifier; } + + void set_pragma_cprover() + { + source_location.remove(ID_pragma); + for(const auto &pragma_set : pragma_cprover) + { + for(const auto &pragma : pragma_set) + source_location.add_pragma(pragma); + } + } }; extern ansi_c_parsert ansi_c_parser; diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index f8104ffb0cc..9e042a0bedd 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -243,16 +243,7 @@ void c_typecheck_baset::typecheck_decl(codet &code) } ansi_c_declarationt declaration; - irep_idt comment = code.source_location().get_comment(); declaration.swap(code.op0()); - if(!comment.empty()) - { - for(auto &d : declaration.declarators()) - { - if(d.source_location().get_comment().empty()) - d.add_source_location().set_comment(comment); - } - } if(declaration.get_is_static_assert()) { diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 3017ead4b1d..a753a5b5ffc 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2019,10 +2019,6 @@ void c_typecheck_baset::typecheck_side_effect_function_call( throw 0; } - irep_idt comment = expr.source_location().get_comment(); - if(!comment.empty() && f_op.source_location().get_comment().empty()) - f_op.add_source_location().set_comment(comment); - const code_typet &code_type=to_code_type(f_op.type()); expr.type()=code_type.return_type(); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index d42c6e8457f..549f2d1b97c 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -2796,11 +2797,31 @@ std::string expr2ct::convert_code( { static bool comment_done=false; - if(!comment_done && !src.source_location().get_comment().empty()) + if( + !comment_done && (!src.source_location().get_comment().empty() || + !src.source_location().get_pragmas().empty())) { comment_done=true; - std::string dest=indent_str(indent); - dest+="/* "+id2string(src.source_location().get_comment())+" */\n"; + std::string dest; + if(!src.source_location().get_comment().empty()) + { + dest += indent_str(indent); + dest += "/* " + id2string(src.source_location().get_comment()) + " */\n"; + } + if(!src.source_location().get_pragmas().empty()) + { + std::ostringstream oss; + oss << indent_str(indent) << "/* "; + const auto &pragmas = src.source_location().get_pragmas(); + join_strings( + oss, + pragmas.begin(), + pragmas.end(), + ',', + [](const std::pair &p) { return p.first; }); + oss << " */\n"; + dest += oss.str(); + } dest+=convert_code(src, indent); comment_done=false; return dest; diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 5e7a797d513..6b337cffe96 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -24,10 +24,6 @@ extern char *yyansi_ctext; #include "literals/convert_integer_literal.h" -#include - -#include - #include "ansi_c_y.tab.h" #ifdef _MSC_VER @@ -2310,38 +2306,10 @@ statement_list: statement { init($$); - if(!PARSER.pragma_cprover.empty()) - { - std::ostringstream oss; - join_strings( - oss, - PARSER.pragma_cprover.begin(), - PARSER.pragma_cprover.end(), - ','); - parser_stack($1).add_source_location().set_comment(oss.str()); - Forall_operands(it, parser_stack($1)) - { - it->add_source_location().set_comment(oss.str()); - } - } mto($$, $1); } | statement_list statement { - if(!PARSER.pragma_cprover.empty()) - { - std::ostringstream oss; - join_strings( - oss, - PARSER.pragma_cprover.begin(), - PARSER.pragma_cprover.end(), - ','); - parser_stack($2).add_source_location().set_comment(oss.str()); - Forall_operands(it, parser_stack($2)) - { - it->add_source_location().set_comment(oss.str()); - } - } mto($$, $2); } ; diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 091eefa1e1c..641682ca431 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -402,11 +402,14 @@ void ansi_c_scanner_init() /* CProver specific pragmas: hint to disable named checks */ {ws}"check"{ws}"push" { - PARSER.pragma_cprover.push_back(irep_idt{}); + PARSER.pragma_cprover.push_back({}); } {ws}"check"{ws}"pop" { if(!PARSER.pragma_cprover.empty()) + { PARSER.pragma_cprover.pop_back(); + PARSER.set_pragma_cprover(); + } } {ws}"check"{ws}"disable"{ws}{named_check} { std::string tmp(yytext); @@ -416,16 +419,10 @@ void ansi_c_scanner_init() std::string(tmp, p, tmp.size() - p - 1) + std::string("-check"); if(PARSER.pragma_cprover.empty()) - PARSER.pragma_cprover.push_back(value); + PARSER.pragma_cprover.push_back({value}); else - { - if(!PARSER.pragma_cprover.back().empty()) - { - value = - id2string(PARSER.pragma_cprover.back()) + "," + value; - } - PARSER.pragma_cprover.back() = value; - } + PARSER.pragma_cprover.back().insert(value); + PARSER.set_pragma_cprover(); } . { diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index b7b369e25c9..d615d9b4603 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -724,6 +724,7 @@ IREP_ID_ONE(clear_may) IREP_ID_ONE(get_must) IREP_ID_ONE(set_must) IREP_ID_ONE(clear_must) +IREP_ID_ONE(pragma) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree diff --git a/src/util/source_location.h b/src/util/source_location.h index d9800657bc9..3ce6e5762c3 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -192,6 +192,16 @@ class source_locationt:public irept optionalt full_path() const; + void add_pragma(const irep_idt &pragma) + { + add(ID_pragma).add(pragma); + } + + const irept::named_subt &get_pragmas() const + { + return find(ID_pragma).get_named_sub(); + } + protected: std::string as_string(bool print_cwd) const; };