Merge pull request #4855 from thomasspriggs/tas/iot

Add `code_inputt` and `code_outputt` for `ID_input` and `ID_output`

Author: thomasspriggs

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -311,7 +311,7 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
 
   // we iterate through all the parameters of the function under test, allocate
   // an object for that parameter (recursively allocating other objects
-  // necessary to initialize it), and declare such object as an ID_input
+  // necessary to initialize it), and mark such object using `code_inputt`.
   for(std::size_t param_number=0;
       param_number<parameters.size();
       param_number++)
@@ -420,17 +420,8 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
     }
 
     // record as an input
-    codet input(ID_input);
-    input.operands().resize(2);
-    input.op0()=
-      address_of_exprt(
-        index_exprt(
-          string_constantt(base_name),
-          from_integer(0, index_type())));
-    input.op1()=main_arguments[param_number];
-    input.add_source_location()=function.location;
-
-    init_code.add(std::move(input));
+    init_code.add(
+      code_inputt{base_name, main_arguments[param_number], function.location});
   }
 
   return make_pair(init_code, main_arguments);
@@ -467,13 +458,8 @@ static optionalt<codet> record_return_value(
   const symbolt &return_symbol =
     symbol_table.lookup_ref(JAVA_ENTRY_POINT_RETURN_SYMBOL);
 
-  codet output(ID_output);
-  output.operands().resize(2);
-  output.op0() = address_of_exprt(index_exprt(
-    string_constantt(return_symbol.base_name), from_integer(0, index_type())));
-  output.op1() = return_symbol.symbol_expr();
-  output.add_source_location() = function.location;
-  return output;
+  return code_outputt{
+    return_symbol.base_name, return_symbol.symbol_expr(), function.location};
 }
 
 static code_blockt record_pointer_parameters(
@@ -495,14 +481,8 @@ static code_blockt record_pointer_parameters(
     if(!can_cast_type<pointer_typet>(p_symbol.type))
       continue;
 
-    codet output(ID_output);
-    output.operands().resize(2);
-    output.op0() = address_of_exprt(index_exprt(
-      string_constantt(p_symbol.base_name), from_integer(0, index_type())));
-    output.op1() = arguments[param_number];
-    output.add_source_location() = function.location;
-
-    init_code.add(std::move(output));
+    init_code.add(code_outputt{
+      p_symbol.base_name, arguments[param_number], function.location});
   }
   return init_code;
 }
