symex --max-search-time limit and cleanup

All symex limits use value -1 as marking "not set". Use size_t for counting
statistics.

Author: tautschnig

src/symex/path_search.cpp

@@ -281,19 +281,19 @@ bool path_searcht::drop_state(const statet &state)
   }
 
   // depth limit
-  if(depth_limit_set && state.get_depth()>depth_limit)
+  if(depth_limit>=0 && state.get_depth()>depth_limit)
     return true;
 
   // context bound
-  if(context_bound_set && state.get_no_thread_interleavings()>context_bound)
+  if(context_bound>=0 && state.get_no_thread_interleavings()>context_bound)
     return true;
 
   // branch bound
-  if(branch_bound_set && state.get_no_branches()>branch_bound)
+  if(branch_bound>=0 && state.get_no_branches()>branch_bound)
     return true;
 
   // unwinding limit -- loops
-  if(unwind_limit_set && state.get_instruction()->is_backwards_goto())
+  if(unwind_limit>=0 && pc->is_backwards_goto())
   {
     bool stop=false;
 
@@ -319,7 +319,7 @@ bool path_searcht::drop_state(const statet &state)
   }
 
   // unwinding limit -- recursion
-  if(unwind_limit_set && state.get_instruction()->is_function_call())
+  if(unwind_limit>=0 && pc->is_function_call())
   {
     bool stop=false;
 
@@ -346,6 +346,11 @@ bool path_searcht::drop_state(const statet &state)
       return true;
   }
 
+  // search time limit (--max-search-time)
+  if(time_limit>=0 &&
+     current_time().get_t()>start_time.get_t()+time_limit*1000)
+    return true;
+
   if(pc->is_assume() &&
      simplify_expr(pc->guard, ns).is_false())
   {

src/symex/path_search.h

@@ -26,53 +26,55 @@ class path_searcht:public safety_checkert
     safety_checkert(_ns),
     show_vcc(false),
     eager_infeasibility(false),
-    depth_limit_set(false), // no limit
-    context_bound_set(false),
-    unwind_limit_set(false),
-    branch_bound_set(false),
+    depth_limit(-1), // no limit
+    context_bound(-1),
+    branch_bound(-1),
+    unwind_limit(-1),
+    time_limit(-1),
     search_heuristic(search_heuristict::DFS)
   {
   }
 
   virtual resultt operator()(
     const goto_functionst &goto_functions);
 
-  void set_depth_limit(unsigned limit)
+  void set_depth_limit(int limit)
   {
-    depth_limit_set=true;
     depth_limit=limit;
   }
 
-  void set_context_bound(unsigned limit)
+  void set_context_bound(int limit)
   {
-    context_bound_set=true;
     context_bound=limit;
   }
 
-  void set_branch_bound(unsigned limit)
+  void set_branch_bound(int limit)
   {
-    branch_bound_set=true;
     branch_bound=limit;
   }
 
-  void set_unwind_limit(unsigned limit)
+  void set_unwind_limit(int limit)
   {
-    unwind_limit_set=true;
     unwind_limit=limit;
   }
 
+  void set_time_limit(int limit)
+  {
+    time_limit=limit;
+  }
+
   bool show_vcc;
   bool eager_infeasibility;
 
   // statistics
-  unsigned number_of_dropped_states;
-  unsigned number_of_paths;
-  unsigned number_of_steps;
-  unsigned number_of_feasible_paths;
-  unsigned number_of_infeasible_paths;
-  unsigned number_of_VCCs;
-  unsigned number_of_VCCs_after_simplification;
-  unsigned number_of_failed_properties;
+  std::size_t number_of_dropped_states;
+  std::size_t number_of_paths;
+  std::size_t number_of_steps;
+  std::size_t number_of_feasible_paths;
+  std::size_t number_of_infeasible_paths;
+  std::size_t number_of_VCCs;
+  std::size_t number_of_VCCs_after_simplification;
+  std::size_t number_of_failed_properties;
   std::size_t number_of_locs;
   absolute_timet start_time;
   time_periodt sat_time;
@@ -130,11 +132,11 @@ class path_searcht:public safety_checkert
   void initialize_property_map(
     const goto_functionst &goto_functions);
 
-  unsigned depth_limit;
-  unsigned context_bound;
-  unsigned branch_bound;
-  unsigned unwind_limit;
-  bool depth_limit_set, context_bound_set, unwind_limit_set, branch_bound_set;
+  int depth_limit;
+  int context_bound;
+  int branch_bound;
+  int unwind_limit;
+  int time_limit;
 
   enum class search_heuristict { DFS, BFS, LOCS } search_heuristic;
 

src/symex/symex_parse_options.cpp

@@ -186,6 +186,10 @@ int symex_parse_optionst::doit()
       path_search.set_unwind_limit(
         unsafe_string2unsigned(cmdline.get_value("unwind")));
 
+    if(cmdline.isset("max-search-time"))
+      path_search.set_time_limit(
+        safe_string2unsigned(cmdline.get_value("max-search-time")));
+
     if(cmdline.isset("dfs"))
       path_search.set_dfs();
 
@@ -607,6 +611,7 @@ void symex_parse_optionst::help()
     " --depth nr                   limit search depth\n"
     " --context-bound nr           limit number of context switches\n"
     " --branch-bound nr            limit number of branches taken\n"
+    " --max-search-time s          limit search to approximately s seconds\n"
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"

src/symex/symex_parse_options.h

@@ -30,7 +30,7 @@ class optionst;
 #define SYMEX_OPTIONS \
   "(function):" \
   "D:I:" \
-  "(depth):(context-bound):(branch-bound):(unwind):" \
+  "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \