Merge pull request #651 from diffblue/property_checker_resultt

tautschnig · web-flow · commit 4f830746b102 · 2024-08-30T19:56:08.000+02:00
introduce `property_checker_resultt`
diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp
@@ -22,8 +22,6 @@ Author: Daniel Kroening, daniel.kroening@inf.ethz.ch
 #include <trans-netlist/unwind_netlist.h>
 #include <verilog/sva_expr.h>
 
-#include "report_results.h"
-
 #include <algorithm>
 #include <iostream>
 
@@ -51,7 +49,7 @@ class bdd_enginet
   {
   }
 
-  int operator()();
+  property_checker_resultt operator()();
 
 protected:
   using propertiest = ebmc_propertiest;
@@ -173,7 +171,7 @@ Function: bdd_enginet::operator()
 
 \*******************************************************************/
 
-int bdd_enginet::operator()()
+property_checker_resultt bdd_enginet::operator()()
 {
   try
   {
@@ -216,30 +214,29 @@ int bdd_enginet::operator()()
       }
 
       std::cout << '\n';
-        
-      return 0;
+
+      return property_checker_resultt::SUCCESS;
     }
 
     if(properties.properties.empty())
     {
       message.error() << "no properties" << messaget::eom;
-      return 1;
+      return property_checker_resultt::ERROR;
     }
 
     for(propertyt &p : properties.properties)
       check_property(p);
 
-    report_results(cmdline, properties, ns, message.get_message_handler());
-    return properties.exit_code();
+    return property_checker_resultt::VERIFICATION_RESULT;
   }
   catch(const char *error_msg)
   {
     message.error() << error_msg << messaget::eom;
-    return 1;
+    return property_checker_resultt::ERROR;
   }
   catch(int)
   {
-    return 1;
+    return property_checker_resultt::ERROR;
   }
 }
 
@@ -1002,7 +999,7 @@ Function: bdd_engine
 
 \*******************************************************************/
 
