SEC-533: Switching type of shadow vars from bool to c_bool. (diffblue#488)

Switching type of shadow vars from bool to c_bool.

Author: marek-trtik

src/taint-slicer/instrumenter.cpp

@@ -16,6 +16,30 @@
 #include <util/arith_tools.h>
 #include <util/pointer_offset_size.h>
 #include <util/msgstream.h>
+#include <util/std_expr.h>
+
+const c_bool_typet &get_shadow_variable_type()
+{
+  static c_bool_typet type(8);
+  return type;
+}
+
+const irep_idt &get_shadow_variable_type_id()
+{
+  return ID_c_bool;
+}
+
+const constant_exprt &get_shadow_variable_value_true()
+{
+  static constant_exprt value = from_integer(1, get_shadow_variable_type());
+  return value;
+}
+
+const constant_exprt &get_shadow_variable_value_false()
+{
+  static constant_exprt value = from_integer(0, get_shadow_variable_type());
+  return value;
+}
 
 const std::string &taint_prefix_of_instrumented_variable()
 {
@@ -132,10 +156,10 @@ exprt make_or_update_initialiser(
   {
     if(names_of_shadow_variables.count(as_string(component.get_name()))!=0UL)
     {
-      INVARIANT(component.type().id()==ID_bool,
+      INVARIANT(
+        component.type().id()==get_shadow_variable_type_id(),
         "Shadow variables must be bool-typed.");
-      fixed_initialiser.copy_to_operands(
-        constant_exprt(ID_false, bool_typet()));
+      fixed_initialiser.copy_to_operands(get_shadow_variable_value_false());
     }
     else
     {
@@ -188,14 +212,12 @@ static void get_access_paths_to_shadow_vars(
   const struct_typet struc=to_struct_type(expr.type());
   for(const struct_union_typet::componentt &member : struc.components())
   {
-    if(member.type().id()==ID_bool)
+    if(member.type().id() == get_shadow_variable_type_id())
     {
       if(names_of_shadow_variables.count(as_string(member.get_name()))!=0UL)
       {
-        access_paths.insert(member_exprt(
-          expr,
-          member.get_name(),
-          bool_typet()));
+        access_paths.insert(
+          member_exprt(expr, member.get_name(), get_shadow_variable_type()));
       }
     }
     else if(member.type().id()==ID_struct)
@@ -438,13 +460,15 @@ exprt taint_instrumentert::drive_access_path_through_super_classes(
             component.get_name())
           )
         {
-          struct_expr.operands().push_back(member_exprt(
-            uncast_access_path, component.get_name(), bool_typet()));
+          struct_expr.operands().push_back(
+            member_exprt(
+              uncast_access_path,
+              component.get_name(),
+              get_shadow_variable_type()));
         }
         else
         {
-          struct_expr.operands().push_back(
-            constant_exprt(ID_false, bool_typet()));
+          struct_expr.operands().push_back(get_shadow_variable_value_false());
         }
       }
     }
@@ -573,9 +597,8 @@ void taint_instrumentert::instrument_instructions_with_shadow_variables(
               for(const exprt &access_path : access_paths)
               {
                 auto iit=instrumentation_code.add_instruction(ASSIGN);
-                iit->code=code_assignt(
-                  access_path,
-                  constant_exprt(ID_false, typet(ID_bool)));
+                iit->code =
+                  code_assignt(access_path, get_shadow_variable_value_false());
                 iit->function=instr_it->function;
               }
 
@@ -667,7 +690,8 @@ void taint_instrumentert::instrument_instructions_with_shadow_variables(
             if(shadows.count(as_string(component.get_name())))
             {
               member_exprt shadow_member(code_decl.symbol(), component);
-              code_assignt init_member(shadow_member, false_exprt());
+              code_assignt init_member(
+                shadow_member, get_shadow_variable_value_false());
               auto new_instruction=
                 program_to_be_instrumented.insert_after(instr_it);
               new_instruction->make_assignment(init_member);
@@ -843,8 +867,8 @@ void taint_instrumentert::run()
     for(const auto &tid_var : from_tokens_to_vars)
     {
       symbolt symbol;
-      symbol.type=typet(ID_bool);
-      symbol.value=constant_exprt(ID_false, typet(ID_bool));
+      symbol.type = get_shadow_variable_type();
+      symbol.value = get_shadow_variable_value_false();
       symbol.location=source_locationt();
       symbol.name=tid_var.second;
       symbol.module="";
@@ -936,7 +960,7 @@ void taint_instrumentert::instrument_data_types(
       components.push_back(base_component);
       for(const auto &var : vars)
       {
-        struct_typet::componentt component(var, bool_typet());
+        struct_typet::componentt component(var, get_shadow_variable_type());
         component.set_base_name(var);
         component.set_pretty_name(var);
         components.push_back(component);
@@ -981,7 +1005,8 @@ void taint_instrumentert::instrument_data_types(
       {
         if(!struct_type.has_component(var))
         {
-          components.push_back(struct_typet::componentt{var, bool_typet()});
+          components.push_back(
+            struct_typet::componentt{var, get_shadow_variable_type()});
           components.back().set_pretty_name(var);
           components.back().set_access(ID_public);
         }
@@ -1061,8 +1086,8 @@ static exprt make_accessor_expression_to_shadow_variable(
     const struct_typet &struct_type = to_struct_type(type);
     if(struct_type.has_component(shadow_variable_name))
     {
-      access_path =
-        member_exprt(access_path, shadow_variable_name, bool_typet());
+      access_path = member_exprt(
+        access_path, shadow_variable_name, get_shadow_variable_type());
       break;
     }
     const struct_typet::componentst &components = struct_type.components();
@@ -1126,10 +1151,12 @@ void taint_instrumentert::instrument_location(
           fn_call,
           assumption.get_argidx(),
           instrumented_symbol_table);
-      const exprt proposition = make_accessor_expression_to_shadow_variable(
-        acc_path,
-        from_tokens_to_vars.at(assumption.get_token_name()),
-        instrumented_symbol_table);
+      const exprt proposition = equal_exprt(
+        make_accessor_expression_to_shadow_variable(
+          acc_path,
+          from_tokens_to_vars.at(assumption.get_token_name()),
+          instrumented_symbol_table),
+        get_shadow_variable_value_true());
       conjuncts.push_back(proposition);
     }
     auto iit=instrumentation_code.add_instruction();
@@ -1143,10 +1170,10 @@ void taint_instrumentert::instrument_location(
   {
     static void make_assignments_to_shadow_variables(
       const std::vector<argidx_and_tokennamet> &args_and_tokens,
-      const irep_idt bool_state_name,
+      const constant_exprt &bool_value,
       const symbol_tablet &symbol_table,
-      const std::map<taint_tokent::namet, automaton_variable_idt> &
-        from_tokens_to_vars,
+      const std::map<taint_tokent::namet, automaton_variable_idt>
+        &from_tokens_to_vars,
       const code_function_callt &fn_call,
       const irep_idt function_id,
       goto_programt &instrumentation_code)
@@ -1162,22 +1189,22 @@ void taint_instrumentert::instrument_location(
             acc_path,
             from_tokens_to_vars.at(arg_token.get_token_name()),
             symbol_table),
-          constant_exprt(bool_state_name, typet(ID_bool)));
+          bool_value);
         iit->function=function_id;
       }
     }
   };
   localt::make_assignments_to_shadow_variables(
     loc.get_turn_on(),
-    ID_true,
+    get_shadow_variable_value_true(),
     get_instrumented_symbol_table(),
     get_from_tokens_to_vars(),
     fn_call,
     loc.get_function_id(),
     instrumentation_code);
   localt::make_assignments_to_shadow_variables(
     loc.get_turn_off(),
-    ID_false,
+    get_shadow_variable_value_false(),
     get_instrumented_symbol_table(),
     get_from_tokens_to_vars(),
     fn_call,
@@ -1216,15 +1243,20 @@ void taint_instrumentert::instrument_location_data_flow_insensitive(
     // Here we build GOTO instruction guarded by a negated conjunction of
     // state variables, forming propositions of the assumption.
     exprt cond=
-      symbol_exprt(
-        from_tokens_to_vars.at(loc.get_assumption().front().get_token_name()),
-        typet(ID_bool));
+      equal_exprt(
+        symbol_exprt(
+          from_tokens_to_vars.at(loc.get_assumption().front().get_token_name()),
+          get_shadow_variable_type()),
+        get_shadow_variable_value_true());
     for(auto it=std::next(loc.get_assumption().cbegin());
         it!=loc.get_assumption().cend();
         ++it)
-      cond=and_exprt(cond,
-                     symbol_exprt(from_tokens_to_vars.at(it->get_token_name()),
-                     typet(ID_bool)));
+      cond = and_exprt(
+        cond,
+        equal_exprt(
+          symbol_exprt(from_tokens_to_vars.at(it->get_token_name()),
+                       get_shadow_variable_type()),
+          get_shadow_variable_value_true()));
     auto iit=instrumentation_code.add_instruction();
     iit->make_goto(instrumention_tail_instruction, not_exprt(cond));
     iit->function=loc.get_function_id();
@@ -1233,22 +1265,22 @@ void taint_instrumentert::instrument_location_data_flow_insensitive(
   for(const auto &arg_token : loc.get_turn_on())
   {
     auto iit=instrumentation_code.add_instruction(ASSIGN);
-    iit->code=code_assignt(
+    iit->code = code_assignt(
       symbol_exprt(
         from_tokens_to_vars.at(arg_token.get_token_name()),
-        typet(ID_bool)),
-      constant_exprt(ID_true, typet(ID_bool)));
+        get_shadow_variable_type()),
+      get_shadow_variable_value_true());
     iit->function=loc.get_function_id();
   }
   // Now we instrument "turn off" assignments of state variables.
   for(const auto &arg_token : loc.get_turn_off())
   {
     auto iit=instrumentation_code.add_instruction(ASSIGN);
-    iit->code=code_assignt(
+    iit->code = code_assignt(
       symbol_exprt(
         from_tokens_to_vars.at(arg_token.get_token_name()),
-        typet(ID_bool)),
-      constant_exprt(ID_false, typet(ID_bool)));
+        get_shadow_variable_type()),
+      get_shadow_variable_value_false());
     iit->function=loc.get_function_id();
   }
   if(props.get_sinks().count(lid))