prpr2770
commented
3 years ago I reviewed the code in ivy_to_cpp.py and tried to determine the difference in the functions that's used to generate the above lines.
The lines corresponding to __from_solver() are as follows:
def emit_eval(header,symbol,obj=None,classname=None,lhs=None):
global indent_level
name = symbol.name
sname = slv.solver_name(symbol)
cname = varname(name) if lhs is None else code_eval(header,lhs)
sort = symbol.sort
domain = sort_domain(sort)
for idx,dsort in enumerate(domain):
dcard = sort_card(dsort)
indent(header)
header.append("for (int X{} = 0; X{} < {}; X{}++)\n".format(idx,idx,dcard,idx))
indent_level += 1
indent(header)
if sort.rng.name in im.module.sort_destructors or sort.rng.name in im.module.native_types or sort.rng in sort_to_cpptype:
code_line(header,'__from_solver<'+classname+'::'+varname(sort.rng.name)+'>(*this,apply("'+sname+'"'+''.join(','+int_to_z3(s,'X{}'.format(idx)) for idx,s in enumerate(domain))+'),'+cname+''.join('[X{}]'.format(idx) for idx in range(len(domain)))+')')
else:
header.append((obj + '.' if obj else '')
+ cname + ''.join("[X{}]".format(idx) for idx in range(len(domain)))
+ ' = ({})eval_apply("{}"'.format(ctype(sort.rng,classname=classname),sname)
+ ''.join(",X{}".format(idx) for idx in range(len(domain)))
+ ");\n")
for idx,dsort in enumerate(domain):
indent_level -= 1
# --------------------------------------
# lines 2896::
if target.get() in ["gen","test"]:
impl.append('template <>\n')
open_scope(impl,line='void __from_solver<' + cfsname + '>( gen &g, const z3::expr &v,' + cfsname + ' &res)')
for idx,sym in enumerate(destrs):
fname = memname(sym)
vs = variables(sym.sort.dom[1:])
for v in vs:
open_loop(impl,[v])
sname = slv.solver_name(sym)
code_line(impl,'__from_solver(g,g.apply("'+sname+'",v'+ ''.join(',g.int_to_z3(g.sort("'+v.sort.name+'"),'+varname(v)+')' for v in vs)+'),res.'+fname+''.join('[{}]'.format(varname(v)) for v in vs) + ')')
for v in vs:
close_loop(impl,[v])
close_scope(impl)The lines related to __randomize() are as follows:
def emit_randomize(header,symbol,classname=None):
global indent_level
name = symbol.name
sname = slv.solver_name(symbol)
cname = varname(name)
sort = symbol.sort
domain = sort_domain(sort)
for idx,dsort in enumerate(domain):
dcard = sort_card(dsort)
indent(header)
header.append("for (int X{} = 0; X{} < {}; X{}++)\n".format(idx,idx,dcard,idx))
indent_level += 1
if sort.rng.name in im.module.sort_destructors or sort.rng.name in im.module.native_types or sort.rng in sort_to_cpptype:
code_line(header,'__randomize<'+classname+'::'+varname(sort.rng.name)+'>(*this,apply("'+sname+'"'+''.join(','+int_to_z3(s,'X{}'.format(idx)) for idx,s in enumerate(domain))+'))')
else:
indent(header)
if il.is_uninterpreted_sort(sort.rng):
raise iu.IvyError(None,'cannot create test generator because type {} is uninterpreted'.format(sort.rng))
header.append('randomize("{}"'.format(sname)
+ ''.join(",X{}".format(idx) for idx in range(len(domain)))
+ ");\n")
for idx,dsort in enumerate(domain):
indent_level -= 1
# indent(header)
# header.append('randomize("{}");\n'.format(slv.solver_name(symbol)))
# ---------------------------------------------------------------------
# lines : 2924 onwards
open_scope(impl,line='void __randomize<' + cfsname + '>( gen &g, const z3::expr &v)')
for idx,sym in enumerate(destrs):
# we can't randomize a type that z3 is representing with an uninterpreted sort,
# because z3 has no numerals for these sorts. Rather than throwing an error, however,
# we just don't randomize, in case randomization for this type is not actually needed.
# In principle, we should check whether randomiation is needed but this is pretty tricky.
if is_really_uninterpreted_sort(sym.sort.rng):
continue
# raise iu.IvyError(None,'cannot create test generator because type {} is uninterpreted'.format(sym.sort.rng))
fname = memname(sym)
vs = variables(sym.sort.dom[1:])
for v in vs:
open_loop(impl,[v])
sname = slv.solver_name(sym)
code_line(impl,'__randomize<'+ctypefull(sym.sort.rng,classname=classname)+'>(g,g.apply("'+sname+'",v'+ ''.join(',g.int_to_z3(g.sort("'+v.sort.name+'"),'+varname(v)+')' for v in vs)+'))')
for v in vs:
close_loop(impl,[v])
close_scope(impl)
There seems to be a difference in the positioning of indent(header) command in both emit_randomize() and emit_eval(). I'm not sure if this is an issue, as I'm currently unaware of its functionality.
There seems to be a bug in the compiler that implements the
__randomize()funciton for data types that contain>2 levelsof depth.I'm attempting to generate messages with the following levels of hierarchy:
When I attempt to use the random generator to create random instances of a message of type
level0_t, I obtain the following sample messagesNote that the all instances of
level2_messageA_thas itsvalue: {}. The compiler generatedcppcodebase has the following lines, which indicates thatlevel2_message_t.valueis not being randomly generated.However, the corresponding
__from_solverfunctionality has the following structure, where we see that all three components of the data-type are being processes.Is there a way in which the compiler is constrained to handle random-generation only upto 2 depth-levels?