From 33b2f41917477533d4993d5a385ee811027ef24f Mon Sep 17 00:00:00 2001 From: polgreen Date: Thu, 19 Oct 2017 19:09:01 +0200 Subject: [PATCH 1/2] Add eager infeasbility, dfs and bfs to symex help file --- src/symex/symex_parse_options.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index d28b638..7be39cf 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -636,6 +636,9 @@ void symex_parse_optionst::help() " --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" + " --dfs use depth first search\n" + " --bfs use breadth first search\n" + " --eager-infeasibility query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*) "\n" "Other options:\n" " --version show version and exit\n" From cec0d9413ec54883a27e5788b47edcdff2def1c7 Mon Sep 17 00:00:00 2001 From: polgreen Date: Thu, 19 Oct 2017 15:12:56 +0200 Subject: [PATCH 2/2] Introduce randomized DFS Randomized DFS shuffles the queue of successor states --- src/symex/path_search.cpp | 25 +++++++++++++++++++++++++ src/symex/path_search.h | 8 ++++++-- src/symex/symex_parse_options.cpp | 8 +++++++- src/symex/symex_parse_options.h | 1 + 4 files changed, 39 insertions(+), 3 deletions(-) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 18106ae..9ca139b 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -20,6 +20,27 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + +void path_searcht::shuffle_queue(queuet &queue) +{ + if(queue.size()<=1) + return; + + INVARIANT(queue.size()::max(), + "Queue size must be less than maximum integer"); + // pick random state and move to front + int rand_i = rand() % queue.size(); + + std::list::iterator it = queue.begin(); + for(int i=0; i queuet; queuet queue; - + /// Pick random element of queue and move to front + /// \param queue queue to be shuffled + void shuffle_queue(queuet &queue); // search heuristic void pick_state(); @@ -151,7 +154,8 @@ class path_searcht:public safety_checkert unsigned unwind_limit; unsigned time_limit; - enum class search_heuristict { DFS, BFS, LOCS } search_heuristic; + enum class search_heuristict + { DFS, RAN_DFS, BFS, LOCS } search_heuristic; source_locationt last_source_location; }; diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 7be39cf..b2a7243 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -232,7 +232,12 @@ int symex_parse_optionst::doit() safe_string2unsigned(cmdline.get_value("max-search-time"))); if(cmdline.isset("dfs")) - path_search.set_dfs(); + { + if(cmdline.isset("randomize")) + path_search.set_randomized_dfs(); + else + path_search.set_dfs(); + } if(cmdline.isset("bfs")) path_search.set_bfs(); @@ -638,6 +643,7 @@ void symex_parse_optionst::help() " --max-search-time s limit search to approximately s seconds\n" " --dfs use depth first search\n" " --bfs use breadth first search\n" + " --randomize used in conjunction with dfs, to search by randomized dfs\n" // NOLINT(*) " --eager-infeasibility query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*) "\n" "Other options:\n" diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index 99fd3f6..066b83e 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -41,6 +41,7 @@ class optionst; "(error-label):(verbosity):(no-library)" \ "(version)" \ "(bfs)(dfs)(locs)" \ + "(randomize)" \ "(cover):" \ "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ "(ppc-macos)(unsigned-char)" \