X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=newfuzzer.h;h=67454ffc268198c96b13360c23df9a0da0939990;hb=HEAD;hp=02c3fc0102d5e4b359fa43acb4b3737f85010078;hpb=e137463093ac5dbf0449d8eba9101d57b1fcbdeb;p=c11tester.git diff --git a/newfuzzer.h b/newfuzzer.h deleted file mode 100644 index 02c3fc01..00000000 --- a/newfuzzer.h +++ /dev/null @@ -1,73 +0,0 @@ -#ifndef __NEWFUZZER_H__ -#define __NEWFUZZER_H__ - -#include "fuzzer.h" -#include "classlist.h" -#include "mymemory.h" -#include "stl-model.h" -#include "predicate.h" - -struct node_dist_info { - node_dist_info(thread_id_t tid, FuncNode * node, int distance) : - tid(tid), - target(node), - dist(distance) - {} - - thread_id_t tid; - FuncNode * target; - int dist; - - SNAPSHOTALLOC -}; - -class NewFuzzer : public Fuzzer { -public: - NewFuzzer(); - int selectWrite(ModelAction *read, SnapVector* rf_set); - bool has_paused_threads(); - void notify_paused_thread(Thread * thread); - - Thread * selectThread(int * threadlist, int numthreads); - Thread * selectNotify(action_list_t * waiters); - bool shouldSleep(const ModelAction * sleep); - bool shouldWake(const ModelAction * sleep); - bool shouldWait(const ModelAction * wait); - - void register_engine(ModelChecker * model, ModelExecution * execution); - Predicate * get_selected_child_branch(thread_id_t tid); - - SNAPSHOTALLOC -private: - ModelHistory * history; - ModelExecution * execution; - - SnapVector thrd_last_read_act; - SnapVector thrd_last_func_inst; - - SnapVector available_branches_tmp_storage; - SnapVector thrd_selected_child_branch; - SnapVector< SnapVector *> thrd_pruned_writes; - - bool check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, inst_act_map_t * inst_act_map, SnapVector * rf_set); - Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst); - bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector * rf_set, inst_act_map_t * inst_act_map); - int choose_branch_index(SnapVector * branches); - - /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite. - */ - SnapVector paused_thread_list; //-- (not in use) - HashTable paused_thread_table; //-- - HashTable failed_predicates; - - SnapVector dist_info_vec; //-- - - void conditional_sleep(Thread * thread); //-- - void wake_up_paused_threads(int * threadlist, int * numthreads); //-- - - bool find_threads(ModelAction * pending_read); //-- - - bool check_predicate_expressions(PredExprSet * pred_expressions, inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate); -}; - -#endif /* end of __NEWFUZZER_H__ */