Skip to content

Commit

Permalink
Merge branch 'sat_solver_domain_with_array'
Browse files Browse the repository at this point in the history
  • Loading branch information
@jsalzbergedu
jsalzbergedu committed Apr 13, 2022
2 parents ec9f4e3 + 3686b58 commit a788768
Show file tree
Hide file tree
Showing 12 changed files with 1,974 additions and 287 deletions.
123 changes: 118 additions & 5 deletions parser/blinkenlights/blinkenlights.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,17 +29,30 @@ def new_variableno(con):
def new_constantno(con):
return new_no(con, "id", "constant")

def new_assertno(con):
return new_no(con, "id", "assertion")

def parse_expr_dispatch(con, pycobj):
if type(pycobj) == pycparser.c_ast.ID:
return parse_id(con, pycobj)
elif type(pycobj) == pycparser.c_ast.Constant:
return parse_constant(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '>=':
return parse_ge(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '+':
return parse_plus(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '>':
return parse_gt(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '>=':
return parse_ge(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '<=':
return parse_le(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '<':
return parse_lt(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '==':
return parse_eq(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '||':
return parse_or(con, pycobj)
elif type(pycobj) == pycparser.c_ast.BinaryOp and pycobj.op == '&&':
return parse_and(con, pycobj)
else:
raise ValueError(type(pycobj).__name__ + " not yet implemented")

Expand Down Expand Up @@ -99,6 +112,51 @@ def parse_gt(con, pycbinop):
con.commit()
return exprno

def parse_le(con, pycbinop):
exprno = new_exprno(con)
con.execute('''insert into expr values (:kind, :idt)''',
{"kind": "le", "idt": exprno})
left_child = parse_expr_dispatch(con, pycbinop.left)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 0, "child": left_child})
right_child = parse_expr_dispatch(con, pycbinop.right)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 1, "child": right_child})
con.commit()
return exprno

def parse_lt(con, pycbinop):
exprno = new_exprno(con)
con.execute('''insert into expr values (:kind, :idt)''',
{"kind": "lt", "idt": exprno})
left_child = parse_expr_dispatch(con, pycbinop.left)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 0, "child": left_child})
right_child = parse_expr_dispatch(con, pycbinop.right)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 1, "child": right_child})
con.commit()
return exprno

def parse_eq(con, pycbinop):
exprno = new_exprno(con)
con.execute('''insert into expr values (:kind, :idt)''',
{"kind": "eq", "idt": exprno})
left_child = parse_expr_dispatch(con, pycbinop.left)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 0, "child": left_child})
right_child = parse_expr_dispatch(con, pycbinop.right)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 1, "child": right_child})
con.commit()
return exprno

def parse_plus(con, pycbinop):
exprno = new_exprno(con)
con.execute('''insert into expr values (:kind, :idt)''',
Expand All @@ -114,6 +172,36 @@ def parse_plus(con, pycbinop):
con.commit()
return exprno

def parse_or(con, pycbinop):
exprno = new_exprno(con)
con.execute('''insert into expr values (:kind, :idt)''',
{"kind": "||", "idt": exprno})
left_child = parse_expr_dispatch(con, pycbinop.left)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 0, "child": left_child})
right_child = parse_expr_dispatch(con, pycbinop.right)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 1, "child": right_child})
con.commit()
return exprno

def parse_and(con, pycbinop):
exprno = new_exprno(con)
con.execute('''insert into expr values (:kind, :idt)''',
{"kind": "&&", "idt": exprno})
left_child = parse_expr_dispatch(con, pycbinop.left)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 0, "child": left_child})
right_child = parse_expr_dispatch(con, pycbinop.right)
childid = new_expr_childno(con)
con.execute('''insert into expr_children values (:idt, :expr, :idx, :child)''',
{"idt": childid, "expr": exprno, "idx": 1, "child": right_child})
con.commit()
return exprno