-int bdd_engine(
+property_checker_resultt bdd_engine(
   const cmdlinet &cmdline,
   transition_systemt &transition_system,
   ebmc_propertiest &properties,
diff --git a/src/ebmc/bdd_engine.h b/src/ebmc/bdd_engine.h
@@ -9,12 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_EBMC_BDD_ENGINE_H
 #define CPROVER_EBMC_BDD_ENGINE_H
 
-#include <util/cmdline.h>
-#include <util/message.h>
+#include "property_checker.h"
 
-#include "ebmc_properties.h"
-
-int bdd_engine(
+property_checker_resultt bdd_engine(
   const cmdlinet &,
   transition_systemt &,
   ebmc_propertiest &,
diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
@@ -19,7 +19,6 @@ Author: Daniel Kroening, daniel.kroening@inf.ethz.ch
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "liveness_to_safety.h"
-#include "report_results.h"
 
 #include <fstream>
 
@@ -118,7 +117,7 @@ Function: k_induction
 
 \*******************************************************************/
 
-int k_induction(
+property_checker_resultt k_induction(
   const cmdlinet &cmdline,
   transition_systemt &transition_system,
   ebmc_propertiest &properties,
@@ -154,9 +153,7 @@ int k_induction(
   k_induction(
     k, transition_system, properties, solver_factory, message_handler);
 
-  const namespacet ns(transition_system.symbol_table);
-  report_results(cmdline, properties, ns, message_handler);
-  return properties.exit_code();
+  return property_checker_resultt::VERIFICATION_RESULT;
 }
 
 /*******************************************************************\
diff --git a/src/ebmc/k_induction.h b/src/ebmc/k_induction.h
@@ -13,11 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 
 #include "ebmc_solver_factory.h"
+#include "property_checker.h"
 
 class transition_systemt;
 class ebmc_propertiest;
 
-int k_induction(
+property_checker_resultt k_induction(
   const cmdlinet &,
   transition_systemt &,
   ebmc_propertiest &,
diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
@@ -27,7 +27,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <chrono>
 #include <iostream>
 
-int word_level_bmc(
+property_checker_resultt word_level_bmc(
   const cmdlinet &cmdline,
   const transition_systemt &transition_system,
   ebmc_propertiest &properties,
@@ -38,8 +38,6 @@ int word_level_bmc(
   bool convert_only = cmdline.isset("smt2") || cmdline.isset("outfile") ||
                       cmdline.isset("show-formula");
 
-  int result = 0;
-
   try
   {
     if(cmdline.isset("max-bound"))
@@ -93,38 +91,34 @@ int word_level_bmc(
         solver_factory,
         message_handler);
 
-      if(!convert_only)
-      {
-        const namespacet ns(transition_system.symbol_table);
-        report_results(cmdline, properties, ns, message_handler);
-        result = properties.exit_code();
-      }
+      if(convert_only)
+        return property_checker_resultt::SUCCESS;
     }
   }
 
   catch(const char *e)
   {
     messaget message{message_handler};
     message.error() << e << messaget::eom;
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
   catch(const std::string &e)
   {
     messaget message{message_handler};
     message.error() << e << messaget::eom;
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
   catch(int)
   {
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
-  return result;
+  return property_checker_resultt::VERIFICATION_RESULT;
 }
 
-int finish_bit_level_bmc(
+property_checker_resultt finish_bit_level_bmc(
   std::size_t bound,
   const bmc_mapt &bmc_map,
   propt &solver,
@@ -179,12 +173,12 @@ int finish_bit_level_bmc(
 
     case propt::resultt::P_ERROR:
       message.error() << "Error from decision procedure" << messaget::eom;
-      return 2;
+      return property_checker_resultt::ERROR;
 
     default:
       message.error() << "Unexpected result from decision procedure"
                       << messaget::eom;
-      return 1;
+      return property_checker_resultt::ERROR;
     }
   }
 
@@ -195,10 +189,10 @@ int finish_bit_level_bmc(
     << std::chrono::duration<double>(sat_stop_time - sat_start_time).count()
     << messaget::eom;
 
-  return properties.exit_code();
+  return property_checker_resultt::VERIFICATION_RESULT;
 }
 
-int bit_level_bmc(
+property_checker_resultt bit_level_bmc(
   cnft &solver,
   bool convert_only,
   const cmdlinet &cmdline,
@@ -220,8 +214,6 @@ int bit_level_bmc(
     bound = 1;
   }
 
-  int result;
-
   try
   {
     bmc_mapt bmc_map;
@@ -288,38 +280,35 @@ int bit_level_bmc(
     }
 
     if(convert_only)
-      result = 0;
+      return property_checker_resultt::SUCCESS;
     else
     {
-      result = finish_bit_level_bmc(
+      return finish_bit_level_bmc(
         bound, bmc_map, solver, transition_system, properties, message_handler);
-      report_results(cmdline, properties, ns, message_handler);
     }
   }
 
   catch(const char *e)
   {
     messaget message{message_handler};
     message.error() << e << messaget::eom;
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
   catch(const std::string &e)
   {
     messaget message{message_handler};
     message.error() << e << messaget::eom;
-    return 10;
+    return property_checker_resultt::ERROR;
   }
 
   catch(int)
   {
-    return 10;
+    return property_checker_resultt::ERROR;
   }
-
-  return result;
 }
 
-int bit_level_bmc(
+property_checker_resultt bit_level_bmc(
   const cmdlinet &cmdline,
   transition_systemt &transition_system,
   ebmc_propertiest &properties,
@@ -380,23 +369,43 @@ int property_checker(
   ebmc_propertiest &properties,
   message_handlert &message_handler)
 {
+  property_checker_resultt result;
+
   if(cmdline.isset("bdd") || cmdline.isset("show-bdds"))
   {
-    return bdd_engine(cmdline, transition_system, properties, message_handler);
+    result =
+      bdd_engine(cmdline, transition_system, properties, message_handler);
   }
   else if(cmdline.isset("aig") || cmdline.isset("dimacs"))
   {
-    return bit_level_bmc(
-      cmdline, transition_system, properties, message_handler);
+    result =
+      bit_level_bmc(cmdline, transition_system, properties, message_handler);
   }
   else if(cmdline.isset("k-induction"))
   {
-    return k_induction(cmdline, transition_system, properties, message_handler);
+    result =
+      k_induction(cmdline, transition_system, properties, message_handler);
   }
   else
   {
     // default engine is word-level BMC
-    return word_level_bmc(
-      cmdline, transition_system, properties, message_handler);
+    result =
+      word_level_bmc(cmdline, transition_system, properties, message_handler);
+  }
+
+  switch(result)
+  {
+  case property_checker_resultt::ERROR:
+    return 10;
+
+  case property_checker_resultt::SUCCESS:
+    return 0;
+
+  case property_checker_resultt::VERIFICATION_RESULT:
+    const namespacet ns{transition_system.symbol_table};
+    report_results(cmdline, properties, ns, message_handler);
+    return properties.exit_code();
   }
+
+  UNREACHABLE;
 }
diff --git a/src/ebmc/property_checker.h b/src/ebmc/property_checker.h
@@ -12,6 +12,13 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "ebmc_properties.h"
 #include "transition_system.h"
 
+enum class property_checker_resultt
+{
+  VERIFICATION_RESULT,
+  SUCCESS,
+  ERROR
+};
+
 int property_checker(
   const cmdlinet &,
   transition_systemt &,

Original file line number	Diff line number	Diff line change
`@@ -22,8 +22,6 @@ Author: Daniel Kroening, [email protected]`
`22`	`22`	`#include <trans-netlist/unwind_netlist.h>`
`23`	`23`	`#include <verilog/sva_expr.h>`
`24`	`24`
`25`		`-#include "report_results.h"`
`26`		`-`
`27`	`25`	`#include <algorithm>`
`28`	`26`	`#include <iostream>`
`29`	`27`
`@@ -51,7 +49,7 @@ class bdd_enginet`
`51`	`49`	`{`
`52`	`50`	`}`
`53`	`51`
`54`		`- int operator()();`
	`52`	`+ property_checker_resultt operator()();`
`55`	`53`
`56`	`54`	`protected:`
`57`	`55`	`using propertiest = ebmc_propertiest;`
`@@ -173,7 +171,7 @@ Function: bdd_enginet::operator()`
`173`	`171`
`174`	`172`	`\*******************************************************************/`
`175`	`173`
`176`		`-int bdd_enginet::operator()()`
	`174`	`+property_checker_resultt bdd_enginet::operator()()`
`177`	`175`	`{`
`178`	`176`	`try`
`179`	`177`	`{`
`@@ -216,30 +214,29 @@ int bdd_enginet::operator()()`
`216`	`214`	`}`
`217`	`215`
`218`	`216`	`std::cout << '\n';`
`219`		`-`
`220`		`- return 0;`
	`217`	`+`
	`218`	`+ return property_checker_resultt::SUCCESS;`
`221`	`219`	`}`
`222`	`220`
`223`	`221`	`if(properties.properties.empty())`
`224`	`222`	`{`
`225`	`223`	`message.error() << "no properties" << messaget::eom;`
`226`		`- return 1;`
	`224`	`+ return property_checker_resultt::ERROR;`
`227`	`225`	`}`
`228`	`226`
`229`	`227`	`for(propertyt &p : properties.properties)`
`230`	`228`	`check_property(p);`
`231`	`229`
`232`		`- report_results(cmdline, properties, ns, message.get_message_handler());`
`233`		`- return properties.exit_code();`
	`230`	`+ return property_checker_resultt::VERIFICATION_RESULT;`
`234`	`231`	`}`
`235`	`232`	`catch(const char *error_msg)`
`236`	`233`	`{`
`237`	`234`	`message.error() << error_msg << messaget::eom;`
`238`		`- return 1;`
	`235`	`+ return property_checker_resultt::ERROR;`
`239`	`236`	`}`
`240`	`237`	`catch(int)`
`241`	`238`	`{`
`242`		`- return 1;`
	`239`	`+ return property_checker_resultt::ERROR;`
`243`	`240`	`}`
`244`	`241`	`}`
`245`	`242`
`@@ -1002,7 +999,7 @@ Function: bdd_engine`
`1002`	`999`
`1003`	`1000`	`\*******************************************************************/`
`1004`	`1001`
`1005`		`-int bdd_engine(`
	`1002`	`+property_checker_resultt bdd_engine(`
`1006`	`1003`	`const cmdlinet &cmdline,`
`1007`	`1004`	`transition_systemt &transition_system,`
`1008`	`1005`	`ebmc_propertiest &properties,`
Original file line number	Diff line number	Diff line change
`@@ -27,7 +27,7 @@ Author: Daniel Kroening, [email protected]`
`27`	`27`	`#include <chrono>`
`28`	`28`	`#include <iostream>`
`29`	`29`
`30`		`-int word_level_bmc(`
	`30`	`+property_checker_resultt word_level_bmc(`
`31`	`31`	`const cmdlinet &cmdline,`
`32`	`32`	`const transition_systemt &transition_system,`
`33`	`33`	`ebmc_propertiest &properties,`
`@@ -38,8 +38,6 @@ int word_level_bmc(`
`38`	`38`	`bool convert_only = cmdline.isset("smt2") \|\| cmdline.isset("outfile") \|\|`
`39`	`39`	`cmdline.isset("show-formula");`
`40`	`40`
`41`		`- int result = 0;`
`42`		`-`
`43`	`41`	`try`
`44`	`42`	`{`
`45`	`43`	`if(cmdline.isset("max-bound"))`
`@@ -93,38 +91,34 @@ int word_level_bmc(`
`93`	`91`	`solver_factory,`
`94`	`92`	`message_handler);`
`95`	`93`
`96`		`- if(!convert_only)`
`97`		`- {`
`98`		`- const namespacet ns(transition_system.symbol_table);`
`99`		`- report_results(cmdline, properties, ns, message_handler);`
`100`		`- result = properties.exit_code();`
`101`		`- }`
	`94`	`+ if(convert_only)`
	`95`	`+ return property_checker_resultt::SUCCESS;`
`102`	`96`	`}`
`103`	`97`	`}`
`104`	`98`
`105`	`99`	`catch(const char *e)`
`106`	`100`	`{`
`107`	`101`	`messaget message{message_handler};`
`108`	`102`	`message.error() << e << messaget::eom;`
`109`		`- return 10;`
	`103`	`+ return property_checker_resultt::ERROR;`
`110`	`104`	`}`
`111`	`105`
`112`	`106`	`catch(const std::string &e)`
`113`	`107`	`{`
`114`	`108`	`messaget message{message_handler};`
`115`	`109`	`message.error() << e << messaget::eom;`
`116`		`- return 10;`
	`110`	`+ return property_checker_resultt::ERROR;`
`117`	`111`	`}`
`118`	`112`
`119`	`113`	`catch(int)`
`120`	`114`	`{`
`121`		`- return 10;`
	`115`	`+ return property_checker_resultt::ERROR;`
`122`	`116`	`}`
`123`	`117`
`124`		`- return result;`
	`118`	`+ return property_checker_resultt::VERIFICATION_RESULT;`
`125`	`119`	`}`
`126`	`120`
`127`		`-int finish_bit_level_bmc(`
	`121`	`+property_checker_resultt finish_bit_level_bmc(`
`128`	`122`	`std::size_t bound,`
`129`	`123`	`const bmc_mapt &bmc_map,`
`130`	`124`	`propt &solver,`
`@@ -179,12 +173,12 @@ int finish_bit_level_bmc(`
`179`	`173`
`180`	`174`	`case propt::resultt::P_ERROR:`
`181`	`175`	`message.error() << "Error from decision procedure" << messaget::eom;`
`182`		`- return 2;`
	`176`	`+ return property_checker_resultt::ERROR;`
`183`	`177`
`184`	`178`	`default:`
`185`	`179`	`message.error() << "Unexpected result from decision procedure"`
`186`	`180`	`<< messaget::eom;`
`187`		`- return 1;`
	`181`	`+ return property_checker_resultt::ERROR;`
`188`	`182`	`}`
`189`	`183`	`}`
`190`	`184`
`@@ -195,10 +189,10 @@ int finish_bit_level_bmc(`
`195`	`189`	`<< std::chrono::duration<double>(sat_stop_time - sat_start_time).count()`
`196`	`190`	`<< messaget::eom;`
`197`	`191`
`198`		`- return properties.exit_code();`
	`192`	`+ return property_checker_resultt::VERIFICATION_RESULT;`
`199`	`193`	`}`
`200`	`194`
`201`		`-int bit_level_bmc(`
	`195`	`+property_checker_resultt bit_level_bmc(`
`202`	`196`	`cnft &solver,`
`203`	`197`	`bool convert_only,`
`204`	`198`	`const cmdlinet &cmdline,`
`@@ -220,8 +214,6 @@ int bit_level_bmc(`
`220`	`214`	`bound = 1;`
`221`	`215`	`}`
`222`	`216`
`223`		`- int result;`
`224`		`-`
`225`	`217`	`try`
`226`	`218`	`{`
`227`	`219`	`bmc_mapt bmc_map;`
`@@ -288,38 +280,35 @@ int bit_level_bmc(`
`288`	`280`	`}`
`289`	`281`
`290`	`282`	`if(convert_only)`
`291`		`- result = 0;`
	`283`	`+ return property_checker_resultt::SUCCESS;`
`292`	`284`	`else`
`293`	`285`	`{`
`294`		`- result = finish_bit_level_bmc(`
	`286`	`+ return finish_bit_level_bmc(`
`295`	`287`	`bound, bmc_map, solver, transition_system, properties, message_handler);`
`296`		`- report_results(cmdline, properties, ns, message_handler);`
`297`	`288`	`}`
`298`	`289`	`}`
`299`	`290`
`300`	`291`	`catch(const char *e)`
`301`	`292`	`{`
`302`	`293`	`messaget message{message_handler};`
`303`	`294`	`message.error() << e << messaget::eom;`
`304`		`- return 10;`
	`295`	`+ return property_checker_resultt::ERROR;`
`305`	`296`	`}`
`306`	`297`
`307`	`298`	`catch(const std::string &e)`
`308`	`299`	`{`
`309`	`300`	`messaget message{message_handler};`
`310`	`301`	`message.error() << e << messaget::eom;`
`311`		`- return 10;`
	`302`	`+ return property_checker_resultt::ERROR;`
`312`	`303`	`}`
`313`	`304`
`314`	`305`	`catch(int)`
`315`	`306`	`{`
`316`		`- return 10;`
	`307`	`+ return property_checker_resultt::ERROR;`
`317`	`308`	`}`
`318`		`-`
`319`		`- return result;`
`320`	`309`	`}`
`321`	`310`
`322`		`-int bit_level_bmc(`
	`311`	`+property_checker_resultt bit_level_bmc(`
`323`	`312`	`const cmdlinet &cmdline,`
`324`	`313`	`transition_systemt &transition_system,`
`325`	`314`	`ebmc_propertiest &properties,`
`@@ -380,23 +369,43 @@ int property_checker(`
`380`	`369`	`ebmc_propertiest &properties,`
`381`	`370`	`message_handlert &message_handler)`
`382`	`371`	`{`
	`372`	`+ property_checker_resultt result;`
	`373`	`+`
`383`	`374`	`if(cmdline.isset("bdd") \|\| cmdline.isset("show-bdds"))`
`384`	`375`	`{`
`385`		`- return bdd_engine(cmdline, transition_system, properties, message_handler);`
	`376`	`+ result =`
	`377`	`+ bdd_engine(cmdline, transition_system, properties, message_handler);`
`386`	`378`	`}`
`387`	`379`	`else if(cmdline.isset("aig") \|\| cmdline.isset("dimacs"))`
`388`	`380`	`{`
`389`		`- return bit_level_bmc(`
`390`		`- cmdline, transition_system, properties, message_handler);`
	`381`	`+ result =`
	`382`	`+ bit_level_bmc(cmdline, transition_system, properties, message_handler);`
`391`	`383`	`}`
`392`	`384`	`else if(cmdline.isset("k-induction"))`
`393`	`385`	`{`
`394`		`- return k_induction(cmdline, transition_system, properties, message_handler);`
	`386`	`+ result =`
	`387`	`+ k_induction(cmdline, transition_system, properties, message_handler);`
`395`	`388`	`}`
`396`	`389`	`else`
`397`	`390`	`{`
`398`	`391`	`// default engine is word-level BMC`
`399`		`- return word_level_bmc(`
`400`		`- cmdline, transition_system, properties, message_handler);`
	`392`	`+ result =`
	`393`	`+ word_level_bmc(cmdline, transition_system, properties, message_handler);`
	`394`	`+ }`
	`395`	`+`
	`396`	`+ switch(result)`
	`397`	`+ {`
	`398`	`+ case property_checker_resultt::ERROR:`
	`399`	`+ return 10;`
	`400`	`+`
	`401`	`+ case property_checker_resultt::SUCCESS:`
	`402`	`+ return 0;`
	`403`	`+`
	`404`	`+ case property_checker_resultt::VERIFICATION_RESULT:`
	`405`	`+ const namespacet ns{transition_system.symbol_table};`
	`406`	`+ report_results(cmdline, properties, ns, message_handler);`
	`407`	`+ return properties.exit_code();`
`401`	`408`	`}`
	`409`	`+`
	`410`	`+ UNREACHABLE;`
`402`	`411`	`}`