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.

Author: tautschnig

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;

src/analyses/goto_check.cpp

@@ -29,7 +29,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
-#include <util/string_utils.h>
 
 #include <langapi/language.h>
 #include <langapi/mode.h>
@@ -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();

src/ansi-c/ansi_c_parser.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANSI_C_ANSI_C_PARSER_H
 
 #include <cassert>
+#include <set>
 
 #include <util/parser.h>
 #include <util/expr.h>
@@ -69,7 +70,7 @@ class ansi_c_parsert:public parsert
   unsigned parenthesis_counter;
   std::string string_literal;
   std::list<exprt> pragma_pack;
-  std::list<irep_idt> pragma_cprover;
+  std::list<std::set<irep_idt>> 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;

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())
   {

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();

src/ansi-c/expr2c.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/string_constant.h>
+#include <util/string_utils.h>
 #include <util/suffix.h>
 #include <util/symbol.h>
 
@@ -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<irep_idt, irept> &p) { return p.first; });
+      oss << " */\n";
+      dest += oss.str();
+    }
     dest+=convert_code(src, indent);
     comment_done=false;
     return dest;

src/ansi-c/parser.y

@@ -24,10 +24,6 @@ extern char *yyansi_ctext;
 
 #include "literals/convert_integer_literal.h"
 
-#include <util/string_utils.h>
-
-#include <sstream>
-
 #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);
         }
         ;

src/ansi-c/scanner.l

@@ -402,11 +402,14 @@ void ansi_c_scanner_init()
 
                 /* CProver specific pragmas: hint to disable named checks */
 <CPROVER_PRAGMA>{ws}"check"{ws}"push" {
-                  PARSER.pragma_cprover.push_back(irep_idt{});
+                  PARSER.pragma_cprover.push_back({});
                 }
 <CPROVER_PRAGMA>{ws}"check"{ws}"pop" {
                   if(!PARSER.pragma_cprover.empty())
+                  {
                     PARSER.pragma_cprover.pop_back();
+                    PARSER.set_pragma_cprover();
+                  }
                 }
 <CPROVER_PRAGMA>{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();
                 }
 
 <CPROVER_PRAGMA>. {

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

src/util/source_location.h

@@ -192,6 +192,16 @@ class source_locationt:public irept
 
   optionalt<std::string> 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;
 };