CONTRACTS: only throw proper exception objects

Author: Remi Delmas

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

@@ -148,7 +148,7 @@ void dfcct::check_transform_goto_model_preconditions(
   //                  "goto model, expected '"
   //               << harness_id << "', aborting contracts transformations."
   //               << messaget::eom;
-  //   throw 0;
+  //   throw invalid_input_exceptiont(msg);
   // }
 
   // if(config.main.value() != harness_id)
@@ -157,7 +157,7 @@ void dfcct::check_transform_goto_model_preconditions(
   //               << config.main.value()
   //               << "' differs from given harness function '" << harness_id
   //               << "', aborting contracts transformations." << messaget::eom;
-  //   throw 0;
+  //   throw invalid_input_exceptiont(msg);
   // }
 
   // check there is at most one function to check

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

@@ -139,15 +139,12 @@ const symbolt *dfcc_dsl_contract_handlert::get_pure_contract_symbol_ptr(
     new_symbol.module = contract_symbol.module;
     new_symbol.location = contract_symbol.location;
     auto entry = goto_model.symbol_table.insert(std::move(new_symbol));
-    if(!entry.second)
-    {
-      log.error().source_location = contract_symbol.location;
-      log.error() << "contract '" << contract_symbol.display_name()
-                  << "' already set at " << entry.first.location.as_string()
-                  << messaget::eom;
-      throw 0;
-    }
-    // this lookup must work, and no need to check for signature compatibility
+    INVARIANT(
+      entry.second,
+      "contract '" + id2string(contract_symbol.display_name()) +
+        "' already set at " + id2string(entry.first.location.as_string()));
+    // this lookup will work and set the pointer
+    // no need to check for signature compatibility
     ns.lookup(pure_contract_id, pure_contract_symbol);
   }
   return pure_contract_symbol;
@@ -157,12 +154,11 @@ const symbolt &dfcc_dsl_contract_handlert::get_pure_contract_symbol(
   const irep_idt &contract_id)
 {
   auto result = get_pure_contract_symbol_ptr(contract_id);
-  if(result != nullptr)
-    return *result;
-
-  log.error() << "dfcc_dsl_contract_handlert: pure contract symbol for "
-              << contract_id << " was not found, aborting" << messaget::eom;
-  throw 0;
+  INVARIANT(
+    result != nullptr,
+    "pure contract symbol for " + id2string(contract_id) +
+      " could not be found");
+  return *result;
 }
 
 const bool dfcc_dsl_contract_handlert::pure_contract_symbol_exists(
@@ -187,30 +183,29 @@ void dfcc_dsl_contract_handlert::check_signature_compat(
     std::ostringstream err_msg;
     err_msg << "dfcc_dsl_contract_handlert: function '" << contract_id
             << "' and the corresponding pure contract symbol '"
-            << pure_contract_id
-            << "' have incompatible type signatures:" << std::endl;
+            << pure_contract_id << "' have incompatible type signatures:\n";
 
     err_msg << "- contract return type "
-            << from_type(ns, contract_id, contract_type.return_type())
-            << std::endl;
+            << from_type(ns, contract_id, contract_type.return_type()) << "\n";
 
     for(const auto &param : contract_type.parameters())
     {
       err_msg << "- contract param type "
-              << from_type(ns, contract_id, param.type()) << std::endl;
+              << from_type(ns, contract_id, param.type()) << "\n";
     }
 
     err_msg << "- pure contract return type "
             << from_type(ns, pure_contract_id, pure_contract_type.return_type())
-            << std::endl;
+            << "\n";
 
     for(const auto &param : pure_contract_type.parameters())
     {
       err_msg << "- pure contract param type "
-              << from_type(ns, pure_contract_id, param.type()) << std::endl;
+              << from_type(ns, pure_contract_id, param.type()) << "\n";
     }
 
-    err_msg << "aborting." << std::endl;
+    err_msg << "aborting."
+            << "\n";
     throw invalid_source_file_exceptiont(
       err_msg.str(), contract_type.source_location());
   }

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

@@ -312,13 +312,13 @@ void dfcc_libraryt::load(std::set<irep_idt> &to_instrument)
   {
     const auto &found =
       goto_model.goto_functions.function_map.find(pair.second);
-    if(!(found != goto_model.goto_functions.function_map.end() &&
-         found->second.body_available()))
-    {
-      log.error() << "dfcc_libraryt: GOTO body of dfcc function " << pair.second
-                  << " not found" << messaget::eom;
-      throw 0;
-    }
+
+    INVARIANT(
+      found != goto_model.goto_functions.function_map.end() &&
+        found->second.body_available(),
+      "body of DFCC library function " + id2string(pair.second) +
+        " could not be found");
+
     dfcc_fun_symbol[pair.first] = ns.lookup(pair.second);
   }
 

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

@@ -184,11 +184,11 @@ void dfcc_spec_functionst::generate_havoc_function(
     {
       if(ins_it->call_function().id() != ID_symbol)
       {
-        log.error().source_location = ins_it->source_location();
-        log.error() << "dfcc_spec_functionst::generate_havoc_function: "
-                       "function pointer calls not supported"
-                    << messaget::eom;
-        throw 0;
+        throw invalid_source_file_exceptiont(
+          "Function pointer call '" +
+            from_expr(ns, function_id, ins_it->call_function()) +
+            "' in function '" + id2string(function_id) + "' is not supported",
+          ins_it->source_location());
       }
 
       const irep_idt &callee_id =
@@ -328,11 +328,11 @@ void dfcc_spec_functionst::to_spec_assigns_function(
     {
       if(ins_it->call_function().id() != ID_symbol)
       {
-        log.error().source_location = ins_it->source_location();
-        log.error()
-          << "dfcc_spec_functionst::function pointer calls not supported"
-          << messaget::eom;
-        throw 0;
+        throw invalid_source_file_exceptiont(
+          "Function pointer call '" +
+            from_expr(ns, function_id, ins_it->call_function()) +
+            "' in function '" + id2string(function_id) + "' is not supported",
+          ins_it->source_location());
       }
 
       const irep_idt &callee_id =
@@ -410,9 +410,11 @@ void dfcc_spec_functionst::to_spec_frees_function(
     {
       if(ins_it->call_function().id() != ID_symbol)
       {
-        log.error().source_location = ins_it->source_location();
-        log.error() << "function pointer calls not supported" << messaget::eom;
-        throw 0;
+        throw invalid_source_file_exceptiont(
+          "Function pointer call '" +
+            from_expr(ns, function_id, ins_it->call_function()) +
+            "' in function '" + id2string(function_id) + "' is not supported",
+          ins_it->source_location());
       }
 
       const irep_idt &callee_id =

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

@@ -79,17 +79,17 @@ void dfcc_swap_and_wrapt::swap_and_wrap(
       return;
 
     // already swapped with something else, abort
-    log.error() << " multiple attempts to swap and wrap function '"
-                << function_id << "':" << messaget::eom;
     auto mode1 =
       (pair.second == dfcc_contract_modet::REPLACE) ? "REPLACE" : "CHECK";
-    log.error() << "with '" << pair.first << "' in mode " << mode1
-                << messaget::eom;
     auto mode2 =
       (contract_mode == dfcc_contract_modet::REPLACE) ? "REPLACE" : "CHECK)";
-    log.error() << "with '" << contract_id << "' in mode " << mode2
-                << messaget::eom;
-    throw 0;
+
+    std::ostringstream err_msg;
+    err_msg << "DFCC: multiple attempts to swap and wrap function '"
+            << function_id << "':\n";
+    err_msg << "- with '" << pair.first << "' in mode " << mode1 << "\n";
+    err_msg << "- with '" << contract_id << "' in mode " << mode2 << "\n";
+    throw invalid_input_exceptiont(err_msg.str());
   }
 
   cache.insert({function_id, {contract_id, contract_mode}});