Removes some dead code.

Several functions from the old implementation of code-contracts that
were made dead by the previous commits are removed by this commit.

Additionally, some variables which were formerly in use are no longer
needed, and so are removed.

Author: klaas

src/goto-instrument/code_contracts.cpp

@@ -34,8 +34,7 @@ class code_contractst
     goto_functionst &_goto_functions):
       ns(_symbol_table),
       symbol_table(_symbol_table),
-      goto_functions(_goto_functions),
-      temporary_counter(0)
+      goto_functions(_goto_functions)
   {
   }
 
@@ -46,10 +45,6 @@ class code_contractst
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
 
-  unsigned temporary_counter;
-
-  std::unordered_set<irep_idt> summarized;
-
   void apply_code_contracts();
   void check_code_contracts();
 
@@ -76,160 +71,11 @@ class code_contractst
     const goto_programt::targett loop_head,
     const loopt &loop);
 
-  void add_contract_check(
-    const irep_idt &function,
-    goto_programt &dest);
-
   const symbolt &new_tmp_symbol(
     const typet &type,
     const source_locationt &source_location);
 };
 
-static void check_apply_invariants(
-  goto_functionst::goto_functiont &goto_function,
-  const local_may_aliast &local_may_alias,
-  const goto_programt::targett loop_head,
-  const loopt &loop)
-{
-  PRECONDITION(!loop.empty());
-
-  // find the last back edge
-  goto_programt::targett loop_end=loop_head;
-  for(const goto_programt::targett &inst : loop)
-  {
-    if(inst->is_goto() &&
-       inst->get_target() == loop_head &&
-       inst->location_number>loop_end->location_number)
-    {
-      loop_end = inst;
-    }
-  }
-
-  // see whether we have an invariant
-  exprt invariant=
-    static_cast<const exprt&>(
-      loop_end->guard.find(ID_C_spec_loop_invariant));
-  if(invariant.is_nil())
-  {
-    return;
-  }
-
-  // change H: loop; E: ...
-  // to
-  // H: assert(invariant);
-  // if(nondet) goto E:
-  // havoc reads and writes of loop;
-  // assume(invariant);
-  // assume(guard)  [only for for/while loops]
-  // loop;
-  // assert(invariant);
-  // assume(false);
-  // E: havoc writes of loop;
-  // assume(invariant)
-  // assume(!guard)
-  // ...
-
-  // find out what can get changed in the loop
-  modifiest modifies;
-  get_modifies(local_may_alias, loop, modifies);
-
-  // find out what is used by the loop
-  usest uses;
-  get_uses(local_may_alias, loop, uses);
-
-  // build the havocking code
-  goto_programt havoc_all_code;
-  goto_programt havoc_writes_code;
-
-  // assert the invariant
-  {
-    goto_programt::targett a=havoc_all_code.add_instruction(ASSERT);
-    a->guard=invariant;
-    a->function=loop_head->function;
-    a->source_location=loop_head->source_location;
-    a->source_location.set_comment("Loop invariant violated before entry");
-  }
-
-  // nondeterministically skip the loop
-  {
-    goto_programt::targett jump=havoc_all_code.add_instruction(GOTO);
-    jump->guard=side_effect_expr_nondett(bool_typet());
-    jump->targets.push_back(loop_end);
-    jump->function=loop_head->function;
-    jump->source_location=loop_head->source_location;
-  }
-
-  // havoc variables being written to
-  build_havoc_code(loop_head, uses, havoc_all_code);
-
-  // assume the invariant
-  {
-    goto_programt::targett assume=havoc_all_code.add_instruction(ASSUME);
-    assume->guard=invariant;
-    assume->function=loop_head->function;
-    assume->source_location=loop_head->source_location;
-  }
-
-  // assert the invariant at the end of the loop body
-  {
-    goto_programt::targett a = goto_function.body.insert_before(loop_end);
-    a->type=ASSERT;
-    a->guard=invariant;
-    a->function=loop_end->function;
-    a->source_location=loop_end->source_location;
-    a->source_location.set_comment("Loop invariant not preserved");
-  }
-
-  // assume false at the end of the loop to discharge the havocking
-  {
-    goto_programt::targett assume = goto_function.body.insert_before(loop_end);
-    assume->type=ASSUME;
-    assume->guard.make_false();
-    assume->function=loop_end->function;
-    assume->source_location=loop_end->source_location;
-  }
-
-  build_havoc_code(loop_end, modifies, havoc_writes_code);
-
-  // Assume the invariant (now after the loop)
-  {
-    goto_programt::targett assume=havoc_writes_code.add_instruction(ASSUME);
-    assume->guard=invariant;
-    assume->function=loop_head->function;
-    assume->source_location=loop_head->source_location;
-  }
-
-  // change the back edge into assume(!guard)
-  loop_end->targets.clear();
-  loop_end->type=ASSUME;
-  if(loop_head->is_goto())
-  {
-    loop_end->guard = loop_head->guard;
-  }
-  else
-  {
-    loop_end->guard.make_not();
-  }
-
-  // Change the loop head to assume the guard if a for/while loop.
-  // This needs to be done after we case on what loop_head is in the previous
-  // section of setup.
-  if(loop_head->is_goto())
-  {
-    exprt guard = loop_head->guard;
-    guard.make_not();
-    loop_head->make_assumption(guard);
-  }
-
-  // Now havoc at the loop head. Use insert_swap to
-  // preserve jumps to loop head.
-  goto_function.body.insert_before_swap(loop_head, havoc_all_code);
-
-  // Now havoc at the loop end. Use insert_swap to
-  // preserve jumps to loop end.
-  goto_function.body.insert_before_swap(loop_end, havoc_writes_code);
-}
-
 void code_contractst::apply_contract(
   goto_programt &goto_program,
   goto_programt::targett target)