@@ -511,20 +491,13 @@ static codet record_exception(
   const symbolt &function,
   const symbol_table_baset &symbol_table)
 {
-  // record exceptional return variable as output
-  codet output(ID_output);
-  output.operands().resize(2);
-
   // retrieve the exception variable
   const symbolt &exc_symbol =
     symbol_table.lookup_ref(JAVA_ENTRY_POINT_EXCEPTION_SYMBOL);
 
-  output.op0()=address_of_exprt(
-    index_exprt(string_constantt(exc_symbol.base_name),
-                from_integer(0, index_type())));
-  output.op1()=exc_symbol.symbol_expr();
-  output.add_source_location()=function.location;
-  return output;
+  // record exceptional return variable as output
+  return code_outputt{
+    exc_symbol.base_name, exc_symbol.symbol_expr(), function.location};
 }
 
 main_function_resultt get_main_symbol(

jbmc/src/java_bytecode/java_entry_point.h

@@ -33,8 +33,8 @@ using build_argumentst =
 ///
 /// 1. Allocates and initializes the parameters of the method under test.
 /// 2. Call it and save its return variable in the variable 'return'.
-/// 3. Declare variable 'return' as an output variable (codet with id
-///    ID_output), together with other objects possibly altered by the execution
+/// 3. Declare variable 'return' as an output variable using a `code_outputt`,
+///    together with other objects possibly altered by the execution of
 ///    the method under test (in `java_record_outputs`)
 ///
 /// When \p assume_init_pointers_not_null is false, the generated parameter

src/ansi-c/ansi_c_entry_point.cpp

@@ -59,22 +59,11 @@ void record_function_outputs(
 
   if(has_return_value)
   {
-    // record return value
-    codet output(ID_output);
-    output.operands().resize(2);
-
     const symbolt &return_symbol = symbol_table.lookup_ref("return'");
 
-    output.op0()=
-      address_of_exprt(
-        index_exprt(
-          string_constantt(return_symbol.base_name),
-          from_integer(0, index_type())));
-
-    output.op1()=return_symbol.symbol_expr();
-    output.add_source_location()=function.location;
-
-    init_code.add(std::move(output));
+    // record return value
+    init_code.add(code_outputt{
+      return_symbol.base_name, return_symbol.symbol_expr(), function.location});
   }
 
   #if 0
@@ -333,15 +322,8 @@ bool generate_ansi_c_start_function(
         init_code.add(code_assumet(std::move(le)));
       }
 
-      {
-        // record argc as an input
-        codet input(ID_input);
-        input.operands().resize(2);
-        input.op0()=address_of_exprt(
-          index_exprt(string_constantt("argc"), from_integer(0, index_type())));
-        input.op1()=argc_symbol.symbol_expr();
-        init_code.add(std::move(input));
-      }
+      // record argc as an input
+      init_code.add(code_inputt{"argc", argc_symbol.symbol_expr()});
 
       if(parameters.size()==3)
       {

src/ansi-c/expr2c.cpp

@@ -2867,10 +2867,10 @@ std::string expr2ct::convert_code(
   if(statement==ID_fence)
     return convert_code_fence(src, indent);
 
-  if(statement==ID_input)
+  if(can_cast_expr<code_inputt>(src))
     return convert_code_input(src, indent);
 
-  if(statement==ID_output)
+  if(can_cast_expr<code_outputt>(src))
     return convert_code_output(src, indent);
 
   if(statement==ID_assume)

src/cpp/library/cprover.h

@@ -22,8 +22,10 @@ void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
 void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
 
-void __CPROVER_input(const char *id, ...);
-void __CPROVER_output(const char *id, ...);
+// NOLINTNEXTLINE(build/deprecated)
+void __CPROVER_input(const char *description, ...);
+// NOLINTNEXTLINE(build/deprecated)
+void __CPROVER_output(const char *description, ...);
 
 // concurrency-related
 void __CPROVER_atomic_begin();

src/goto-programs/builtin_functions.cpp

@@ -316,37 +316,29 @@ void goto_convertt::do_input(
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  codet input_code(ID_input);
-  input_code.operands()=arguments;
-  input_code.add_source_location()=function.source_location();
-
   if(arguments.size()<2)
   {
     error().source_location=function.find_source_location();
     error() << "input takes at least two arguments" << eom;
     throw 0;
   }
 
-  copy(input_code, OTHER, dest);
+  copy(code_inputt{arguments, function.source_location()}, OTHER, dest);
 }
 
 void goto_convertt::do_output(
   const exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  codet output_code(ID_output);
-  output_code.operands()=arguments;
-  output_code.add_source_location()=function.source_location();
-
   if(arguments.size()<2)
   {
     error().source_location=function.find_source_location();
     error() << "output takes at least two arguments" << eom;
     throw 0;
   }
 
-  copy(output_code, OTHER, dest);
+  copy(code_outputt{arguments, function.source_location()}, OTHER, dest);
 }
 
 void goto_convertt::do_atomic_begin(

src/goto-programs/interpreter.cpp

@@ -408,7 +408,7 @@ void interpretert::execute_other()
       assign(address, rhs);
     }
   }
-  else if(statement==ID_output)
+  else if(can_cast_expr<code_outputt>(pc->get_other()))
   {
     return;
   }

src/goto-symex/symex_other.cpp

@@ -97,12 +97,12 @@ void goto_symext::symex_other(
     const codet clean_code = to_code(clean_expr(code, state, false));
     symex_printf(state, clean_code);
   }
-  else if(statement==ID_input)
+  else if(can_cast_expr<code_inputt>(code))
   {
     const codet clean_code = to_code(clean_expr(code, state, false));
     symex_input(state, clean_code);
   }
-  else if(statement==ID_output)
+  else if(can_cast_expr<code_outputt>(code))
   {
     const codet clean_code = to_code(clean_expr(code, state, false));
     symex_output(state, clean_code);

src/pointer-analysis/value_set.cpp

@@ -1634,7 +1634,7 @@ void value_sett::apply_code_rec(
   else if(statement==ID_fence)
   {
   }
-  else if(statement==ID_input || statement==ID_output)
+  else if(can_cast_expr<code_inputt>(code) || can_cast_expr<code_outputt>(code))
   {
     // doesn't do anything
   }

src/pointer-analysis/value_set_fi.cpp

@@ -1400,7 +1400,7 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns)
           statement==ID_array_set)
   {
   }
-  else if(statement==ID_input || statement==ID_output)
+  else if(can_cast_expr<code_inputt>(code) || can_cast_expr<code_outputt>(code))
   {
     // doesn't do anything
   }

src/pointer-analysis/value_set_fivr.cpp

@@ -1528,7 +1528,7 @@ void value_set_fivrt::apply_code(const codet &code, const namespacet &ns)
       assign(lhs, code_return.return_value(), ns);
     }
   }
-  else if(statement==ID_input || statement==ID_output)
+  else if(can_cast_expr<code_inputt>(code) || can_cast_expr<code_outputt>(code))
   {
     // doesn't do anything
   }

src/pointer-analysis/value_set_fivrns.cpp

@@ -1192,7 +1192,7 @@ void value_set_fivrnst::apply_code(const codet &code, const namespacet &ns)
       assign(lhs, code_return.return_value(), ns);
     }
   }
