adding foreign function interface and REPL support

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.

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

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

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):

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]))

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):

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)

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)

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
 

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

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 <iostream>
+#include <stdlib.h>
+#include <sys/types.h>          /* See NOTES */
+#include <sys/socket.h>
+#include <netinet/in.h>
+#include <netinet/ip.h> 
+#include <sys/select.h>
+#include <string.h>
+#include <stdio.h>
+#include <string>
+
+// 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<std::string> &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<std::string> &args, unsigned num, std::string &action) {
+    if (args.size() != num)
+        throw bad_arity(action,num);
+}
+
+int int_arg(std::vector<std::string> &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 <index>\\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<std::string> 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 <string>
@@ -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)

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()
+
+