ongoing work on preconditions (parse, lex, sema)
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -46,6 +46,7 @@ add_custom_command(OUTPUT "${CMAKE_BINARY_DIR}/tools/alive_lexer.cpp"
include_directories(${PROJECT_SOURCE_DIR})
set(IR_SRC
+ ir/constant.cpp
ir/function.cpp
ir/instr.cpp
ir/state.cpp

ADD
ir/constant.cpp
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "ir/constant.h"
+#include "smt/expr.h"
+#include "util/compiler.h"
+#include <cassert>
+
+using namespace smt;
+using namespace std;
+
+namespace IR {
+
+void Constant::print(ostream &os) const {
+ UNREACHABLE();
+}
+
+pair<expr, expr> Constant::toSMT_cnst() const {
+ return { expr::mkVar(getName().c_str(), bits()), true };
+}
+
+StateValue Constant::toSMT(State &s) const {
+ auto ret = toSMT_cnst();
+ s.addUB(move(ret.second));
+ return { move(ret.first), true };
+}
+
+
+ConstantBinOp::ConstantBinOp(Type &type, Constant &lhs, Constant &rhs, Op op)
+ : Constant(type, ""), lhs(lhs), rhs(rhs), op(op) {
+ const char *opname = nullptr;
+ switch (op) {
+ case ADD: opname = " + "; break;
+ case SUB: opname = " - "; break;
+ case SDIV: opname = " / "; break;
+ case UDIV: opname = " /u "; break;
+ }
+
+ string str = '(' + this->lhs.getName();
+ str += opname;
+ str += rhs.getName();
+ str += ')';
+ this->setName(move(str));
+}
+
+static void div_ub(const expr &a, const expr &b, expr &ub, bool sign) {
+ auto bits = b.bits();
+ ub &= b != expr::mkUInt(0, bits);
+ if (sign)
+ ub &= (a != expr::IntMin(bits) || b != expr::mkInt(-1, bits));
+}
+
+pair<expr, expr> ConstantBinOp::toSMT_cnst() const {
+ auto a = lhs.toSMT_cnst();
+ auto b = rhs.toSMT_cnst();
+ auto ub = move(a.second) && move(b.second);
+ expr val;
+
+ switch (op) {
+ case ADD: val = a.first + b.first; break;
+ case SUB: val = a.first - b.first; break;
+ case SDIV:
+ val = a.first.sdiv(b.first);
+ div_ub(a.first, b.first, ub, true);
+ break;
+ case UDIV:
+ val = a.first.udiv(b.first);
+ div_ub(a.first, b.first, ub, false);
+ break;
+ }
+ return { move(val), move(ub) };
+}
+
+expr ConstantBinOp::getTypeConstraints() const {
+ return Value::getTypeConstraints() &&
+ getType().enforceIntType() &&
+ getType() == lhs.getType() &&
+ getType() == rhs.getType();
+}
+
+
+ConstantFn::ConstantFn(Type &type, string_view name, vector<Value*> &&args) :
+ Constant(type, ""), args(move(args)) {
+ unsigned num_args;
+ if (name == "log2") {
+ fn = LOG2;
+ num_args = 1;
+ } else if (name == "width") {
+ fn = WIDTH;
+ num_args = 1;
+ } else {
+ throw ConstantFnException("Unknown function: " + string(name));
+ }
+
+ auto actual_args = this->args.size();
+ if (actual_args != num_args)
+ throw ConstantFnException("Expected " + to_string(num_args) +
+ " parameter for " + string(name) + ", but got " +
+ to_string(actual_args));
+
+ string str = string(name) + '(';
+ bool first = true;
+ for (auto arg : this->args) {
+ if (!first)
+ str += ", ";
+ first = false;
+ str += arg->getName();
+ }
+ str += ')';
+ this->setName(move(str));
+}
+
+pair<expr, expr> ConstantFn::toSMT_cnst() const {
+ return { expr() /* TODO */, true };
+}
+
+
+void BoolPred::print(ostream &os) const {
+ os << '(';
+ lhs.print(os);
+ os << ") " << (pred == AND ? "&&" : "||") << " (";
+ rhs.print(os);
+ os << ')';
+}
+
+expr BoolPred::toSMT() const {
+ auto a = lhs.toSMT();
+ auto b = rhs.toSMT();
+ switch (pred) {
+ case AND: return a && b;
+ case OR: return a || b;
+ }
+ UNREACHABLE();
+}
+
+
+void CmpPred::print(ostream &os) const {
+ // TODO
+}
+
+expr CmpPred::toSMT() const {
+ return expr() /* TODO */;
+}
+
+}

ADD
ir/constant.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "ir/value.h"
+#include <string>
+#include <string_view>
+#include <utility>
+#include <vector>
+
+namespace IR {
+
+class Constant : public Value {
+public:
+ Constant(Type &type, std::string &&name) : Value(type, std::move(name)) {}
+ void print(std::ostream &os) const override;
+ // <value, UB>
+ virtual std::pair<smt::expr, smt::expr> toSMT_cnst() const;
+ StateValue toSMT(State &s) const override;
+};
+
+
+class ConstantBinOp final : public Constant {
+public:
+ enum Op { ADD, SUB, SDIV, UDIV };
+
+private:
+ Constant &lhs, &rhs;
+ Op op;
+
+public:
+ ConstantBinOp(Type &type, Constant &lhs, Constant &rhs, Op op);
+ std::pair<smt::expr, smt::expr> toSMT_cnst() const override;
+ smt::expr getTypeConstraints() const override;
+};
+
+
+class ConstantFn final : public Constant {
+ enum Fn { LOG2, WIDTH } fn;
+ std::vector<Value*> args;
+
+public:
+ ConstantFn(Type &type, std::string_view name, std::vector<Value*> &&args);
+ std::pair<smt::expr, smt::expr> toSMT_cnst() const override;
+};
+
+struct ConstantFnException {
+ std::string str;
+ ConstantFnException(std::string &&str) : str(std::move(str)) {}
+};
+
+
+class Predicate {
+public:
+ virtual void print(std::ostream &os) const = 0;
+ virtual smt::expr toSMT() const = 0;
+};
+
+
+class BoolPred final : public Predicate {
+public:
+ enum Pred { AND, OR };
+
+private:
+ Predicate &lhs, &rhs;
+ Pred pred;
+
+public:
+ BoolPred(Predicate &lhs, Predicate &rhs, Pred pred)
+ : lhs(lhs), rhs(rhs), pred(pred) {}
+ void print(std::ostream &os) const override;
+ smt::expr toSMT() const override;
+};
+
+
+class CmpPred final : public Predicate {
+public:
+ enum Pred { EQ, NE, SLE, SLT, SGE, SGT, ULE, ULT, UGE, UGT };
+
+private:
+ Constant &lhs, &rhs;
+ Pred pred;
+
+public:
+ CmpPred(Constant &lhs, Constant &rhs, Pred pred)
+ : lhs(lhs), rhs(rhs), pred(pred) {}
+ void print(std::ostream &os) const override;
+ smt::expr toSMT() const override;
+};
+
+}

MODIFY
ir/function.cpp
ir/function.cpp
@@ -78,6 +78,10 @@ void Function::addConstant(unique_ptr<Value> &&c) {
constants.emplace_back(move(c));
}
+void Function::addPredicate(unique_ptr<Predicate> &&p) {
+ predicates.emplace_back(move(p));
+}
+
void Function::addUndef(unique_ptr<UndefValue> &&u) {
undefs.emplace_back(move(u));
}

MODIFY
ir/function.h
ir/function.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include "ir/constant.h"
#include "ir/instr.h"
#include "ir/value.h"
#include "smt/expr.h"
@@ -47,9 +48,11 @@ class Function {
std::string name;
std::unordered_map<std::string, BasicBlock> BBs;
std::vector<BasicBlock*> BB_order;
+ Predicate *precondition = nullptr;
// constants used in this function
std::vector<std::unique_ptr<Value>> constants;
+ std::vector<std::unique_ptr<Predicate>> predicates;
std::vector<std::unique_ptr<Value>> undefs;
std::vector<std::unique_ptr<Value>> inputs;
@@ -72,6 +75,8 @@ public:
return constants;
}
+ void addPredicate(std::unique_ptr<Predicate> &&p);
+
void addUndef(std::unique_ptr<UndefValue> &&c);
util::const_strip_unique_ptr<decltype(undefs)> getUndefs() const {
return undefs;

MODIFY
ir/value.h
ir/value.h
@@ -21,6 +21,7 @@ protected:
Value(Type &type, std::string &&name)
: type(type), name(std::move(name)) {}
+ void setName(std::string &&str) { name = std::move(str); }
static std::string fresh_id();
public:

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -21,7 +21,7 @@ using namespace std;
static const YYCTYPE *YYCURSOR;
static const YYCTYPE *YYLIMIT;
static const YYCTYPE *YYTEXT;
-static const YYCTYPE *YYMARKER;
+//static const YYCTYPE *YYMARKER;
static const YYCTYPE *tag1, *yyt1;
#if 0
@@ -109,7 +109,12 @@ re2c:yyfill:check = 0;
"%" [a-zA-Z0-9_.]+ {
COPY_STR();
- return IDENTIFIER;
+ return REGISTER;
+}
+
+"C" [0-9]+ {
+ COPY_STR();
+ return CONSTANT;
}
"=" {
@@ -129,6 +134,19 @@ re2c:yyfill:check = 0;
return LABEL;
}
+"(" { return LPAREN; }
+")" { return RPAREN; }
+"+" { return PLUS; }
+"*" { return STAR; }
+"&&" { return BAND; }
+"||" { return BOR; }
+"==" { return CEQ; }
+"!=" { return CNE; }
+">" { return CSGT; }
+"<" { return CSLT; }
+">u" { return CUGT; }
+"<u" { return CULT; }
+
"true" { return TRUE; }
"false" { return FALSE; }
"undef" { return UNDEF; }
@@ -169,6 +187,11 @@ re2c:yyfill:check = 0;
"ret" { return RETURN; }
"unreachable" { return UNREACH; }
+[a-zA-Z][a-zA-Z0-9]* {
+ COPY_STR();
+ return IDENTIFIER;
+}
+
* { error("couldn't parse: '" + string((char*)YYTEXT, 16) + '\''); }
*/

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "tools/alive_parser.h"
+#include "ir/constant.h"
#include "ir/value.h"
#include "tools/alive_lexer.h"
#include "util/compiler.h"
@@ -27,6 +28,11 @@ static void error(string &&s) {
throw ParseException(move(s), yylineno);
}
+static void error(const char *s, token t) {
+ throw ParseException(string(s) + "; got: " + token_name[t], yylineno);
+}
+
+static vector<unique_ptr<IntType>> int_types;
static unordered_map<string, Value*> identifiers;
static Function *fn;
@@ -37,6 +43,19 @@ static Value& get_constant(uint64_t n, Type &t) {
return *ret;
}
+static Value& get_constant(string_view name, Type &type) {
+ string id(name);
+ if (auto I = identifiers.find(id);
+ I != identifiers.end())
+ return *I->second;
+
+ auto c = make_unique<Constant>(type, string(id));
+ auto ret = c.get();
+ fn->addConstant(move(c));
+ identifiers.emplace(move(id), ret);
+ return *ret;
+}
+
struct tokenizer_t {
token last;
@@ -106,10 +125,82 @@ static void parse_name(Transform &t) {
t.name = yylval.str;
}
+static Value& parse_const_expr(Type &type);
+
+static Predicate* parse_predicate(Predicate *last = nullptr,
+ token last_t = END) {
+ switch (auto t = *tokenizer) {
+ case LPAREN: {
+ auto newpred = parse_predicate();
+ tokenizer.ensure(RPAREN);
+ if (last == nullptr) {
+parse_more:
+ switch (auto t = *tokenizer) {
+ case BAND:
+ case BOR:
+ return parse_predicate(newpred, t);
+ default:
+ tokenizer.unget(t);
+ return newpred;
+ }
+ }
+
+ if (last_t == BAND) {
+ auto p = make_unique<BoolPred>(*last, *newpred, BoolPred::AND);
+ newpred = p.get();
+ fn->addPredicate(move(p));
+ goto parse_more;
+ }
+
+ assert(last_t == BOR);
+
+ switch (auto t = *tokenizer) {
+ case BAND: {
+ newpred = parse_predicate(newpred, BAND);
+ auto p = make_unique<BoolPred>(*last, *newpred, BoolPred::OR);
+ auto ret = p.get();
+ fn->addPredicate(move(p));
+ return ret;
+ }
+
+ case BOR: {
+ auto p = make_unique<BoolPred>(*last, *newpred, BoolPred::OR);
+ auto ret = p.get();
+ fn->addPredicate(move(p));
+ return parse_predicate(ret, BOR);
+ }
+
+ default: {
+ tokenizer.unget(t);
+ auto p = make_unique<BoolPred>(*last, *newpred,
+ last_t == BAND ? BoolPred::AND :
+ BoolPred::OR);
+ auto ret = p.get();
+ fn->addPredicate(move(p));
+ return ret;
+ }
+ }
+ break;
+ }
+ case IDENTIFIER:
+ //TODO
+ break;
+
+ case CONSTANT:
+ //TODO
+ parse_const_expr(*int_types[64].get());
+ break;
+
+ default:
+ error("Expected predicate", t);
+ }
+ UNREACHABLE();
+}
+
static void parse_pre(Transform &t) {
if (!tokenizer.consumeIf(PRE))
return;
- // TODO
+ parse_predicate();
}
static void parse_comma() {
@@ -117,7 +208,6 @@ static void parse_comma() {
}
-static vector<unique_ptr<IntType>> int_types;
static vector<unique_ptr<SymbolicType>> sym_types;
static unsigned sym_num;
@@ -137,19 +227,53 @@ static Type& parse_type(bool optional = true) {
auto t = make_unique<SymbolicType>("symty_" + to_string(sym_num++));
return *sym_types.emplace_back(move(t)).get();
} else {
- error(string("Expecting a type, got: ") + token_name[t]);
+ error("Expecting a type", t);
}
}
UNREACHABLE();
}
+static Value& parse_operand(Type &type);
+
+static Value& parse_const_expr(Type &type) {
+ switch (auto t = *tokenizer) {
+ case LPAREN: {
+ auto &ret = parse_const_expr(type);
+ tokenizer.ensure(RPAREN);
+ return ret;
+ }
+ case CONSTANT:
+ return get_constant(yylval.str, type);
+ case IDENTIFIER: {
+ string_view name = yylval.str;
+ std::vector<Value*> args;
+ tokenizer.ensure(LPAREN);
+ if (!tokenizer.consumeIf(RPAREN)) {
+ do {
+ args.push_back(&parse_operand(parse_type()));
+ } while (tokenizer.consumeIf(COMMA));
+ tokenizer.ensure(RPAREN);
+ }
+ try {
+ auto f = make_unique<ConstantFn>(type, name, move(args));
+ auto ret = f.get();
+ fn->addConstant(move(f));
+ return *ret;
+ } catch (ConstantFnException &e) {
+ error(move(e.str));
+ }
+ }
+ default:
+ error("Expected constant expression", t);
+ }
+ UNREACHABLE();
+}
+
static Value& parse_operand(Type &type) {
switch (auto t = *tokenizer) {
case NUM:
- // FIXME: constraint type to int
return get_constant(yylval.num, type);
case TRUE:
- // FIXME: constrain types below to boolean
return get_constant(1, type);
case FALSE:
return get_constant(0, type);
@@ -165,7 +289,7 @@ static Value& parse_operand(Type &type) {
fn->addConstant(move(val));
return *ret;
}
- case IDENTIFIER: {
+ case REGISTER: {
string id(yylval.str);
if (auto I = identifiers.find(id);
I != identifiers.end())
@@ -177,8 +301,13 @@ static Value& parse_operand(Type &type) {
identifiers.emplace(move(id), ret);
return *ret;
}
+ case CONSTANT:
+ case IDENTIFIER:
+ case LPAREN:
+ tokenizer.unget(t);
+ return parse_const_expr(type);
default:
- error(string("Expected an operand, got: ") + token_name[t]);
+ error("Expected an operand", t);
}
UNREACHABLE();
}
@@ -360,10 +489,10 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case FALSE:
case UNDEF:
case POISON:
- case IDENTIFIER:
+ case REGISTER:
return parse_copyop(name, t);
default:
- error(string("Expected instruction name; got: ") + token_name[t]);
+ error("Expected instruction name", t);
}
UNREACHABLE();
}
@@ -382,7 +511,7 @@ static void parse_fn(Function &f) {
while (true) {
switch (auto t = *tokenizer) {
- case IDENTIFIER: {
+ case REGISTER: {
string name(yylval.str);
auto i = parse_instr(name);
identifiers.emplace(move(name), i.get());

MODIFY
tools/tokens.h
tools/tokens.h
@@ -6,7 +6,16 @@ TOKEN(ADD)
TOKEN(AND)
TOKEN(ARROW)
TOKEN(ASHR)
+TOKEN(BAND)
+TOKEN(BOR)
TOKEN(COMMA)
+TOKEN(CONSTANT)
+TOKEN(CEQ)
+TOKEN(CNE)
+TOKEN(CSLT)
+TOKEN(CSGT)
+TOKEN(CULT)
+TOKEN(CUGT)
TOKEN(EQ)
TOKEN(EQUALS)
TOKEN(EXACT)
@@ -16,6 +25,7 @@ TOKEN(ICMP)
TOKEN(IDENTIFIER)
TOKEN(INT_TYPE)
TOKEN(LABEL)
+TOKEN(LPAREN)
TOKEN(LSHR)
TOKEN(MUL)
TOKEN(NAME)
@@ -24,9 +34,12 @@ TOKEN(NSW)
TOKEN(NUM)
TOKEN(NUW)
TOKEN(OR)
+TOKEN(PLUS)
TOKEN(POISON)
TOKEN(PRE)
+TOKEN(REGISTER)
TOKEN(RETURN)
+TOKEN(RPAREN)
TOKEN(SDIV)
TOKEN(SELECT)
TOKEN(SEXT)
@@ -36,6 +49,7 @@ TOKEN(SHL)
TOKEN(SLE)
TOKEN(SLT)
TOKEN(SREM)
+TOKEN(STAR)
TOKEN(SUB)
TOKEN(TO)
TOKEN(TRUE)

ongoing work on preconditions (parse, lex, sema)