From: Brian Demsky Date: Thu, 12 Dec 2019 05:54:43 +0000 (-0800) Subject: Add functions to SnapList plus tabbing X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=f5d5c517f482c639d5daa579dfdc840d19eecea5;p=c11tester.git Add functions to SnapList plus tabbing --- diff --git a/execution.cc b/execution.cc index 3c2edafa..b1687a75 100644 --- a/execution.cc +++ b/execution.cc @@ -1159,8 +1159,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) { - action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); - list->push_back(act); + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); + list->push_back(act); } // Update action trace, a total order of all actions diff --git a/execution.h b/execution.h index 54934891..d9a994f0 100644 --- a/execution.h +++ b/execution.h @@ -143,7 +143,7 @@ private: action_list_t action_trace; /** Per-object list of actions. Maps an object (i.e., memory location) - * to a trace of all actions performed on the object. + * to a trace of all actions performed on the object. * Used only for SC fences, unlocks, & wait. */ HashTable obj_map; diff --git a/funcnode.cc b/funcnode.cc index 663447bf..30b691df 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -349,7 +349,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) * @return true if branch found, false otherwise. */ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, -ModelAction * next_act, SnapVector * unset_predicates) + ModelAction * next_act, SnapVector * unset_predicates) { /* Check if a branch with func_inst and corresponding predicate exists */ bool branch_found = false; @@ -376,34 +376,34 @@ ModelAction * next_act, SnapVector * unset_predicates) bool equality; switch(pred_expression->token) { - case NOPREDICATE: - predicate_correct = true; - break; - case EQUALITY: - FuncInst * to_be_compared; - ModelAction * last_act; + case NOPREDICATE: + predicate_correct = true; + break; + case EQUALITY: + FuncInst * to_be_compared; + ModelAction * last_act; - to_be_compared = pred_expression->func_inst; - last_act = to_be_compared->get_associated_act(marker); + to_be_compared = pred_expression->func_inst; + last_act = to_be_compared->get_associated_act(marker); - last_read = last_act->get_reads_from_value(); - next_read = next_act->get_reads_from_value(); - equality = (last_read == next_read); - if (equality != pred_expression->value) - predicate_correct = false; + last_read = last_act->get_reads_from_value(); + next_read = next_act->get_reads_from_value(); + equality = (last_read == next_read); + if (equality != pred_expression->value) + predicate_correct = false; - break; - case NULLITY: - next_read = next_act->get_reads_from_value(); - // TODO: implement likely to be null - equality = ( (void*) (next_read & 0xffffffff) == NULL); - if (equality != pred_expression->value) - predicate_correct = false; - break; - default: + break; + case NULLITY: + next_read = next_act->get_reads_from_value(); + // TODO: implement likely to be null + equality = ( (void*) (next_read & 0xffffffff) == NULL); + if (equality != pred_expression->value) predicate_correct = false; - model_print("unkown predicate token\n"); - break; + break; + default: + predicate_correct = false; + model_print("unkown predicate token\n"); + break; } } @@ -419,8 +419,8 @@ ModelAction * next_act, SnapVector * unset_predicates) /* Infer predicate expressions, which are generated in FuncNode::generate_predicates */ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act, -HashTable * loc_act_map, -SnapVector * half_pred_expressions) + HashTable * loc_act_map, + SnapVector * half_pred_expressions) { void * loc = next_act->get_location(); @@ -465,7 +465,7 @@ SnapVector * half_pred_expressions) /* Able to generate complex predicates when there are multiple predciate expressions */ void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, -SnapVector * half_pred_expressions) + SnapVector * half_pred_expressions) { if (half_pred_expressions->size() == 0) { Predicate * new_pred = new Predicate(next_inst); @@ -744,7 +744,7 @@ void FuncNode::assign_base_score() leaves.push_back(node); } - for (uint i = 0; i < children->size(); i++) + for (uint i = 0;i < children->size();i++) queue.push_front( (*children)[i] ); } @@ -764,7 +764,7 @@ void FuncNode::assign_base_score() double weight_sum = 0; bool has_unassigned_node = false; - for (uint i = 0; i < children->size(); i++) { + for (uint i = 0;i < children->size();i++) { Predicate * child = (*children)[i]; // If a child has unassigned weight diff --git a/history.cc b/history.cc index 67f873b6..cc8f332a 100644 --- a/history.cc +++ b/history.cc @@ -398,7 +398,7 @@ WaitObj * ModelHistory::getWaitObj(thread_id_t tid) } void ModelHistory::add_waiting_thread(thread_id_t self_id, -thread_id_t waiting_for_id, FuncNode * target_node, int dist) + thread_id_t waiting_for_id, FuncNode * target_node, int dist) { WaitObj * self_wait_obj = getWaitObj(self_id); self_wait_obj->add_waiting_for(waiting_for_id, target_node, dist); @@ -426,7 +426,7 @@ void ModelHistory::remove_waiting_thread(thread_id_t tid) } void ModelHistory::stop_waiting_for_node(thread_id_t self_id, -thread_id_t waiting_for_id, FuncNode * target_node) + thread_id_t waiting_for_id, FuncNode * target_node) { WaitObj * self_wait_obj = getWaitObj(self_id); bool thread_removed = self_wait_obj->remove_waiting_for_node(waiting_for_id, target_node); diff --git a/newfuzzer.cc b/newfuzzer.cc index c9d3f177..9898ea59 100644 --- a/newfuzzer.cc +++ b/newfuzzer.cc @@ -93,7 +93,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector * rf_set * @return False if no child matches read_inst */ bool NewFuzzer::check_store_visibility(Predicate * curr_pred, FuncInst * read_inst, -inst_act_map_t * inst_act_map, SnapVector * rf_set) + inst_act_map_t * inst_act_map, SnapVector * rf_set) { available_branches_tmp_storage.clear(); @@ -191,7 +191,7 @@ Predicate * NewFuzzer::get_selected_child_branch(thread_id_t tid) * @return true if rf_set is pruned */ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred, -SnapVector * rf_set, inst_act_map_t * inst_act_map) + SnapVector * rf_set, inst_act_map_t * inst_act_map) { if (pred == NULL) return false; @@ -376,7 +376,7 @@ bool NewFuzzer::find_threads(ModelAction * pending_read) } bool NewFuzzer::check_predicate_expressions(PredExprSet * pred_expressions, -inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate) + inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate) { bool satisfy_predicate = true; @@ -386,31 +386,31 @@ inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate) bool equality; switch (expression->token) { - case NOPREDICATE: - *no_predicate = true; - break; - case EQUALITY: - FuncInst * to_be_compared; - ModelAction * last_act; - uint64_t last_read; - - to_be_compared = expression->func_inst; - last_act = inst_act_map->get(to_be_compared); - last_read = last_act->get_reads_from_value(); - - equality = (write_val == last_read); - if (equality != expression->value) - satisfy_predicate = false; - break; - case NULLITY: - // TODO: implement likely to be null - equality = ((void*) (write_val & 0xffffffff) == NULL); - if (equality != expression->value) - satisfy_predicate = false; - break; - default: - model_print("unknown predicate token\n"); - break; + case NOPREDICATE: + *no_predicate = true; + break; + case EQUALITY: + FuncInst * to_be_compared; + ModelAction * last_act; + uint64_t last_read; + + to_be_compared = expression->func_inst; + last_act = inst_act_map->get(to_be_compared); + last_read = last_act->get_reads_from_value(); + + equality = (write_val == last_read); + if (equality != expression->value) + satisfy_predicate = false; + break; + case NULLITY: + // TODO: implement likely to be null + equality = ((void*) (write_val & 0xffffffff) == NULL); + if (equality != expression->value) + satisfy_predicate = false; + break; + default: + model_print("unknown predicate token\n"); + break; } if (!satisfy_predicate) diff --git a/stl-model.h b/stl-model.h index cbcae7c0..a334c272 100644 --- a/stl-model.h +++ b/stl-model.h @@ -214,6 +214,33 @@ public: _size++; } + sllnode<_Tp>add_front(_Tp val) { + sllnode<_Tp> * tmp = new sllnode<_Tp>(); + tmp->prev = NULL; + tmp->next = head; + tmp->val = val; + if (head == NULL) + tail = tmp; + else + head->prev = tmp; + head = tmp; + _size++; + return tmp; + } + + sllnode<_Tp> * add_back(_Tp val) { + sllnode<_Tp> * tmp = new sllnode<_Tp>(); + tmp->prev = tail; + tmp->next = NULL; + tmp->val = val; + if (tail == NULL) + head = tmp; + else tail->next = tmp; + tail = tmp; + _size++; + return tmp; + } + void pop_front() { sllnode<_Tp> *tmp = head; head = head->next;