Merge pull request #207 from peterschrammel/trace-outputs

kroening · web-flow · commit e26d20ed9f4d · 2016-08-21T17:30:45.000+01:00
Test inputs and outputs for C and Java
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
@@ -61,6 +61,7 @@ exprt::operandst build_function_environment(
       new_symbol.mode=ID_C;
       new_symbol.is_static_lifetime=false;
       new_symbol.name=identifier;
+      new_symbol.base_name=base_name;
       new_symbol.type=p.type();
     
       symbol_table.move(new_symbol);
@@ -93,6 +94,79 @@ exprt::operandst build_function_environment(
 
 /*******************************************************************\
 
+Function: record_function_outputs
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void record_function_outputs(
+  const symbolt &function,
+  code_blockt &init_code,
+  symbol_tablet &symbol_table)
+{
+  const code_typet::parameterst &parameters=
+    to_code_type(function.type).parameters();
+
+  exprt::operandst result;
+  result.reserve(parameters.size()+1);
+
+  bool has_return_value=
+    to_code_type(function.type).return_type()!=empty_typet();
+
+  if(has_return_value)
+  {
+    //record return value
+    codet output(ID_output);
+    output.operands().resize(2);
+
+    const symbolt &return_symbol=symbol_table.lookup("return'");
+
+    output.op0()=address_of_exprt(
+      index_exprt(string_constantt(return_symbol.base_name), 
+                  gen_zero(index_type())));
+    output.op1()=return_symbol.symbol_expr();
+    output.add_source_location()=
+      function.value.operands().back().source_location();
+
+    init_code.move_to_operands(output);
+  }
+
+  std::size_t i=0;
+
+  for(const auto & p : parameters)
+  {
+    irep_idt base_name=p.get_base_name();
+    if(base_name.empty()) base_name="argument#"+i2string(i);
+    irep_idt identifier=id2string(function.name)+
+      "::"+id2string(base_name);
+
+    const symbolt &symbol = symbol_table.lookup(identifier);
+
+    if(symbol.type.id()==ID_pointer)
+    {
+      codet output(ID_output);
+      output.operands().resize(2);
+
+      output.op0()=address_of_exprt(
+        index_exprt(string_constantt(symbol.base_name), 
+                    gen_zero(index_type())));
+      output.op1()=symbol.symbol_expr();
+      output.add_source_location()=p.source_location();
+
+      init_code.move_to_operands(output);
+    }
+
+    i++;
+  }
+}
+
+/*******************************************************************\
+
 Function: ansi_c_entry_point
 
   Inputs:
@@ -203,6 +277,18 @@ bool ansi_c_entry_point(
   call_main.add_source_location()=symbol.location;
   call_main.function()=symbol.symbol_expr();
   call_main.function().add_source_location()=symbol.location;
+  if(to_code_type(symbol.type).return_type()!=empty_typet())
+  {
+    auxiliary_symbolt return_symbol;
+    return_symbol.mode=ID_C;
+    return_symbol.is_static_lifetime=false;
+    return_symbol.name="return'";
+    return_symbol.base_name="return";
+    return_symbol.type=to_code_type(symbol.type).return_type();
+
+    symbol_table.add(return_symbol);
+    call_main.lhs()=return_symbol.symbol_expr();
+  }
 
   const code_typet::parameterst &parameters=
     to_code_type(symbol.type).parameters();
@@ -410,6 +496,10 @@ bool ansi_c_entry_point(
 
   init_code.move_to_operands(call_main);
 
+  // TODO: add read/modified (recursively in call graph) globals as INPUT/OUTPUT
+
+  record_function_outputs(symbol, init_code, symbol_table);
+
   // add the entry point symbol
   symbolt new_symbol;
 
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -3542,6 +3542,9 @@ std::string expr2ct::convert_code(
   if(statement==ID_input)
     return convert_code_input(src, indent);
 
+  if(statement==ID_output)
+    return convert_code_output(src, indent);
+
   if(statement==ID_assume)
     return convert_code_assume(src, indent);
 
@@ -3889,6 +3892,38 @@ std::string expr2ct::convert_code_input(
 
 /*******************************************************************\
 
+Function: expr2ct::convert_code_output
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string expr2ct::convert_code_output(
+  const codet &src,
+  unsigned indent)
+{
+  std::string dest=indent_str(indent)+"OUTPUT(";
+
+  forall_operands(it, src)
+  {
+    unsigned p;
+    std::string arg_str=convert(*it, p);
+
+    if(it!=src.operands().begin()) dest+=", ";
+    dest+=arg_str;
+  }
+
+  dest+=");";
+
+  return dest;
+}
+
+/*******************************************************************\
+
 Function: expr2ct::convert_code_array_set
 
   Inputs:
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
@@ -172,6 +172,7 @@ class expr2ct
   std::string convert_code_printf(const codet &src, unsigned indent);
   std::string convert_code_fence(const codet &src, unsigned indent);
   std::string convert_code_input(const codet &src, unsigned indent);
+  std::string convert_code_output(const codet &src, unsigned indent);
   std::string convert_code_array_set(const codet &src, unsigned indent);
   std::string convert_code_array_copy(const codet &src, unsigned indent);
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -968,7 +968,7 @@ bool cbmc_parse_optionst::process_goto_program(
         return true;
       }
           
-      status() << "Instrumenting coverge goals" << eom;
+      status() << "Instrumenting coverage goals" << eom;
       instrument_cover_goals(symbol_table, goto_functions, c);
       goto_functions.update();
     }
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
@@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/i2string.h>
 #include <util/prefix.h>
+#include <ansi-c/c_types.h>
+#include <ansi-c/string_constant.h>
 
 #include <goto-programs/goto_functions.h>
 
@@ -132,6 +134,128 @@ bool java_static_lifetime_init(
   return false;
 }
 
+
+/*******************************************************************\
+
+Function: java_build_arguments
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt::operandst java_build_arguments(
+  const symbolt &function,
+  code_blockt &init_code,
+  symbol_tablet &symbol_table)
+{
+  const code_typet::parameterst &parameters=
+    to_code_type(function.type).parameters();
+
+  exprt::operandst main_arguments;
+  main_arguments.resize(parameters.size());
+
+  for(std::size_t param_number=0;
+      param_number<parameters.size();
+      param_number++)
+  {
+    bool is_this=param_number==0 &&
+                 parameters[param_number].get_this();
+    bool allow_null=config.main!="" && !is_this;
+
+    main_arguments[param_number]=
+      object_factory(parameters[param_number].type(), 
+                     init_code, allow_null, symbol_table);
+
+    const symbolt &p_symbol=
+      symbol_table.lookup(parameters[param_number].get_identifier());
+
+    // record as an input
+    codet input(ID_input);
+    input.operands().resize(2);
+    input.op0()=address_of_exprt(
+      index_exprt(string_constantt(p_symbol.base_name), 
+                  gen_zero(index_type())));
+    input.op1()=main_arguments[param_number];
+    input.add_source_location()=parameters[param_number].source_location();
+
+    init_code.move_to_operands(input);
+  }
+
+  return main_arguments;
+}
+
+/*******************************************************************\
+
+Function: java_record_outputs
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void java_record_outputs(
+  const symbolt &function,
+  const exprt::operandst &main_arguments,
+  code_blockt &init_code, 
+  symbol_tablet &symbol_table)
+{
+  const code_typet::parameterst &parameters=
+    to_code_type(function.type).parameters();
+
+  exprt::operandst result;
+  result.reserve(parameters.size()+1);
+
+  bool has_return_value=
+    to_code_type(function.type).return_type()!=empty_typet();
+
+  if(has_return_value)
+  {
+    //record return value
+    codet output(ID_output);
+    output.operands().resize(2);
+
+    const symbolt &return_symbol=symbol_table.lookup("return'");
+
+    output.op0()=address_of_exprt(
+      index_exprt(string_constantt(return_symbol.base_name), 
+                  gen_zero(index_type())));
+    output.op1()=return_symbol.symbol_expr();
+    output.add_source_location()=
+      function.value.operands().back().source_location();
+
+    init_code.move_to_operands(output);
+  }
+
+  for(std::size_t param_number=0;
+      param_number<parameters.size();
+      param_number++)
+  {
+    const symbolt &p_symbol=
+      symbol_table.lookup(parameters[param_number].get_identifier());
+
+    if(p_symbol.type.id()==ID_pointer)
+    {
+      // record as an output
+      codet output(ID_output);
+      output.operands().resize(2);
+      output.op0()=address_of_exprt(
+        index_exprt(string_constantt(p_symbol.base_name), 
+                    gen_zero(index_type())));
+      output.op1()=main_arguments[param_number];
+      output.add_source_location()=parameters[param_number].source_location();
+
+      init_code.move_to_operands(output);
+    }
+  }
+}
+
 /*******************************************************************\
 
 Function: java_entry_point
@@ -287,8 +411,6 @@ bool java_entry_point(
   assert(!symbol.value.is_nil());
   assert(symbol.type.id()==ID_code);
 
-  const code_typet &code_type=to_code_type(symbol.type);
-    
   create_initialize(symbol_table);
 
   if(java_static_lifetime_init(symbol_table, symbol.location, message_handler))
@@ -321,30 +443,27 @@ bool java_entry_point(
   code_function_callt call_main;
   call_main.add_source_location()=symbol.location;
   call_main.function()=symbol.symbol_expr();
-
-  const code_typet::parameterst &parameters=
-    code_type.parameters();
-
-  exprt::operandst main_arguments;
-  main_arguments.resize(parameters.size());
-  
-  for(std::size_t param_number=0;
-      param_number<parameters.size();
-      param_number++)
+  if(to_code_type(symbol.type).return_type()!=empty_typet())
   {
-    bool is_this=param_number==0 &&
-                 parameters[param_number].get_this();
-    bool allow_null=config.main!="" && !is_this;
-    
-    main_arguments[param_number]=
-      object_factory(parameters[param_number].type(), 
-                     init_code, allow_null, symbol_table);
+    auxiliary_symbolt return_symbol;
+    return_symbol.mode=ID_C;
+    return_symbol.is_static_lifetime=false;
+    return_symbol.name="return'";
+    return_symbol.base_name="return";
+    return_symbol.type=to_code_type(symbol.type).return_type();
+
+    symbol_table.add(return_symbol);
+    call_main.lhs()=return_symbol.symbol_expr();
   }
 
+  exprt::operandst main_arguments=
+    java_build_arguments(symbol, init_code, symbol_table);
   call_main.arguments()=main_arguments;
 
   init_code.move_to_operands(call_main);
 
+  java_record_outputs(symbol, main_arguments, init_code, symbol_table);
+
   // add "main"
   symbolt new_symbol;
 

Original file line number	Diff line number	Diff line change
`@@ -968,7 +968,7 @@ bool cbmc_parse_optionst::process_goto_program(`
`968`	`968`	`return true;`
`969`	`969`	`}`
`970`	`970`
`971`		`- status() << "Instrumenting coverge goals" << eom;`
	`971`	`+ status() << "Instrumenting coverage goals" << eom;`
`972`	`972`	`instrument_cover_goals(symbol_table, goto_functions, c);`
`973`	`973`	`goto_functions.update();`
`974`	`974`	`}`