-  else if(statement==ID_input || statement==ID_output)
+  else if(can_cast_expr<code_inputt>(code) || can_cast_expr<code_outputt>(code))
   {
     // doesn't do anything
   }

src/util/allocate_objects.cpp

@@ -247,13 +247,8 @@ void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code)
   //   INPUT("<identifier>", <identifier>);
   for(symbolt const *symbol_ptr : symbols_created)
   {
-    codet input_code(ID_input);
-    input_code.operands().resize(2);
-    input_code.op0() = address_of_exprt(index_exprt(
-      string_constantt(symbol_ptr->base_name), from_integer(0, index_type())));
-    input_code.op1() = symbol_ptr->symbol_expr();
-    input_code.add_source_location() = source_location;
-    init_code.add(std::move(input_code));
+    init_code.add(code_inputt{
+      symbol_ptr->base_name, symbol_ptr->symbol_expr(), source_location});
   }
 }
 

src/util/std_code.cpp

@@ -11,7 +11,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "std_code.h"
 
+#include "arith_tools.h"
+#include "c_types.h"
 #include "std_expr.h"
+#include "string_constant.h"
 
 /// If this `codet` is a \ref code_blockt (i.e.\ it represents a block of
 /// statements), return the unmodified input. Otherwise (i.e.\ the `codet`
@@ -167,3 +170,59 @@ void code_function_bodyt::set_parameter_identifiers(
     sub.back().set(ID_identifier, id);
   }
 }
+
+code_inputt::code_inputt(
+  std::vector<exprt> arguments,
+  optionalt<source_locationt> location)
+  : codet{ID_input, std::move(arguments)}
+{
+  if(location)
+    add_source_location() = std::move(*location);
+  check(*this, validation_modet::INVARIANT);
+}
+
+code_inputt::code_inputt(
+  const irep_idt &description,
+  exprt expression,
+  optionalt<source_locationt> location)
+  : code_inputt{{address_of_exprt(index_exprt(
+                   string_constantt(description),
+                   from_integer(0, index_type()))),
+                 std::move(expression)},
+                std::move(location)}
+{
+}
+
+void code_inputt::check(const codet &code, const validation_modet vm)
+{
+  DATA_CHECK(
+    vm, code.operands().size() >= 2, "input must have at least two operands");
+}
+
+code_outputt::code_outputt(
+  std::vector<exprt> arguments,
+  optionalt<source_locationt> location)
+  : codet{ID_output, std::move(arguments)}
+{
+  if(location)
+    add_source_location() = std::move(*location);
+  check(*this, validation_modet::INVARIANT);
+}
+
+code_outputt::code_outputt(
+  const irep_idt &description,
+  exprt expression,
+  optionalt<source_locationt> location)
+  : code_outputt{{address_of_exprt(index_exprt(
+                    string_constantt(description),
+                    from_integer(0, index_type()))),
+                  std::move(expression)},
+                 std::move(location)}
+{
+}
+
+void code_outputt::check(const codet &code, const validation_modet vm)
+{
+  DATA_CHECK(
+    vm, code.operands().size() >= 2, "output must have at least two operands");
+}