def parse_dispatch(pycobj, con):
if type(pycobj) == pycparser.c_ast.Compound:
return parse_compound(pycobj, con)
Expand All @@ -127,6 +215,8 @@ def parse_dispatch(pycobj, con):
return parse_while(pycobj, con)
elif type(pycobj) == pycparser.c_ast.Assignment:
return parse_assign(pycobj, con)
elif type(pycobj) == pycparser.c_ast.FuncCall and pycobj.name and pycobj.name.name == "assert":
return parse_assert(pycobj, con)
elif type(pycobj) == pycparser.c_ast.Decl:
return parse_decl(pycobj, con)
else:
Expand Down Expand Up @@ -241,6 +331,22 @@ def parse_while(pycwhile, con):
con.commit()
return idno

def parse_assert(pycassert, con):
# Kludge: treat the assert as an empty statement list.
# This means that assert will define the invariant at after[sl]
# and moreover that the assertion table will collect the appropriate exprs.
idno = parse_pycobj(pycassert, "compound", con)
child = parse_compound_rec(idno, (), con)
childid = new_childno(con)
con.execute('''insert into children values (:idt, :node, :idx, :child)''',
{"idt": childid, "node": idno, "idx": 0, "child": child})
con.commit()
child = parse_expr_dispatch(con, pycassert.args.exprs[0])
assertion = new_assertno(con)
con.execute('''insert into assertion values (:idt, :node, :expr)''',
{"idt": assertion, "node": idno, "expr": child})
return idno

def parse_ifthen(pycifthen, con):
idno = parse_pycobj(pycifthen, "ifthen", con)
child = parse_expr_dispatch(con, pycifthen.cond)
Expand Down Expand Up @@ -305,20 +411,27 @@ def dispatch_command(command, con):
else:
raise ValueError("Command ", command, "not handled")

def setup_con():
con = sqlite3.connect('analysis.db')
def setup_con(db_name):
con = sqlite3.connect(db_name)
con.execute('''CREATE TABLE IF NOT EXISTS node (kind text, id integer, PRIMARY KEY (id))''')
con.execute('''CREATE TABLE IF NOT EXISTS fileinfo (id integer, filename text, column integer, line integer, node integer, PRIMARY KEY (id))''')
con.execute('''CREATE TABLE IF NOT EXISTS children (id integer, node integer, idx integer, child integer, PRIMARY KEY (id))''')
con.execute('''CREATE TABLE IF NOT EXISTS expr (kind text, id integer, PRIMARY KEY (id))''')
con.execute('''CREATE TABLE IF NOT EXISTS expr_children (id integer, expr integer, idx integer, child integer, PRIMARY KEY (id))''')
con.execute('''CREATE TABLE IF NOT EXISTS variable (id integer, name text, PRIMARY KEY (id))''')
con.execute('''CREATE TABLE IF NOT EXISTS constant (id integer, constant integer, PRIMARY KEY (id))''')
con.execute('''CREATE TABLE IF NOT EXISTS assertion (id integer, node integer, expr integer, PRIMARY KEY (id))''')
con.commit()
return con

if __name__ == '__main__':
con = setup_con()
db_name = None
if len(sys.argv) > 1:
print("writing to database, ", sys.argv[1])
db_name = sys.argv[1]
else:
db_name = "analysis.db"
con = setup_con(db_name)
while True:
line = sys.stdin.read()
if not line:
Expand Down
2 changes: 1 addition & 1 deletion parser/test/test_blinkenlights.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ class TestBlinkenlights(object):

@classmethod
def setup_class(cls):
cls.con = blinkenlights.setup_con()
cls.con = blinkenlights.setup_con("analysis.db")
return

def test_basic_parse(self):
Expand Down
3 changes: 3 additions & 0 deletions server/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,9 @@ serde_json = "1.0"
mktemp = "0.4.1"
serde_rusqlite = "0.29.0"
rusqlite = "0.26.0"
z3 = "0.11.2"
z3-sys = "0.7.1"
lazy_static = "1.4.0"

[[bin]]
name = "blinkenlights-server"
Expand Down
Loading

0 comments on commit a788768

Please sign in to comment.