c_nondet_symbol_factory.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: C Nondet Symbol Factory
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
 
#include "c_nondet_symbol_factory.h"
 
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/fresh_symbol.h>
#include <util/namespace.h>
#include <util/nondet_bool.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <util/symbol.h>
 
#include <goto-programs/goto_functions.h>
 
#include "allocate_objects.h"
#include "c_object_factory_parameters.h"
 
void symbol_factoryt::gen_nondet_init(
  code_blockt &assignments,
  const exprt &expr,
  const std::size_t depth,
  recursion_sett recursion_set,
  const bool assign_const)
{
  const typet &type = expr.type();
 
  if(!assign_const && expr.type().get_bool(ID_C_constant))
  {
    return;
  }
 
  if(type.id()==ID_pointer)
  {
    // dereferenced type
    const pointer_typet &pointer_type=to_pointer_type(type);
    const typet &base_type = pointer_type.base_type();
 
    if(base_type.id() == ID_code)
    {
      // Handle the pointer-to-code case separately:
      // leave as nondet_ptr to allow `remove_function_pointers`
      // to replace the pointer.
      assignments.add(code_frontend_assignt{
        expr, side_effect_expr_nondett{pointer_type, loc}});
      return;
    }
 
    if(base_type.id() == ID_struct_tag)
    {
      const irep_idt struct_tag =
        to_struct_tag_type(base_type).get_identifier();
 
      if(
        recursion_set.find(struct_tag) != recursion_set.end() &&
        depth >= object_factory_params.max_nondet_tree_depth)
      {
        assignments.add(
          code_frontend_assignt{expr, null_pointer_exprt{pointer_type}, loc});
 
        return;
      }
    }
 
    code_blockt non_null_inst;
 
    typet object_type = base_type;
    if(object_type.id() == ID_empty)
      object_type = char_type();
 
    exprt init_expr = allocate_objects.allocate_object(
      non_null_inst, expr, object_type, lifetime);
 
    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);
 
    if(depth < object_factory_params.min_null_tree_depth)
    {
      // Add the following code to assignments:
      // <expr> = <aoe>;
      assignments.append(non_null_inst);
    }
    else
    {
      // Add the following code to assignments:
      //           IF !NONDET(_Bool) THEN GOTO <label1>
      //           <expr> = <null pointer>
      //           GOTO <label2>
      // <label1>: <expr> = &tmp$<temporary_counter>;
      //           <code from recursive call to gen_nondet_init() with
      //             tmp$<temporary_counter>>
      // And the next line is labelled label2
      const code_frontend_assignt set_null_inst{
        expr, null_pointer_exprt{pointer_type}, loc};
 
      code_ifthenelset null_check(
        side_effect_expr_nondett(bool_typet(), loc),
        std::move(set_null_inst),
        std::move(non_null_inst));
 
      assignments.add(std::move(null_check));
    }
  }
  else if(type.id() == ID_struct_tag)
  {
    const auto &struct_tag_type = to_struct_tag_type(type);
 
    const irep_idt struct_tag = struct_tag_type.get_identifier();
 
    recursion_set.insert(struct_tag);
 
    const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
 
    for(const auto &component : struct_type.components())
    {
      const typet &component_type = component.type();
 
      if(!assign_const && component_type.get_bool(ID_C_constant))
      {
        continue;
      }
 
      const irep_idt name = component.get_name();
 
      member_exprt me(expr, name, component_type);
      me.add_source_location() = loc;
 
      gen_nondet_init(assignments, me, depth, recursion_set, assign_const);
    }
  }
  else if(type.id() == ID_array)
  {
    gen_nondet_array_init(assignments, expr, depth, recursion_set);
  }
  else
  {
    // If type is a ID_c_bool then add the following code to assignments:
    //   <expr> = NONDET(_BOOL);
    // Else add the following code to assignments:
    //   <expr> = NONDET(type);
    exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
                                       : side_effect_expr_nondett(type, loc);
    code_frontend_assignt assign(expr, rhs);
    assign.add_source_location()=loc;
 
    assignments.add(std::move(assign));
  }
}
void symbol_factoryt::gen_nondet_init( {…}
 
void symbol_factoryt::gen_nondet_array_init(
  code_blockt &assignments,
  const exprt &expr,
  std::size_t depth,
  const recursion_sett &recursion_set)
{
  auto const &array_type = to_array_type(expr.type());
  const auto &size = array_type.size();
  PRECONDITION(size.is_constant());
  auto const array_size = numeric_cast<mp_integer>(to_constant_expr(size));
  DATA_INVARIANT(
    array_size.has_value() && *array_size >= 0,
    "Arrays should have positive size");
  for(mp_integer index = 0; index < *array_size; ++index)
  {
    gen_nondet_init(
      assignments,
      index_exprt(expr, from_integer(index, size_type())),
      depth,
      recursion_set);
  }
}
void symbol_factoryt::gen_nondet_array_init( {…}
 
symbol_exprt c_nondet_symbol_factory(
  code_blockt &init_code,
  symbol_table_baset &symbol_table,
  const irep_idt base_name,
  const typet &type,
  const source_locationt &loc,
  const c_object_factory_parameterst &object_factory_parameters,
  const lifetimet lifetime)
{
  const symbolt &main_symbol = get_fresh_aux_symbol(
    type,
    id2string(goto_functionst::entry_point()),
    id2string(base_name),
    loc,
    ID_C,
    symbol_table);
  symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
 
  symbol_factoryt state(
    symbol_table,
    loc,
    goto_functionst::entry_point(),
    object_factory_parameters,
    lifetime);
 
  code_blockt assignments;
  state.gen_nondet_init(assignments, main_symbol_expr);
 
  state.add_created_symbol(main_symbol);
  state.declare_created_symbols(init_code);
 
  init_code.append(assignments);
 
  state.mark_created_symbols_as_input(init_code);
 
  return main_symbol_expr;
}
symbol_exprt c_nondet_symbol_factory( {…}