CONTRACTS: cleanup failure and debug output

Author: Remi Delmas

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -126,20 +126,6 @@ void dfcct::check_transform_goto_model_preconditions(
   const bool apply_loop_contracts,
   const std::set<std::string> &to_exclude_from_nondet_static)
 {
-  log.debug() << "harness_id " << harness_id << messaget::eom;
-
-  for(const auto &pair : to_check)
-  {
-    log.debug() << "to check " << pair.first << "->" << pair.second
-                << messaget::eom;
-  }
-
-  for(const auto &pair : to_replace)
-  {
-    log.debug() << "to replace " << pair.first << "->" << pair.second
-                << messaget::eom;
-  }
-
   // TODO reactivate this once I understand how entry points work
   // Check that the goto_model entry point matches the given harness_id
   // if(!config.main.has_value())

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_functions.cpp

@@ -95,23 +95,13 @@ const std::size_t dfcc_dsl_contract_functionst::get_nof_frees_targets() const
 
 void dfcc_dsl_contract_functionst::gen_spec_assigns_function()
 {
-  log.debug() << "->dfcc_dsl_contract_functionst::gen_spec_assigns_functions("
-              << pure_contract_symbol.name << ")" << messaget::eom;
-
   const auto &spec_function_symbol = utils.clone_and_rename_function(
     pure_contract_symbol.name, spec_assigns_function_id, empty_typet());
 
   const auto &spec_function_id = spec_function_symbol.name;
 
   auto &spec_code_type = to_code_type(spec_function_symbol.type);
 
-  for(auto &param : spec_code_type.parameters())
-  {
-    log.debug()
-      << "dfcc_dsl_contract_functionst::gen_spec_assigns_functions: new param "
-      << param.get_identifier() << messaget::eom;
-  }
-
   exprt::operandst lambda_parameters;
 
   if(code_with_contract.return_type().id() != ID_empty)
@@ -151,16 +141,6 @@ void dfcc_dsl_contract_functionst::gen_spec_assigns_function()
 
   goto_model.goto_functions.update();
 
-  // debug print the generated body
-  log.debug() << "->dfcc_dsl_contract_functionst::gen_spec_assigns_functions("
-              << pure_contract_symbol.name
-              << ") before inlining :" << messaget::eom;
-
-  forall_goto_program_instructions(iter, body)
-  {
-    body.output_instruction(ns, spec_function_id, log.debug(), *iter);
-  }
-
   inline_and_check_warnings(spec_function_id);
 
   PRECONDITION_WITH_DIAGNOSTICS(
@@ -169,16 +149,6 @@ void dfcc_dsl_contract_functionst::gen_spec_assigns_function()
     "model instrumentation");
 
   goto_model.goto_functions.update();
-
-  // debug print the generated body
-  log.debug() << "->dfcc_dsl_contract_functionst::gen_spec_assigns_functions("
-              << pure_contract_symbol.name
-              << ") after inlining :" << messaget::eom;
-
-  forall_goto_program_instructions(iter, body)
-  {
-    body.output_instruction(ns, spec_function_id, log.debug(), *iter);
-  }
 }
 
 void dfcc_dsl_contract_functionst::encode_assignable_target_group(
@@ -208,10 +178,6 @@ void dfcc_dsl_contract_functionst::encode_assignable_target(
   const exprt &target,
   goto_programt &dest)
 {
-  log.debug() << "->dfcc_dsl_contract_functionst::encode_assignable_target("
-              << from_expr_using_mode(ns, language_mode, target) << ")"
-              << messaget::eom;
-
   const source_locationt &source_location = target.source_location();
 
   if(can_cast_expr<side_effect_expr_function_callt>(target))
@@ -283,17 +249,10 @@ void dfcc_dsl_contract_functionst::encode_assignable_target(
         from_expr_using_mode(ns, language_mode, target),
       target.source_location());
   }
-  log.debug() << "<-dfcc_dsl_contract_functionst::encode_assignable_target("
-              << from_expr_using_mode(ns, language_mode, target) << ")"
-              << messaget::eom;
 }
 
 void dfcc_dsl_contract_functionst::gen_spec_frees_function()
 {
-  log.debug()
-    << "dfcc_dsl_contract_functionst::create_spec_frees_function_from_contract("
-    << pure_contract_symbol.name << ")" << messaget::eom;
-
   // fetch pure contract symbol
   const auto &code_with_contract =
     to_code_with_contract_type(pure_contract_symbol.type);
@@ -305,13 +264,6 @@ void dfcc_dsl_contract_functionst::gen_spec_frees_function()
 
   auto &spec_code_type = to_code_type(spec_function_symbol.type);
 
-  for(auto &param : spec_code_type.parameters())
-  {
-    log.debug()
-      << "dfcc_dsl_contract_functionst::gen_spec_frees_function: param "
-      << param.get_identifier() << messaget::eom;
-  }
-
   exprt::operandst lambda_parameters;
 
   if(code_with_contract.return_type().id() != ID_empty)
@@ -361,12 +313,6 @@ void dfcc_dsl_contract_functionst::gen_spec_frees_function()
     "model instrumentation");
 
   goto_model.goto_functions.update();
-
-  // debug print instructions
-  forall_goto_program_instructions(iter, body)
-  {
-    body.output_instruction(ns, spec_function_id, log.debug(), *iter);
-  }
 }
 
 void dfcc_dsl_contract_functionst::inline_and_check_warnings(

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_handler.cpp

@@ -112,12 +112,6 @@ const symbolt *dfcc_dsl_contract_handlert::get_pure_contract_symbol_ptr(
   auto pure_contract_id = "contract::" + id2string(contract_id);
   if(!ns.lookup(pure_contract_id, pure_contract_symbol))
   {
-    log.debug() << "contract_symbol: " << contract_symbol.name << messaget::eom;
-    log.debug() << contract_symbol.type.pretty() << messaget::eom;
-    log.debug() << "pure_contract_symbol: " << pure_contract_id
-                << messaget::eom;
-    log.debug() << pure_contract_symbol->type.pretty() << messaget::eom;
-
     check_signature_compat(
       contract_id,
       to_code_type(contract_symbol.type),

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_wrapper_program.cpp

@@ -218,9 +218,6 @@ void dfcc_dsl_wrapper_programt::add_to_dest(goto_programt &dest)
 
 void dfcc_dsl_wrapper_programt::encode_requires_write_set()
 {
-  log.debug() << "->dfcc_dsl_wrapper_programt::encode_requires_write_set()"
-              << messaget::eom;
-
   PRECONDITION(requires_write_set_symbol_opt);
   PRECONDITION(addr_of_requires_write_set_symbol_opt);
 
@@ -326,15 +323,10 @@ void dfcc_dsl_wrapper_programt::encode_requires_write_set()
     postamble.add(goto_programt::make_function_call(call));
     postamble.add(goto_programt::make_dead(write_set));
   }
-  log.debug() << "<-dfcc_dsl_wrapper_programt::encode_requires_write_set()"
-              << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_ensures_write_set()
 {
-  log.debug() << "->dfcc_dsl_wrapper_programt::encode_ensures_write_set()"
-              << messaget::eom;
-
   PRECONDITION(ensures_write_set_symbol_opt);
   PRECONDITION(addr_of_ensures_write_set_symbol_opt);
 
@@ -451,15 +443,10 @@ void dfcc_dsl_wrapper_programt::encode_ensures_write_set()
 
   // declare write set DEAD
   postamble.add(goto_programt::make_dead(write_set));
-  log.debug() << "<-dfcc_dsl_wrapper_programt::encode_ensures_write_set()"
-              << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_contract_write_set()
 {
-  log.debug() << "->dfcc_dsl_wrapper_programt::encode_contract_write_set()"
-              << messaget::eom;
-
   PRECONDITION(contract_write_set_symbol_opt);
 
   const auto write_set = contract_write_set_symbol_opt->symbol_expr();
@@ -576,15 +563,10 @@ void dfcc_dsl_wrapper_programt::encode_contract_write_set()
     postamble.add(goto_programt::make_function_call(call));
     postamble.add(goto_programt::make_dead(write_set));
   }
-  log.debug() << "<-dfcc_dsl_wrapper_programt::encode_contract_write_set()"
-              << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_is_fresh_set()
 {
-  log.debug() << "->dfcc_dsl_wrapper_programt::encode_is_fresh_set()"
-              << messaget::eom;
-
   PRECONDITION(is_fresh_set_symbol_opt);
   PRECONDITION(addr_of_is_fresh_set_symbol_opt);
 
@@ -622,15 +604,10 @@ void dfcc_dsl_wrapper_programt::encode_is_fresh_set()
 
   // DEAD instructions in postamble
   postamble.add(goto_programt::make_dead(object_set));
-
-  log.debug() << "<-dfcc_dsl_wrapper_programt::encode_is_fresh_set()"
-              << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_requires_clauses()
 {
-  log.debug() << "->dfcc_dsl_wrapper_programt::encode_requires_clauses()"
-              << messaget::eom;
   // we use this empty requires write set to check for the absence of side
   // effects in the requires clauses
   PRECONDITION(addr_of_requires_write_set_symbol_opt);
@@ -700,14 +677,10 @@ void dfcc_dsl_wrapper_programt::encode_requires_clauses()
 
   // append resulting program to preconditions section
   preconditions.destructive_append(requires_program);
-  log.debug() << "<-dfcc_dsl_wrapper_programt::encode_requires_clauses()"
-              << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_ensures_clauses()
 {
-  log.debug() << "->dfcc_dsl_wrapper_programt::encode_ensures_clauses()"
-              << messaget::eom;
   // we need the contract write set for the freed predicates
   PRECONDITION(addr_of_contract_write_set_symbol_opt);
   // we need the ensures write set to check for side effects
@@ -799,16 +772,10 @@ void dfcc_dsl_wrapper_programt::encode_ensures_clauses()
 
   // add the ensures program to the postconditions section
   postconditions.destructive_append(ensures_program);
-  log.debug() << "<-dfcc_dsl_wrapper_programt::encode_ensures_clauses()"
-              << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_requires_contract_clauses()
 {
-  log.debug()
-    << "->dfcc_dsl_wrapper_programt::encode_requires_contract_clauses()"
-    << messaget::eom;
-
   const auto &requires_contract = contract_code_type.requires_contract();
 
   if(contract_mode == dfcc_contract_modet::CHECK)
@@ -841,17 +808,10 @@ void dfcc_dsl_wrapper_programt::encode_requires_contract_clauses()
         preconditions);
     }
   }
-  log.debug()
-    << "<-dfcc_dsl_wrapper_programt::encode_requires_contract_clauses()"
-    << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_ensures_contract_clauses()
 {
-  log.debug()
-    << "->dfcc_dsl_wrapper_programt::encode_ensures_contract_clauses()"
-    << messaget::eom;
-
   const auto &ensures_contract = contract_code_type.ensures_contract();
 
   if(contract_mode == dfcc_contract_modet::CHECK)
@@ -875,9 +835,6 @@ void dfcc_dsl_wrapper_programt::encode_ensures_contract_clauses()
         postconditions);
     }
   }
-  log.debug()
-    << "<-dfcc_dsl_wrapper_programt::encode_ensures_contract_clauses()"
-    << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::assert_function_pointer_obeys_contract(
@@ -910,11 +867,6 @@ void dfcc_dsl_wrapper_programt::assume_function_pointer_obeys_contract(
   const function_pointer_obeys_contract_exprt &expr,
   goto_programt &dest)
 {
-  log.debug()
-    << "->dfcc_dsl_wrapper_programt::assume_function_pointer_obeys_contract("
-    << from_expr_using_mode(ns, contract_symbol.mode, expr) << ")"
-    << messaget::eom;
-
   function_pointer_contracts.insert(
     expr.contract_symbol_expr().get_identifier());
 
@@ -930,11 +882,6 @@ void dfcc_dsl_wrapper_programt::assume_function_pointer_obeys_contract(
   loc.set_comment(comment.str());
   dest.add(goto_programt::make_assignment(
     expr.function_pointer(), expr.address_of_contract(), loc));
-
-  log.debug()
-    << "<-dfcc_dsl_wrapper_programt::assume_function_pointer_obeys_contract("
-    << from_expr_using_mode(ns, contract_symbol.mode, expr) << ")"
-    << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_function_call()
@@ -947,9 +894,6 @@ void dfcc_dsl_wrapper_programt::encode_function_call()
 
 void dfcc_dsl_wrapper_programt::encode_checked_function_call()
 {
-  log.debug() << "->dfcc_dsl_wrapper_programt::encode_checked_function_call("
-              << wrapped_symbol.name << ")" << messaget::eom;
-
   PRECONDITION(contract_write_set_symbol_opt);
 
   // build call to the wrapped function
@@ -986,16 +930,10 @@ void dfcc_dsl_wrapper_programt::encode_checked_function_call()
     addr_of_contract_write_set_symbol_opt->symbol_expr());
 
   function_call.add(goto_programt::make_function_call(call));
-
-  log.debug() << "<-dfcc_dsl_wrapper_programt::encode_checked_function_call()"
-              << messaget::eom;
 }
 
 void dfcc_dsl_wrapper_programt::encode_havoced_function_call()
 {
-  log.debug() << "->dfcc_dsl_wrapper_programt::encode_havoced_function_call()"
-              << messaget::eom;
-
   PRECONDITION(contract_write_set_symbol_opt);
 
   // generate local write set and add as parameter to the call
@@ -1134,6 +1072,4 @@ void dfcc_dsl_wrapper_programt::encode_havoced_function_call()
       .symbol_expr(),
     {address_of_contract_write_set, caller_write_set});
   function_call.add(goto_programt::make_function_call(deallocate_call));
-  log.debug() << "<-dfcc_dsl_wrapper_programt::encode_havoced_function_call()"
-              << messaget::eom;
 }