Skip to content

Commit

Permalink
Removed deputy since it becomes irrelevant to the goals of Csmith
Browse files Browse the repository at this point in the history
  • Loading branch information
jxyang committed Jun 5, 2017
1 parent a26a738 commit 9071d83
Show file tree
Hide file tree
Showing 8 changed files with 1 addition and 159 deletions.
2 changes: 0 additions & 2 deletions src/ArrayVariable.cpp
Expand Up @@ -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
Expand Down
2 changes: 0 additions & 2 deletions src/CGOptions.cpp
Expand Up @@ -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)
Expand Down Expand Up @@ -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);
Expand Down
4 changes: 0 additions & 4 deletions src/CGOptions.h
Expand Up @@ -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);

Expand Down Expand Up @@ -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_;
Expand Down
30 changes: 0 additions & 30 deletions src/CVQualifiers.cpp
Expand Up @@ -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<string>& 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; i<is_consts.size(); i++) {
if (i>0) {
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
{
Expand Down
1 change: 0 additions & 1 deletion src/CVQualifiers.h
Expand Up @@ -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<string>& annotations) const;
void output() const;
void OutputFirstQuals(std::ostream &out) const;

Expand Down
5 changes: 0 additions & 5 deletions src/RandomProgramGenerator.cpp
Expand Up @@ -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++;
Expand Down
115 changes: 1 addition & 114 deletions src/Variable.cpp
Expand Up @@ -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<string>
Variable::deputy_annotation(void) const
{
size_t len;
int pos, i, j;
vector<string> 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<static_cast<int>(FactPointTo::all_ptrs.size()); i++) {
if (FactPointTo::all_ptrs[i] == tmp) {
pos = i;
break;
}
}
if (pos == -1) break;
vector<const Variable*> 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<static_cast<int>(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; j<av->get_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; i<prepend; i++) {
if (null_based) {
annotations.insert(annotations.begin(), "SAFE");
} else {
annotations.insert(annotations.begin(), "BOUND(__auto, __auto)");
}
}
return annotations;
}

const Variable*
Variable::get_collective(void) const
{
Expand Down Expand Up @@ -855,13 +748,7 @@ Variable::OutputForComment(std::ostream &out) const
void
Variable::output_qualified_type(std::ostream &out) const
{
if (type->eType == ePointer && CGOptions::deputy()) {
vector<string> 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);
}

// --------------------------------------------------------------
Expand Down
1 change: 0 additions & 1 deletion src/Variable.h
Expand Up @@ -108,7 +108,6 @@ class Variable

virtual std::string get_actual_name() const;
std::string to_string(void) const;
std::vector<std::string> deputy_annotation(void) const;

// ISSUE: we treat volatiles specially
bool compatible(const Variable *v) const;
Expand Down

0 comments on commit 9071d83

Please sign in to comment.