@@ -297,8 +143,6 @@ void code_contractst::apply_contract(
   // TODO: Havoc write set of the function between assert and ensure.
 
   target->make_assumption(ensures);
-
-  summarized.insert(function);
 }
 
 void code_contractst::apply_invariant(
@@ -599,28 +443,6 @@ void code_contractst::check_apply_invariant(
   goto_function.body.insert_before_swap(loop_head, havoc_code);
 }
 
-void code_contractst::code_contracts(
-  goto_functionst::goto_functiont &goto_function)
-{
-  local_may_aliast local_may_alias(goto_function);
-  natural_loops_mutablet natural_loops(goto_function.body);
-
-  // iterate over the (natural) loops in the function
-  for(const auto &l_it : natural_loops.loop_map)
-  {
-    check_apply_invariants(
-      goto_function,
-      local_may_alias,
-      l_it.first,
-      l_it.second);
-  }
-
-  // look at all function calls
-  Forall_goto_program_instructions(it, goto_function.body)
-    if(it->is_function_call())
-      apply_contract(goto_function.body, it);
-}
-
 const symbolt &code_contractst::new_tmp_symbol(
   const typet &type,
   const source_locationt &source_location)
@@ -634,122 +456,6 @@ const symbolt &code_contractst::new_tmp_symbol(
     symbol_table);
 }
 
