From 16bf7f2a11bb060cdfa0752c185cd47164fcc515 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 7 Aug 2016 20:10:32 -0700 Subject: [PATCH] adding foreign function interface and REPL support --- doc/install.md | 2 +- examples/test_native/Makefile | 7 ++ examples/test_native/test.ivy | 21 ++++ ivy/ivy_actions.py | 9 ++ ivy/ivy_ast.py | 39 ++++++- ivy/ivy_compiler.py | 7 +- ivy/ivy_isolate.py | 1 - ivy/ivy_lexer.py | 7 ++ ivy/ivy_module.py | 1 + ivy/ivy_parser.py | 35 ++++++- ivy/ivy_to_cpp.py | 192 +++++++++++++++++++++++++++++++++- test/native.py | 67 ++++++++++++ 12 files changed, 379 insertions(+), 9 deletions(-) create mode 100644 examples/test_native/Makefile create mode 100644 examples/test_native/test.ivy create mode 100644 test/native.py diff --git a/doc/install.md b/doc/install.md index 6c1cf15..28047a5 100644 --- a/doc/install.md +++ b/doc/install.md @@ -83,7 +83,7 @@ If you don't want to do a system-wide install (and you aren't using a virtual environment) there are various ways to install in your home directory. For example: - $ python setup install --home=~ + $ python setup.py install --home=~ See the [python documentation](https://docs.python.org/2/install/) for general instructions on installing python packages. diff --git a/examples/test_native/Makefile b/examples/test_native/Makefile new file mode 100644 index 0000000..497f7f4 --- /dev/null +++ b/examples/test_native/Makefile @@ -0,0 +1,7 @@ +all: test + +test.cpp: test.ivy + ivy_to_cpp target=repl test.ivy + +test: main.cpp test.cpp + g++ -g -o test test.cpp diff --git a/examples/test_native/test.ivy b/examples/test_native/test.ivy new file mode 100644 index 0000000..fa7ec69 --- /dev/null +++ b/examples/test_native/test.ivy @@ -0,0 +1,21 @@ +#lang ivy1.5 + +module bar = { + + object foo = {} + + <<< + int `foo`; + >>> + + action incr = { + <<< + `foo`++; + >>> + } + +} + +type t +interpret t -> {0..1} +instance baz(X:t) : bar diff --git a/ivy/ivy_actions.py b/ivy/ivy_actions.py index 87d6242..bcf4a0a 100644 --- a/ivy/ivy_actions.py +++ b/ivy/ivy_actions.py @@ -690,6 +690,15 @@ class LetAction(Action): # print "let res: {}".format(res) return res +class NativeAction(Action): + """ Quote native code in an action """ + def name(self): + return 'native' + def __str__(self): + return ivy_ast.native_to_string(self.args) + def int_update(self,domain,pvars): + return ([], true_clauses(), false_clauses()) + call_action_ctr = 0 class CallAction(Action): diff --git a/ivy/ivy_ast.py b/ivy/ivy_ast.py index b688770..191dc77 100644 --- a/ivy/ivy_ast.py +++ b/ivy/ivy_ast.py @@ -666,6 +666,41 @@ class DelegateDef(AST): s += ' -> ' + self.delegee return s + +class NativeCode(AST): + def __init__(self,string): + self.args = [] + self.code = string + def __str__(self): + return self.code + def clone(self,args): + return NativeCode(self.code) + + +def native_to_string(args): + res = '<<<' + fields = args[0].code.split('`') + fields = [(str(args[int(s)+1]) if idx % 2 == 1 else s) for idx,s in enumerate(fields)] + res += '`'.join(fields) + res += '>>>' + return res + + +class NativeDef(AST): + def name(self): + return 'native' + def __str__(self): + res = ('[' + str(self.args[0]) + '] ') if self.args[0] else '' + res += native_to_string(self.args[1:]) + return res + +class NativeDecl(Decl): + def name(self): + return 'native' + def defines(self): + return [] + + class TypeDef(Definition): def __init__(self,name,sort): self.args = [name,sort] @@ -837,14 +872,14 @@ def ast_rewrite(x,rewrite): return type(x)(ast_rewrite(x.bounds,rewrite),ast_rewrite(x.args[0],rewrite)) if hasattr(x,'rewrite'): return x.rewrite(rewrite) - if isinstance(x,LabeledFormula): + if isinstance(x,LabeledFormula) or isinstance(x,NativeDef): arg0 = x.args[0] if x.args[0] == None: if isinstance(rewrite,AstRewriteSubstPrefix) and rewrite.pref != None: arg0 = rewrite.pref else: arg0 = rewrite.rewrite_atom(x.args[0],always=True) - res = x.clone([arg0,ast_rewrite(x.args[1],rewrite)]) + res = x.clone([arg0] + [ast_rewrite(y,rewrite) for y in x.args[1:]]) return res if isinstance(x,TypeDef): atom = rewrite.rewrite_atom(Atom(x.args[0])) diff --git a/ivy/ivy_compiler.py b/ivy/ivy_compiler.py index bea390c..8ea2b53 100644 --- a/ivy/ivy_compiler.py +++ b/ivy/ivy_compiler.py @@ -7,7 +7,7 @@ from ivy_interp import Interp, eval_state_facts from functools import partial from ivy_concept_space import * from ivy_parser import parse,ConstantDecl,ActionDef -from ivy_actions import DerivedUpdate, type_check_action, type_check, SymbolList, UpdatePattern, ActionContext, LocalAction, AssignAction, CallAction, Sequence, IfAction, AssertAction, AssumeAction +from ivy_actions import DerivedUpdate, type_check_action, type_check, SymbolList, UpdatePattern, ActionContext, LocalAction, AssignAction, CallAction, Sequence, IfAction, AssertAction, AssumeAction, NativeAction from ivy_utils import IvyError import ivy_logic import ivy_dafny_compiler as dc @@ -295,6 +295,8 @@ def compile_assert_action(self): AssertAction.cmpl = compile_assert_action AssumeAction.cmpl = compile_assert_action +NativeAction.cmpl = lambda self: self + def compile_action_def(a,sig): sig = sig.copy() if not hasattr(a.args[1],'lineno'): @@ -461,6 +463,9 @@ class IvyARGSetup(IvyDeclInterp): self.mod.privates.add(pvt.privatized()) def delegate(self,exp): self.mod.delegates.append(exp) + def native(self,native_def): + print native_def + self.mod.natives.append(native_def) def ivy_new(filename = None): diff --git a/ivy/ivy_isolate.py b/ivy/ivy_isolate.py index 2eed2e8..7400bf7 100644 --- a/ivy/ivy_isolate.py +++ b/ivy/ivy_isolate.py @@ -672,7 +672,6 @@ def create_isolate(iso,mod = None,**kwargs): if mod.isolates: raise iu.IvyError(None,'no isolate specified on command line') # apply all the mixins in no particular order - iu.dbg('"got here"') for name,mixins in mod.mixins.iteritems(): for mixin in mixins: action1,action2 = (lookup_action(mixin,mod,a.relname) for a in mixin.args) diff --git a/ivy/ivy_lexer.py b/ivy/ivy_lexer.py index 66de635..55b162b 100644 --- a/ivy/ivy_lexer.py +++ b/ivy/ivy_lexer.py @@ -31,6 +31,7 @@ tokens = ( 'GT', 'MINUS', 'DOTS', + 'NATIVEQUOTE', ) reserved = all_reserved = { @@ -153,6 +154,12 @@ def t_VARIABLE(t): t.type = reserved.get(t.value,'VARIABLE') return t +def t_NATIVEQUOTE(t): + r'<<<[\s\S]*?>>>' + t.lexer.lineno += sum(1 for c in t.value if c == '\n') + t.type = reserved.get(t.value,'NATIVEQUOTE') + return t + def t_error(t): print "Illegal character '%s'" % t.value[0] t.lexer.skip(1) diff --git a/ivy/ivy_module.py b/ivy/ivy_module.py index d70567a..9d9932d 100644 --- a/ivy/ivy_module.py +++ b/ivy/ivy_module.py @@ -54,6 +54,7 @@ class Module(object): self.sort_destructors = defaultdict(list) self.privates = set() # set of string (names of private actions) self.interps = defaultdict(list) # maps type names to lists of labeled interpretions + self.natives = [] # list of NativeDef self.sig = il.sig.copy() # capture the current signature diff --git a/ivy/ivy_parser.py b/ivy/ivy_parser.py index 2c75876..34b614e 100644 --- a/ivy/ivy_parser.py +++ b/ivy/ivy_parser.py @@ -3,7 +3,7 @@ # from ivy_concept_space import NamedSpace, ProductSpace, SumSpace from ivy_ast import * -from ivy_actions import AssumeAction, AssertAction, EnsuresAction, SetAction, AssignAction, HavocAction, IfAction, AssignFieldAction, NullFieldAction, CopyFieldAction, InstantiateAction, CallAction, LocalAction, LetAction, Sequence, UpdatePattern, PatternBasedUpdate, SymbolList, UpdatePatternList, Schema, ChoiceAction +from ivy_actions import AssumeAction, AssertAction, EnsuresAction, SetAction, AssignAction, HavocAction, IfAction, AssignFieldAction, NullFieldAction, CopyFieldAction, InstantiateAction, CallAction, LocalAction, LetAction, Sequence, UpdatePattern, PatternBasedUpdate, SymbolList, UpdatePatternList, Schema, ChoiceAction, NativeAction from ivy_lexer import * import ivy_utils as iu import copy @@ -589,6 +589,12 @@ def p_optaction_action(p): 'optaction : action' p[0] = p[1] +def p_optaction_nativequote(p): + 'optaction : NATIVEQUOTE' + text,bqs = parse_nativequote(p,1) + p[0] = NativeAction(*([text] + bqs)) + p[0].lineno = get_lineno(p,1) + if iu.get_numeric_version() <= [1,1]: def p_top_action_symbol_eq_loc_action_loc(p): 'top : top ACTION SYMBOL loc EQ LCB optaction RCB loc' @@ -780,6 +786,33 @@ def p_top_interpret_symbol_arrow_lcb_symbol_dots_symbol_rcb(p): thing.lineno = get_lineno(p,4) p[0].declare(thing) +def parse_nativequote(p,n): + string = p[n][3:-3] # drop the quotation marks + fields = string.split('`') + bqs = [Atom(s) for idx,s in enumerate(fields) if idx % 2 == 1] + text = "`".join([(s if idx % 2 == 0 else str(idx/2)) for idx,s in enumerate(fields)]) + eols = [sum(1 for c in s if c == '\n') for idx,s in enumerate(fields) if idx % 2 == 0] + seols = 0 + filename,line = get_lineno(p,n) + for idx,e in enumerate(eols[:-1]): + seols += e + bqs[idx].lineno = (filename,line+seols) + if len(fields) %2 != 1: + thing = Atom("") + thing.lineno = (filename,line) + report_error(IvyError(thing,"unterminated back-quote")) + return NativeCode(text),bqs + +def p_top_nativequote(p): + 'top : top NATIVEQUOTE' + p[0] = p[1] + text,bqs = parse_nativequote(p,2) + defn = NativeDef(*([None] + [text] + bqs)) + defn.lineno = get_lineno(p,2) + thing = NativeDecl(defn) + thing.lineno = get_lineno(p,2) + p[0].declare(thing) + def p_loc(p): 'loc : ' p[0] = None diff --git a/ivy/ivy_to_cpp.py b/ivy/ivy_to_cpp.py index d09e4e5..7817a80 100755 --- a/ivy/ivy_to_cpp.py +++ b/ivy/ivy_to_cpp.py @@ -381,6 +381,21 @@ def emit_derived(header,impl,df,classname): action.formal_returns = [retval] emit_some_action(header,impl,name,action,classname) + +def native_declaration(atom): + res = varname(atom.rep) + for arg in atom.args: + res += '[' + str(sort_card(im.module.sig.sorts[arg.sort])) + ']' + return res + +def native_to_str(native): + fields = native.args[1].code.split('`') + fields = [(native_declaration(native.args[int(s)+2]) if idx % 2 == 1 else s) for idx,s in enumerate(fields)] + return ''.join(fields) + +def emit_native(header,impl,native,classname): + header.append(native_to_str(native)) + def emit_method_decl(header,name,action,body=False,classname=None): if not hasattr(action,"formal_returns"): print "bad name: {}".format(name) @@ -564,8 +579,8 @@ def module_to_cpp_class(classname): header.append(' ivy_gen *___ivy_gen;\n') header.append(' int ___ivy_choose(int rng,const char *name,int id);\n') if target.get() != "gen": - header.append(' virtual void ivy_assert(bool){}\n') - header.append(' virtual void ivy_assume(bool){}\n') + header.append(' virtual void ivy_assert(bool,const char *){}\n') + header.append(' virtual void ivy_assume(bool,const char *){}\n') header.append(' virtual void ivy_check_progress(int,int){}\n') impl = ['#include "' + classname + '.h"\n\n'] @@ -598,6 +613,9 @@ def module_to_cpp_class(classname): for df in im.module.concepts: emit_derived(header,impl,df,classname) + for native in im.module.natives: + emit_native(header,impl,native,classname) + # declare one counter for each progress obligation # TRICKY: these symbols are boolean but we create a C++ int for df in im.module.progress: @@ -628,8 +646,25 @@ def module_to_cpp_class(classname): for name,action in im.module.actions.iteritems(): if name in im.module.public_actions: emit_action_gen(header,impl,name,action,classname) + + if target.get() == "repl": + emit_repl_boilerplate1(header,impl,classname) + for actname in sorted(im.module.public_actions): + action = im.module.actions[actname] + getargs = ','.join('int_arg(args,0,ivy.__CARD__{})'.format(varname(x.sort.name)) for x in action.formal_params) + impl.append(""" + if (action == "actname") { + check_arity(args,numargs,action); + ivy.baz__incr(getargs); + } + else +""".replace('actname',actname).replace('numargs',str(len(action.formal_params))).replace('getargs',getargs)) + emit_repl_boilerplate2(header,impl,classname) + return ''.join(header) , ''.join(impl) + + def assign_symbol_from_model(header,sym,m): if slv.solver_name(sym) == None: return # skip interpreted symbols @@ -992,6 +1027,157 @@ def emit_choice(self,header): ia.ChoiceAction.emit = emit_choice +def native_reference(atom): + res = varname(atom.rep) + for arg in atom.args: + res += '[' + varname(arg.rep) + ']' + return res + +def emit_native_action(self,header): + fields = self.args[0].code.split('`') + fields = [(native_reference(self.args[int(s)+1]) if idx % 2 == 1 else s) for idx,s in enumerate(fields)] + header.append(''.join(fields)) + +ia.NativeAction.emit = emit_native_action + + +def emit_repl_boilerplate1(header,impl,classname): + impl.append(""" +#include +#include +#include /* See NOTES */ +#include +#include +#include +#include +#include +#include +#include + +// Override methods to implement low-level network service + +bool is_white(int c) { + return (c == ' ' || c == '\\t' || c == '\\n'); +} + +bool is_ident(int c) { + return c == '_' || c == '.' || (c >= 'A' && c <= 'Z') + || (c >= 'a' && c <= 'z') + || (c >= '0' && c <= '9'); +} + +void skip_white(const std::string& str, int &pos){ + while (pos < str.size() && is_white(str[pos])) + pos++; +} + +struct syntax_error { +}; + +struct out_of_bounds { + int idx; + out_of_bounds(int _idx) : idx(_idx) {} +}; + +std::string get_ident(const std::string& str, int &pos) { + std::string res = ""; + while (pos < str.size() && is_ident(str[pos])) { + res.push_back(str[pos]); + pos++; + } + if (res.size() == 0) + throw syntax_error(); + return res; +} + + +void parse_command(const std::string &cmd, std::string &action, std::vector &args) { + int pos = 0; + skip_white(cmd,pos); + action = get_ident(cmd,pos); + skip_white(cmd,pos); + if (pos < cmd.size() && cmd[pos] == '(') { + pos++; + skip_white(cmd,pos); + args.push_back(get_ident(cmd,pos)); + while(true) { + skip_white(cmd,pos); + if (!(pos < cmd.size() && cmd[pos] == ',')) + break; + pos++; + args.push_back(get_ident(cmd,pos)); + } + if (!(pos < cmd.size() && cmd[pos] == ')')) + throw syntax_error(); + pos++; + } + skip_white(cmd,pos); + if (pos != cmd.size()) + throw syntax_error(); +} + +struct bad_arity { + std::string action; + int num; + bad_arity(std::string &_action, unsigned _num) : action(_action), num(_num) {} +}; + +void check_arity(std::vector &args, unsigned num, std::string &action) { + if (args.size() != num) + throw bad_arity(action,num); +} + +int int_arg(std::vector &args, unsigned idx, int bound) { + int res = atoi(args[idx].c_str()); + if (res < 0 || res >= bound) + throw out_of_bounds(idx); + return res; +} + +int main(int argc, char **argv){ + + // if (argc != 2) { + // std::cerr << "usage: classname \\n"; + // return(1); + // } + + // int my_id = atoi(argv[1]); + + classname ivy; + + while(true) { + std::cout << "> "; + std::cout.flush(); + std::string cmd; + std::cin >> cmd; + std::string action; + std::vector args; + try { + parse_command(cmd,action,args); +""".replace('classname',classname)) + + +def emit_repl_boilerplate2(header,impl,classname): + impl.append(""" + { + std::cout << "undefined action: " << action << std::endl; + } + } + catch (syntax_error&) { + std::cout << "syntax error" << std::endl; + } + catch (out_of_bounds &err) { + std::cout << "argument " << err.idx + 1 << " out of bounds" << std::endl; + } + catch (bad_arity &err) { + std::cout << "action " << err.action << " takes " << err.num << " input parameters" << std::endl; + } + + } +} +""".replace('classname',classname)) + + def emit_boilerplate1(header,impl): header.append(""" #include @@ -1247,7 +1433,7 @@ public: """) -target = iu.EnumeratedParameter("target",["impl","gen"],"gen") +target = iu.EnumeratedParameter("target",["impl","gen","repl"],"gen") def main(): ia.set_determinize(True) diff --git a/test/native.py b/test/native.py new file mode 100644 index 0000000..9b9aab5 --- /dev/null +++ b/test/native.py @@ -0,0 +1,67 @@ + +from ivy import ivy_module as im +from ivy.ivy_compiler import ivy_from_string +from ivy.tk_ui import new_ui +from ivy import ivy_utils as iu +from ivy import ivy_check as ick +from ivy import ivy_logic as il +from ivy import ivy_to_cpp as i2c +from ivy import ivy_actions as ia +from ivy import ivy_solver as slv +from ivy import ivy_isolate as iso + + +prog = """#lang ivy1.5 + +module bar = { + + object foo = {} + + <<< + int `foo`; + >>> + + action incr = { + <<< + `foo`++; + >>> + } + +} + +type t +interpret t -> {0..1} +instance baz(X:t) : bar + +""" + +ia.set_determinize(True) +slv.set_use_native_enums(True) +iso.set_interpret_all_sorts(True) + +with im.Module(): + iu.set_parameters({'mode':'induction','show_compiled':'true','target':'impl'}) + ivy_from_string(prog,create_isolate=True) + + classname = 'foo' + header,impl = i2c.module_to_cpp_class(classname) + print header + print impl + +# main_ui.answer("OK") +# ui.check_inductiveness() +# # ui = ui.cti +# cg = ui.current_concept_graph +# cg.show_relation(cg.relation('link(X,Y)'),'+') +# cg.gather() +# main_ui.answer("OK") +# cg.strengthen() +# main_ui.answer("OK") +# ui.check_inductiveness() +# # cg.show_relation(cg.relation('semaphore'),'+') +# cg.gather() +# main_ui.answer("View") +# cg.bmc_conjecture(bound=1) +# # main_ui.mainloop() + +