From 9071d83340128279e8da1e84152564b8456c9003 Mon Sep 17 00:00:00 2001 From: jxyang Date: Sun, 4 Jun 2017 21:19:21 -0700 Subject: [PATCH] Removed deputy since it becomes irrelevant to the goals of Csmith --- src/ArrayVariable.cpp | 2 - src/CGOptions.cpp | 2 - src/CGOptions.h | 4 -- src/CVQualifiers.cpp | 30 --------- src/CVQualifiers.h | 1 - src/RandomProgramGenerator.cpp | 5 -- src/Variable.cpp | 115 +-------------------------------- src/Variable.h | 1 - 8 files changed, 1 insertion(+), 159 deletions(-) diff --git a/src/ArrayVariable.cpp b/src/ArrayVariable.cpp index e79552405..9d934b244 100644 --- a/src/ArrayVariable.cpp +++ b/src/ArrayVariable.cpp @@ -447,8 +447,6 @@ ArrayVariable::is_visible_local(const Block* blk) const bool ArrayVariable::no_loop_initializer(void) const { - // don't use loop initializer if we are outputing deputy annotations - if (CGOptions::deputy()) return true; // don't use loop initializer if we are doing test case reduction // if (CGOptions::get_reducer()) return true; // can not use loop initializer if either array member are structs, or they are constants, or it has > 1 initial values diff --git a/src/CGOptions.cpp b/src/CGOptions.cpp index 7f225763b..6c9d3dcad 100644 --- a/src/CGOptions.cpp +++ b/src/CGOptions.cpp @@ -165,7 +165,6 @@ DEFINE_GETTER_SETTER_BOOL(muls) DEFINE_GETTER_SETTER_BOOL(accept_argc) DEFINE_GETTER_SETTER_BOOL(random_random) DEFINE_GETTER_SETTER_INT(stop_by_stmt) -DEFINE_GETTER_SETTER_BOOL(deputy) DEFINE_GETTER_SETTER_BOOL(step_hash_by_stmt) DEFINE_GETTER_SETTER_BOOL(compound_assignment) DEFINE_GETTER_SETTER_STRING_REF(dump_default_probabilities) @@ -281,7 +280,6 @@ CGOptions::set_default_settings(void) muls(true); accept_argc(true); stop_by_stmt(-1); - deputy(false); step_hash_by_stmt(false); const_as_condition(false); match_exact_qualifiers(false); diff --git a/src/CGOptions.h b/src/CGOptions.h index 739d15ac2..b613ae582 100644 --- a/src/CGOptions.h +++ b/src/CGOptions.h @@ -351,9 +351,6 @@ class CGOptions { static void monitored_funcs(string fnames); - static bool deputy(void); - static bool deputy(bool p); - static bool const_as_condition(void); static bool const_as_condition(bool p); @@ -519,7 +516,6 @@ class CGOptions { static bool nomain_; static bool compound_assignment_; static int stop_by_stmt_; - static bool deputy_; static bool step_hash_by_stmt_; static bool blind_check_global_; static bool random_based_; diff --git a/src/CVQualifiers.cpp b/src/CVQualifiers.cpp index 0c61cfef4..2219d921d 100644 --- a/src/CVQualifiers.cpp +++ b/src/CVQualifiers.cpp @@ -606,36 +606,6 @@ CVQualifiers::output_qualified_type(const Type* t, std::ostream &out) const } } -void -CVQualifiers::output_qualified_type_with_deputy_annotation(const Type* t, std::ostream &out, const vector& annotations) const -{ - assert(t); - assert(sanity_check(t)); - assert(is_consts.size() == annotations.size()+1); - size_t i; - const Type* base = t->get_base_type(); - for (i=0; i0) { - out << "* "; - out << annotations[i-1] << " "; - } - if (is_consts[i]) { - if (!CGOptions::consts()) - assert(0); - out << "const "; - } - if (is_volatiles[i]) { - if (!CGOptions::volatiles()) - assert(0); - out << "volatile "; - } - if (i==0) { - base->Output(out); - out << " "; - } - } -} - bool CVQualifiers::is_const_after_deref(int deref_level) const { diff --git a/src/CVQualifiers.h b/src/CVQualifiers.h index 5c6edc9d1..b2b4b5b62 100644 --- a/src/CVQualifiers.h +++ b/src/CVQualifiers.h @@ -87,7 +87,6 @@ class CVQualifiers bool sanity_check(const Type* t) const; void output_qualified_type(const Type* t, std::ostream &out) const; - void output_qualified_type_with_deputy_annotation(const Type* t, std::ostream &out, const vector& annotations) const; void output() const; void OutputFirstQuals(std::ostream &out) const; diff --git a/src/RandomProgramGenerator.cpp b/src/RandomProgramGenerator.cpp index 87d710379..6b476a94c 100644 --- a/src/RandomProgramGenerator.cpp +++ b/src/RandomProgramGenerator.cpp @@ -1057,11 +1057,6 @@ main(int argc, char **argv) continue; } - if (strcmp (argv[i], "--deputy") == 0) { - CGOptions::deputy(true); - continue; - } - if (strcmp (argv[i], "--delta-input") == 0) { string filename; i++; diff --git a/src/Variable.cpp b/src/Variable.cpp index da6c76433..c42d96cab 100644 --- a/src/Variable.cpp +++ b/src/Variable.cpp @@ -597,113 +597,6 @@ Variable::is_volatile_after_deref(int deref_level) const return false; } -/* - * return an array deputy annotation for each level of indirection of a pointer based on it's point-to set - * for non-pointers, return an empty set - */ -vector -Variable::deputy_annotation(void) const -{ - size_t len; - int pos, i, j; - vector annotations; - const Variable* tmp = this; - bool has_null = false; - bool null_based = false; - if (name == "p_24") - i = 0; - while (tmp && tmp->type->eType == ePointer) { - pos = -1; - string anno; - for (i=0; i(FactPointTo::all_ptrs.size()); i++) { - if (FactPointTo::all_ptrs[i] == tmp) { - pos = i; - break; - } - } - if (pos == -1) break; - vector set = FactPointTo::all_aliases[pos]; - // take out tbd in point-to-set for parameters - j = find_variable_in_set(set, FactPointTo::tbd_ptr); - if (set.size() > 1 && j != -1) { - set.erase(set.begin() + j); - } - bool has_array = false; - len = set.size(); - for (j=0; j(len); j++) { - if (set[j] == FactPointTo::null_ptr) { - // remove null pointer from set - has_null = true; - set.erase(set.begin() + j); - j--; - len--; - } - else if (set[j]->isArray || set[j]->is_array_field()) { - has_array = true; - } - } - /* if "int *** p = 0", we can annotate it as "int * SAFE * SAFE * SAFE p" */ - if (len == 0 && has_null) { - null_based = true; - } - if (!has_array) { - anno = (has_null ? "SAFE" : "SAFE NONNULL"); - // special handling to satisfy deputy, no "NONNULL" for array of pointers - if (tmp->isArray || tmp->is_array_field()) { - anno = "SAFE"; - } - } - tmp = 0; - - if (len == 1) { - const Variable* pointee = set[0]; - if (pointee->isArray || pointee->is_array_field()) { - ostringstream oss; - oss << "BOUND(&"; - pointee->OutputLowerBound(oss); - oss << ", &"; - pointee->OutputUpperBound(oss); - oss << ")"; - anno = oss.str(); - } - //if (pointee->is_array_field()) { - // while (pointee->field_var_of) { - // pointee = pointee->field_var_of; - // } - // assert(pointee->isArray); - //} - //// pointing to an array - //if (pointee->isArray) { - // const ArrayVariable* av = (const ArrayVariable*)pointee; - // ostringstream oss; - // oss << "COUNT("; - // for (j=0; jget_dimension(); j++) { - // if (j > 0) oss << " * "; - // oss << av->get_sizes()[j]; - // } - // oss << ")"; - // anno = oss.str(); - //} - if (pointee->type && pointee->type->eType == ePointer) { - tmp = pointee; - } - } - if (anno == "") { - anno = "BOUND(__auto, __auto)"; - } - annotations.insert(annotations.begin(), anno); - } - int prepend = type->get_indirect_level() - annotations.size(); - for (i=0; ieType == ePointer && CGOptions::deputy()) { - vector annotations = deputy_annotation(); - qfer.output_qualified_type_with_deputy_annotation(type, out, annotations); - } - else { - qfer.output_qualified_type(type, out); - } + qfer.output_qualified_type(type, out); } // -------------------------------------------------------------- diff --git a/src/Variable.h b/src/Variable.h index 74b294f57..caccb7d7b 100644 --- a/src/Variable.h +++ b/src/Variable.h @@ -108,7 +108,6 @@ class Variable virtual std::string get_actual_name() const; std::string to_string(void) const; - std::vector deputy_annotation(void) const; // ISSUE: we treat volatiles specially bool compatible(const Variable *v) const;