Merge pull request diffblue#328 from diffblue/add-get-may-etc-as-irep-id

Turn get_may, set_may, etc into irep_ids
smowton · Jan 31, 2018 · 412dbb1 · 412dbb1
2 parents cba7ba8 + fa6282a
commit 412dbb1
Show file tree

Hide file tree

Showing 10 changed files with 50 additions and 47 deletions.
diff --git a/cbmc/src/analyses/custom_bitvector_analysis.cpp b/cbmc/src/analyses/custom_bitvector_analysis.cpp
@@ -319,10 +319,11 @@ void custom_bitvector_domaint::transform(
       {
         const irep_idt &identifier=to_symbol_expr(function).get_identifier();
 
-        if(identifier=="__CPROVER_set_must" ||
-           identifier=="__CPROVER_clear_must" ||
-           identifier=="__CPROVER_set_may" ||
-           identifier=="__CPROVER_clear_may")
+        if(
+          identifier == CPROVER_PREFIX "set_must" ||
+          identifier == CPROVER_PREFIX "clear_must" ||
+          identifier == CPROVER_PREFIX "set_may" ||
+          identifier == CPROVER_PREFIX "clear_may")
         {
           if(code_function_call.arguments().size()==2)
           {
@@ -331,13 +332,13 @@ void custom_bitvector_domaint::transform(
 
             modet mode;
 
-            if(identifier=="__CPROVER_set_must")
+            if(identifier == CPROVER_PREFIX "set_must")
               mode=modet::SET_MUST;
-            else if(identifier=="__CPROVER_clear_must")
+            else if(identifier == CPROVER_PREFIX "clear_must")
               mode=modet::CLEAR_MUST;
-            else if(identifier=="__CPROVER_set_may")
+            else if(identifier == CPROVER_PREFIX "set_may")
               mode=modet::SET_MAY;
-            else if(identifier=="__CPROVER_clear_may")
+            else if(identifier == CPROVER_PREFIX "clear_may")
               mode=modet::CLEAR_MAY;
             else
               UNREACHABLE;
@@ -459,13 +460,13 @@ void custom_bitvector_domaint::transform(
 
         modet mode;
 
-        if(statement=="set_must")
+        if(statement == ID_set_must)
           mode=modet::SET_MUST;
-        else if(statement=="clear_must")
+        else if(statement == ID_clear_must)
           mode=modet::CLEAR_MUST;
-        else if(statement=="set_may")
+        else if(statement == ID_set_may)
           mode=modet::SET_MAY;
-        else if(statement=="clear_may")
+        else if(statement == ID_clear_may)
           mode=modet::CLEAR_MAY;
         else
           UNREACHABLE;
@@ -664,8 +665,7 @@ void custom_bitvector_domaint::erase_blank_vectors(bitst &bits)
 
 bool custom_bitvector_domaint::has_get_must_or_may(const exprt &src)
 {
-  if(src.id()=="get_must" ||
-     src.id()=="get_may")
+  if(src.id() == ID_get_must || src.id() == ID_get_may)
     return true;
 
   forall_operands(it, src)
@@ -679,7 +679,7 @@ exprt custom_bitvector_domaint::eval(
   const exprt &src,
   custom_bitvector_analysist &custom_bitvector_analysis) const
 {
-  if(src.id()=="get_must" || src.id()=="get_may")
+  if(src.id() == ID_get_must || src.id() == ID_get_may)
   {
     if(src.operands().size()==2)
     {
@@ -694,15 +694,15 @@ exprt custom_bitvector_domaint::eval(
       if(pointer.is_constant() &&
          to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
       {
-        if(src.id()=="get_may")
+        if(src.id() == ID_get_may)
         {
           for(const auto &bit : may_bits)
             if(get_bit(bit.second, bit_nr))
               return true_exprt();
 
           return false_exprt();
         }
-        else if(src.id()=="get_must")
+        else if(src.id() == ID_get_must)
         {
           return false_exprt();
         }
@@ -716,9 +716,9 @@ exprt custom_bitvector_domaint::eval(
 
         bool value=false;
 
-        if(src.id()=="get_must")
+        if(src.id() == ID_get_must)
           value=get_bit(v.must_bits, bit_nr);
-        else if(src.id()=="get_may")
+        else if(src.id() == ID_get_may)
           value=get_bit(v.may_bits, bit_nr);
 
         if(value)

diff --git a/cbmc/src/ansi-c/c_typecheck_expr.cpp b/cbmc/src/ansi-c/c_typecheck_expr.cpp
@@ -2035,9 +2035,8 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_function_call_arguments(expr);
 
-    exprt get_must_expr=
-      binary_predicate_exprt(
-        expr.arguments()[0], "get_must", expr.arguments()[1]);
+    exprt get_must_expr = binary_predicate_exprt(
+      expr.arguments()[0], ID_get_must, expr.arguments()[1]);
     get_must_expr.add_source_location()=source_location;
 
     return get_must_expr;
@@ -2053,9 +2052,8 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_function_call_arguments(expr);
 
-    exprt get_may_expr=
-      binary_predicate_exprt(
-        expr.arguments()[0], "get_may", expr.arguments()[1]);
+    exprt get_may_expr = binary_predicate_exprt(
+      expr.arguments()[0], ID_get_may, expr.arguments()[1]);
     get_may_expr.add_source_location()=source_location;
 
     return get_may_expr;

diff --git a/cbmc/src/ansi-c/expr2c.cpp b/cbmc/src/ansi-c/expr2c.cpp
@@ -2929,8 +2929,7 @@ std::string expr2ct::convert_code(
   if(statement==ID_array_replace)
     return convert_code_array_replace(src, indent);
 
-  if(statement=="set_may" ||
-     statement=="set_must")
+  if(statement == ID_set_may || statement == ID_set_must)
     return
       indent_str(indent)+convert_function(src, id2string(statement), 16)+";";
 
@@ -3493,10 +3492,10 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_pointer_object)
     return convert_function(src, "POINTER_OBJECT", precedence=16);
 
-  else if(src.id()=="get_must")
+  else if(src.id() == ID_get_must)
     return convert_function(src, "__CPROVER_get_must", precedence=16);
 
-  else if(src.id()=="get_may")
+  else if(src.id() == ID_get_may)
     return convert_function(src, "__CPROVER_get_may", precedence=16);
 
   else if(src.id()=="object_value")

diff --git a/cbmc/src/goto-analyzer/taint_analysis.cpp b/cbmc/src/goto-analyzer/taint_analysis.cpp
@@ -159,7 +159,7 @@ void taint_analysist::instrument(
               {
               case taint_parse_treet::rulet::SOURCE:
                 {
-                  codet code_set_may("set_may");
+                  codet code_set_may(ID_set_may);
                   code_set_may.operands().resize(2);
                   code_set_may.op0()=where;
                   code_set_may.op1()=
@@ -173,7 +173,7 @@ void taint_analysist::instrument(
               case taint_parse_treet::rulet::SINK:
                 {
                   goto_programt::targett t=insert_before.add_instruction();
-                  binary_predicate_exprt get_may("get_may");
+                  binary_predicate_exprt get_may(ID_get_may);
                   get_may.op0()=where;
                   get_may.op1()=address_of_exprt(string_constantt(rule.taint));
                   t->make_assertion(not_exprt(get_may));
@@ -186,7 +186,7 @@ void taint_analysist::instrument(
 
               case taint_parse_treet::rulet::SANITIZER:
                 {
-                  codet code_clear_may("clear_may");
+                  codet code_clear_may(ID_clear_may);
                   code_clear_may.operands().resize(2);
                   code_clear_may.op0()=where;
                   code_clear_may.op1()=

diff --git a/cbmc/src/goto-instrument/thread_instrumentation.cpp b/cbmc/src/goto-instrument/thread_instrumentation.cpp
@@ -43,7 +43,7 @@ void thread_exit_instrumentation(goto_programt &goto_program)
   exprt mutex_locked_string=
     string_constantt("mutex-locked");
 
-  binary_exprt get_may("get_may");
+  binary_exprt get_may(ID_get_may);
 
   // NULL is any
   get_may.op0()=null_pointer_exprt(pointer_type(empty_typet()));
@@ -89,8 +89,8 @@ void mutex_init_instrumentation(
   goto_programt &goto_program,
   typet lock_type)
 {
-  symbol_tablet::symbolst::const_iterator f_it=
-    symbol_table.symbols.find("__CPROVER_set_must");
+  symbol_tablet::symbolst::const_iterator f_it =
+    symbol_table.symbols.find(CPROVER_PREFIX "set_must");
 
   if(f_it==symbol_table.symbols.end())
     return;

diff --git a/cbmc/src/goto-programs/goto_inline_class.cpp b/cbmc/src/goto-programs/goto_inline_class.cpp
@@ -720,12 +720,12 @@ const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive(
 bool goto_inlinet::is_ignored(const irep_idt id) const
 {
   return
-    id=="__CPROVER_cleanup" ||
-    id=="__CPROVER_set_must" ||
-    id=="__CPROVER_set_may" ||
-    id=="__CPROVER_clear_must" ||
-    id=="__CPROVER_clear_may" ||
-    id=="__CPROVER_cover";
+    id == CPROVER_PREFIX "cleanup" ||
+    id == CPROVER_PREFIX "set_must" ||
+    id == CPROVER_PREFIX "set_may" ||
+    id == CPROVER_PREFIX "clear_must" ||
+    id == CPROVER_PREFIX "clear_may" ||
+    id == CPROVER_PREFIX "cover";
 }
 
 bool goto_inlinet::check_inline_map(

diff --git a/cbmc/src/util/irep_ids.def b/cbmc/src/util/irep_ids.def
@@ -849,6 +849,12 @@ IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_ONE(lvsa_evs_type)
 IREP_ID_ONE(is_initializer)
 IREP_ID_TWO(C_is_taint_wrapper_type, #is_taint_wrapper_type)
+IREP_ID_ONE(get_may)
+IREP_ID_ONE(set_may)
+IREP_ID_ONE(clear_may)
+IREP_ID_ONE(get_must)
+IREP_ID_ONE(set_must)
+IREP_ID_ONE(clear_must)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO
diff --git a/src/pointer-analysis/local_value_set.cpp b/src/pointer-analysis/local_value_set.cpp
@@ -665,9 +665,9 @@ void local_value_sett::assign_rec(
 void local_value_sett::apply_code_rec(const codet &code, const namespacet &ns)
 {
   const irep_idt &statement = code.get_statement();
-  const bool set_may = statement == "set_may";
-  const bool get_may = statement == "get_may";
-  const bool clear_may = statement == "clear_may";
+  const bool set_may = statement == ID_set_may;
+  const bool get_may = statement == ID_get_may;
+  const bool clear_may = statement == ID_clear_may;
 
   if(statement == ID_dead)
   {

diff --git a/src/taint-analysis/taint_statistics.cpp b/src/taint-analysis/taint_statistics.cpp
@@ -375,9 +375,9 @@ void  taint_statisticst::end_goto_program_building(
           statistics_of_functions.at(as_string(name_fn.first));
       for(goto_programt::instructiont const&  I :
            name_fn.second.body.instructions)
-        if(I.type == OTHER && I.code.get_statement() == "set_may")
+        if(I.type == OTHER && I.code.get_statement() == ID_set_may)
           fn_stats.on_set_may(I.location_number);
-        else if(I.type == OTHER &&I.code.get_statement() == "clear_may")
+        else if(I.type == OTHER && I.code.get_statement() == ID_clear_may)
           fn_stats.on_clear_may(I.location_number);
     }
 

diff --git a/src/taint-analysis/taint_trace_recogniser.cpp b/src/taint-analysis/taint_trace_recogniser.cpp
@@ -306,7 +306,7 @@ static void  taint_collect_successors_inside_function(
 
 static exprt taint_find_expression_of_rule(exprt const&  expr)
 {
-  if(expr.id() == "get_may")
+  if(expr.id() == ID_get_may)
   {
     if (expr.operands().size() != 2UL)
       return exprt(ID_empty);