microsoft
/
ivy
зеркало из https://github.com/microsoft/ivy.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

working on C++ callbacks

This commit is contained in:
Ken McMillan 2016-08-15 18:55:10 -07:00
Родитель 38bd374ef3
Коммит 60a44a77ad
7 изменённых файлов: 129 добавлений и 23 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

15
doc/examples/udp.ivy
Просмотреть файл

@ -11,9 +11,10 @@ module udp_wrapper(addr,pkt,me) = {
class udp_reader : public reader {
int sock;
int my_id;
ivy_class &parent;
%`handle_recv` rcb;
public:
udp_reader(int _my_id, ivy_class &_p) : my_id(_my_id), parent(_p) {
udp_reader(int _my_id, %`handle_recv` rcb)
: my_id(_my_id), rcb(rcb) {
sock = socket(AF_INET, SOCK_DGRAM, 0);
if (sock < 0)
{ std::cerr << "cannot create socket\n"; exit(1); }
@ -36,7 +37,7 @@ module udp_wrapper(addr,pkt,me) = {
//std::cout << "RECEIVING\n";
if (recvfrom(sock,&pkt,sizeof(int),0,0,0) < 0)
{ std::cerr << "recvfrom failed\n"; exit(1); }
parent.`recv`(my_id,pkt);
rcb(pkt);
}
virtual void write(int dst, int pkt) {
struct sockaddr_in dstaddr;
@ -55,9 +56,13 @@ module udp_wrapper(addr,pkt,me) = {
udp_reader *`rdr`;
>>>
<<< init
install_reader(`rdr` = new udp_reader(`me`,*this));
install_reader(`rdr` = new udp_reader(`me`,`handle_recv`));
>>>
action handle_recv(x:pkt) = {
call recv(me,x)
}
implement send(dst:addr,x:pkt) {
<<<
`rdr`->write(`dst`,`x`);
@ -84,4 +89,4 @@ interpret a -> bv[1]
import foo.recv
export foo.send
extract iso_foo = foo(me)
# extract iso_foo = foo(me)

4
ivy/ivy_ast.py
Просмотреть файл

@ -439,8 +439,8 @@ class ObjectDecl(Decl):
def name(self):
return 'object'
def defines(self):
# return [(c.relname,lineno(c)) for c in self.args]
return []
return [(c.relname,lineno(c)) for c in self.args]
# return []
class LabeledFormula(AST):
@property

9
ivy/ivy_compiler.py
Просмотреть файл

@ -301,6 +301,13 @@ def compile_native_action(self):
NativeAction.cmpl = compile_native_action
def compile_native_def(self):
def cna(arg):
return (sortify_with_inference(arg) if isinstance(arg,ivy_ast.Variable) else
a.clone(map(sortify_with_inference,a.args)))
args = list(self.args[0:2]) + [cna(a) for a in self.args[2:]]
return self.clone(args)
def compile_action_def(a,sig):
sig = sig.copy()
if not hasattr(a.args[1],'lineno'):
@ -470,7 +477,7 @@ class IvyARGSetup(IvyDeclInterp):
def delegate(self,exp):
self.mod.delegates.append(exp)
def native(self,native_def):
self.mod.natives.append(native_def)
self.mod.natives.append(compile_native_def(native_def))
def ivy_new(filename = None):

44
ivy/ivy_isolate.py
Просмотреть файл

@ -186,7 +186,7 @@ def strip_sort(sort,strip_params):
def strip_action(ast,strip_map,strip_binding):
if isinstance(ast,ia.CallAction):
name = ast.args[0].rep
name = canon_act(ast.args[0].rep)
args = [strip_action(arg,strip_map,strip_binding) for arg in ast.args[0].args]
strip_params = get_strip_params(name,ast.args[0].args,strip_map,strip_binding,ast)
call = ast.args[0].clone(args[len(strip_params):])
@ -195,6 +195,7 @@ def strip_action(ast,strip_map,strip_binding):
sname = strip_binding[ast]
if sname not in ivy_logic.sig.symbols:
ivy_logic.add_symbol(sname,ast.sort)
strip_added_symbols.append(ivy_logic.Symbol(sname,ast.sort))
return ivy_logic.Symbol(sname,ast.sort)
args = [strip_action(arg,strip_map,strip_binding) for arg in ast.args]
if ivy_logic.is_app(ast):
@ -205,15 +206,21 @@ def strip_action(ast,strip_map,strip_binding):
new_args = args[len(strip_params):]
new_symbol = ivy_logic.Symbol(name,new_sort)
return new_symbol(*new_args)
if isinstance(ast,ivy_ast.Atom):
name = ast.rep
strip_params = get_strip_params(name,ast.args,strip_map,strip_binding,ast)
if strip_params:
new_args = args[len(strip_params):]
return ast.clone(new_args)
return ast.clone(args)
def get_strip_binding(ast,strip_map,strip_binding):
[get_strip_binding(arg,strip_map,strip_binding) for arg in ast.args]
if ivy_logic.is_app(ast):
name = ast.rep.name
name = ast.rep.name if ivy_logic.is_app(ast) else ast.rep if isinstance(ast,ivy_ast.Atom) else None
if name:
strip_params = strip_map_lookup(name,strip_map)
if not(len(ast.args) >= len(strip_params)):
raise iu.IvyError(action,"cannot strip isolate parameters from {}",name)
raise iu.IvyError(ast,"cannot strip isolate parameters from {}".format(name))
for sp,ap in zip(strip_params,ast.args):
if ap in strip_binding and strip_binding[ap] != sp:
raise iu.IvyError(action,"cannot strip parameter {} from {}",ap,name)
@ -234,7 +241,28 @@ def strip_labeled_fmlas(lfmlas,strip_map):
del lfmlas[:]
lfmlas.extend(new_lfmlas)
def strip_native(native,strip_map):
strip_binding = {}
for a in native.args[2:]:
get_strip_binding(a,strip_map,strip_binding)
fmlas = [strip_action(fmla,strip_map,strip_binding) for fmla in native.args[2:]]
lbl = native.args[0]
if lbl:
lbl = lbl.clone(lbl.args[len(strip_map_lookup(lbl.rep,strip_map,with_dot=False)):])
return native.clone([lbl,native.args[1]] + fmlas)
def strip_natives(natives,strip_map):
iu.dbg('natives')
new_natives = [strip_native(f,strip_map) for f in natives]
del natives[:]
natives.extend(new_natives)
def canon_act(name):
return name[4:] if name.startswith('ext:') else name
def strip_isolate(mod,isolate):
global strip_added_symbols
strip_added_symbols = []
strip_map = {}
for atom in isolate.verified() + isolate.present():
name = atom.relname
@ -248,7 +276,7 @@ def strip_isolate(mod,isolate):
# strip the actions
new_actions = {}
for name,action in mod.actions.iteritems():
strip_params = strip_map_lookup(name[4:] if name.startswith('ext:') else name,strip_map)
strip_params = strip_map_lookup(canon_act(name),strip_map)
if not(len(action.formal_params) >= len(strip_params)):
raise iu.IvyError(action,"cannot strip isolate parameters from {}".format(name))
strip_binding = dict(zip(action.formal_params,strip_params))
@ -262,6 +290,10 @@ def strip_isolate(mod,isolate):
# strip the axioms and conjectures
for x in [mod.labeled_axioms,mod.labeled_props,mod.labeled_conjs,mod.labeled_inits]:
strip_labeled_fmlas(x,strip_map)
# strip the native quotes
strip_natives(mod.natives,strip_map)
# strip the signature
new_symbols = {}
for name,sym in ivy_logic.sig.symbols.iteritems():
@ -275,6 +307,8 @@ def strip_isolate(mod,isolate):
ivy_logic.sig.symbols.clear()
ivy_logic.sig.symbols.update(new_symbols)
del mod.params[:]
mod.params.extend(strip_added_symbols)
def get_calls_mods(mod,summarized_actions,actname,calls,mods,mixins):
if actname in calls or actname not in summarized_actions:

1
ivy/ivy_module.py
Просмотреть файл

@ -56,6 +56,7 @@ class Module(object):
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.params = []
self.sig = il.sig.copy() # capture the current signature

4
ivy/ivy_parser.py
Просмотреть файл

@ -99,7 +99,7 @@ def do_insts(ivy,insts):
if defn:
# print "instantiating %s" % inst
if pref != None:
ivy.define((pref.rep,inst.lineno))
# ivy.define((pref.rep,inst.lineno))
ivy.declare(ObjectDecl(pref))
aparams = inst.args
fparams = defn.args[0].args
@ -227,7 +227,7 @@ def p_top_object_symbol_eq_lcb_top_rcb(p):
p[0] = p[1]
module = p[6]
pref = Atom(p[3],[])
p[0].define((pref.rep,get_lineno(p,2)))
# p[0].define((pref.rep,get_lineno(p,2)))
p[0].declare(ObjectDecl(pref))
for decl in module.decls:
idecl = subst_prefix_atoms_ast(decl,{},pref,module.defined)

75
ivy/ivy_to_cpp.py
Просмотреть файл

@ -15,6 +15,7 @@ import ivy_transrel as tr
import ivy_logic_utils as ilu
import ivy_compiler as ic
import ivy_isolate as iso
import ivy_ast
import itertools
from collections import defaultdict
@ -83,6 +84,8 @@ special_names = {
def varname(name):
global special_names
if not isinstance(name,str):
name = name.name
if name in special_names:
return special_names[name]
name = name.replace('loc:','loc__').replace('ext:','ext__').replace('___branch:','__branch__').replace('.','__')
@ -413,19 +416,61 @@ def native_type(native):
def native_declaration(atom):
res = varname(atom.rep)
for arg in atom.args:
res += '[' + str(sort_card(im.module.sig.sorts[arg.sort])) + ']'
sort = arg.sort if isinstance(arg.sort,str) else arg.sort.name
res += '[' + str(sort_card(im.module.sig.sorts[sort])) + ']'
return res
thunk_counter = 0
def action_return_type(action):
return 'int' if action.formal_returns else 'void'
def thunk_name(actname):
return 'thunk__' + varname(actname)
def create_thunk(impl,actname,action,classname):
tc = thunk_name(actname)
impl.append('struct ' + tc + '{\n')
impl.append(' ' + classname + ' *__ivy' + ';\n')
params = [p for p in action.formal_params if p.name.startswith('prm:')]
inputs = [p for p in action.formal_params if not p.name.startswith('prm:')]
for p in params:
declare_symbol(impl,p)
impl.append(' ')
emit_param_decls(impl,tc,params,extra = [ classname + ' *__ivy'])
impl.append(': __ivy(__ivy)' + ''.join(',' + varname(p) + '(' + varname(p) + ')' for p in params) + '{}\n')
impl.append(' ' + action_return_type(action) + ' ')
emit_param_decls(impl,'operator()',inputs);
impl.append(' const {\n __ivy->' + varname(actname)
+ '(' + ','.join(varname(p.name) for p in action.formal_params) + ');\n }\n};\n')
def native_typeof(arg):
if isinstance(arg,ivy_ast.Atom):
if arg.rep in im.module.actions:
return thunk_name(arg.rep)
raise IvyError(arg,'undefined action: ' + arg.rep)
return int + len(arg.sort.dom) * '[]'
def native_to_str(native,reference=False):
tag,code = native_split(native.args[1].code)
fields = code.split('`')
f = native_reference if reference else native_declaration
fields = [(f(native.args[int(s)+2]) if idx % 2 == 1 else s) for idx,s in enumerate(fields)]
def nfun(idx):
return native_typeof if fields[idx-1].endswith('%') else f
def dm(s):
return s[:-1] if s.endswith('%') else s
fields = [(nfun(idx)(native.args[int(s)+2]) if idx % 2 == 1 else dm(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_param_decls(header,name,params,extra=[]):
header.append(varname(name) + '(')
header.append(', '.join(extra + ['int ' + varname(p.name) for p in params]))
header.append(')')
def emit_method_decl(header,name,action,body=False,classname=None):
if not hasattr(action,"formal_returns"):
print "bad name: {}".format(name)
@ -443,12 +488,7 @@ def emit_method_decl(header,name,action,body=False,classname=None):
raise iu.IvyError(action,'cannot handle multiple output values')
if body:
header.append(classname + '::')
header.append(varname(name) + '(')
first = True
for p in action.formal_params:
header.append(('' if first else ', ') + 'int ' + varname(p.name))
first = False
header.append(')')
emit_param_decls(header,name,action.formal_params)
def emit_action(header,impl,name,classname):
action = im.module.actions[name]
@ -640,6 +680,21 @@ def module_to_cpp_class(classname):
#include <unistd.h>
""")
impl.append("typedef {} ivy_class;\n".format(classname))
native_exprs = []
for n in im.module.natives:
native_exprs.extend(n.args[2:])
for n in im.module.actions.values():
if isinstance(n,ia.NativeAction):
native_exprs.extend(n.args[1:])
callbacks = set()
for e in native_exprs:
if isinstance(e,ivy_ast.Atom) and e.rep in im.module.actions:
callbacks.add(e.rep)
for actname in sorted(callbacks):
action = im.module.actions[actname]
create_thunk(impl,actname,action,classname)
impl.append("""
class reader {
public:
@ -1134,6 +1189,10 @@ def emit_choice(self,header):
ia.ChoiceAction.emit = emit_choice
def native_reference(atom):
if isinstance(atom,ivy_ast.Atom) and atom.rep in im.module.actions:
res = thunk_name(atom.rep) + '(this'
res += ''.join(', ' + varname(arg.rep) for arg in atom.args) + ')'
return res
res = varname(atom.rep)
for arg in atom.args:
n = arg.name if hasattr(arg,'name') else arg.rep