-void code_contractst::add_contract_check(
-  const irep_idt &function,
-  goto_programt &dest)
-{
-  PRECONDITION(!dest.instructions.empty());
-
-  goto_functionst::function_mapt::iterator f_it=
-    goto_functions.function_map.find(function);
-  assert(f_it!=goto_functions.function_map.end());
-
-  const goto_functionst::goto_functiont &gf=f_it->second;
-
-  exprt requires = static_cast<const exprt&>(gf.type.find(ID_C_spec_requires));
-  exprt ensures = static_cast<const exprt&>(gf.type.find(ID_C_spec_ensures));
-  assert(ensures.is_not_nil());
-
-  // build:
-  // if(nondet)
-  //   decl ret
-  //   decl parameter1 ...
-  //   assume(requires)  [optional]
-  //   ret=function(parameter1, ...)
-  //   assert(ensures)
-  //   assume(false)
-  // skip: ...
-
-  // build skip so that if(nondet) can refer to it
-  goto_programt tmp_skip;
-  goto_programt::targett skip=tmp_skip.add_instruction(SKIP);
-  skip->function=dest.instructions.front().function;
-  skip->source_location=ensures.source_location();
-
-  goto_programt check;
-
-  // if(nondet)
-  goto_programt::targett g=check.add_instruction();
-  g->make_goto(skip, side_effect_expr_nondett(bool_typet()));
-  g->function=skip->function;
-  g->source_location=skip->source_location;
-
-  // prepare function call including all declarations
-  code_function_callt call;
-  call.function()=ns.lookup(function).symbol_expr();
-  replace_symbolt replace;
-
-  // decl ret
-  if(gf.type.return_type()!=empty_typet())
-  {
-    goto_programt::targett d=check.add_instruction(DECL);
-    d->function=skip->function;
-    d->source_location=skip->source_location;
-
-    symbol_exprt r=
-      new_tmp_symbol(gf.type.return_type(),
-                     d->source_location).symbol_expr();
-    d->code=code_declt(r);
-
-    call.lhs()=r;
-
-    replace.insert("__CPROVER_return_value", r);
-  }
-
-  // decl parameter1 ...
-  for(const auto &p_it : gf.type.parameters())
-  {
-    goto_programt::targett d=check.add_instruction(DECL);
-    d->function=skip->function;
-    d->source_location=skip->source_location;
-
-    symbol_exprt p=
-      new_tmp_symbol(p_it.type(),
-                     d->source_location).symbol_expr();
-    d->code=code_declt(p);
-
-    call.arguments().push_back(p);
-
-    if(!p_it.get_identifier().empty())
-      replace.insert(p_it.get_identifier(), p);
-  }
-
-  // rewrite any use of parameters
-  replace(requires);
-  replace(ensures);
-
-  // assume(requires)
-  if(requires.is_not_nil())
-  {
-    goto_programt::targett a=check.add_instruction();
-    a->make_assumption(requires);
-    a->function=skip->function;
-    a->source_location=requires.source_location();
-  }
-
-  // ret=function(parameter1, ...)
-  goto_programt::targett f=check.add_instruction();
-  f->make_function_call(call);
-  f->function=skip->function;
-  f->source_location=skip->source_location;
-
-  // assert(ensures)
-  goto_programt::targett a=check.add_instruction();
-  a->make_assertion(ensures);
-  a->function=skip->function;
-  a->source_location=ensures.source_location();
-
-  // assume(false)
-  goto_programt::targett af=check.add_instruction();
-  af->make_assumption(false_exprt());
-  af->function=skip->function;
-  af->source_location=ensures.source_location();
-
-  // prepend the new code to dest
-  check.destructive_append(tmp_skip);
-  dest.destructive_insert(dest.instructions.begin(), check);
-}
-
 void code_contractst::apply_code_contracts()
 {
   Forall_goto_functions(it, goto_functions)

src/goto-instrument/loop_utils.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "loop_utils.h"
 
 #include <util/std_expr.h>
-#include <util/expr_iterator.h>
 
 #include <analyses/natural_loops.h>
 #include <analyses/local_may_alias.h>
@@ -108,41 +107,3 @@ void get_modifies(
     }
   }
 }
-
-// TODO handle aliasing at all
-void get_uses(
-  const local_may_aliast &local_may_alias,
-  const loopt &loop,
-  usest &uses)
-{
-  for(loopt::const_iterator
-      i_it=loop.begin(); i_it!=loop.end(); i_it++)
-  {
-    const goto_programt::instructiont &instruction=**i_it;
-    if(instruction.code.is_not_nil())
-    {
-      for(const_depth_iteratort it=instruction.code.depth_begin();
-          it!=instruction.code.depth_end();
-          ++it)
-      {
-        if((*it).id()==ID_symbol)
-        {
-          uses.insert(*it);
-        }
-      }
-    }
-
-    if(instruction.guard.is_not_nil())
-    {
-      for(const_depth_iteratort it=instruction.guard.depth_begin();
-          it!=instruction.guard.depth_end();
-          ++it)
-      {
-        if((*it).id()==ID_symbol)
-        {
-          uses.insert(*it);
-        }
-      }
-    }
-  }
-}