def pythonast(self, args, tonative=False):
return ast.BoolOp(ast.And(), args)
python类BoolOp()的实例源码
def pythonast(self, args, tonative=False):
return ast.BoolOp(ast.Or(), args)
def ast(self):
"""Python AST of this predicate (construct transitively for all indirect children as well).
:return: AST of describing all children predicates
"""
return ast.BoolOp(ast.And(), [ast.Expr(value=x.ast()) for x in self._children])
def ast(self):
"""Python AST of this predicate (construct transitively for all indirect children as well).
:return: AST of describing all children predicates
"""
return ast.BoolOp(ast.Or(), [ast.Expr(value=x.ast()) for x in self._children])
def ast(self):
"""Python AST of this predicate (construct transitively for all indirect children as well).
:return: AST of describing all children predicates
"""
return ast.BoolOp(ast.And(), [ast.Expr(value=x.ast()) for x in self._children])
def ast(self):
"""Python AST of this predicate (construct transitively for all indirect children as well).
:return: AST of describing all children predicates
"""
return ast.BoolOp(ast.Or(), [ast.Expr(value=x.ast()) for x in self._children])
def peval_boolop(state, ctx, op, values):
assert type(op) in (ast.And, ast.Or)
new_values = []
for value in values:
state, new_value = _peval_expression(state, value, ctx)
# Short circuit
if is_known_value(new_value):
success, bool_value = try_call(bool, args=(new_value.value,))
short_circuit_applicable = (
success
and (
(type(op) == ast.And and not bool_value)
or (type(op) == ast.Or and bool_value)))
if short_circuit_applicable:
return state, new_value
# Just skip it, it won't change the BoolOp result.
else:
new_values.append(new_value)
if len(new_values) == 0:
return state, KnownValue(type(op) == ast.And)
elif len(new_values) == 1:
return state, new_values[0]
else:
return state, ast.BoolOp(op=op, values=new_values)
def _peval_comprehension_ifs(state, ifs, ctx):
if len(ifs) > 0:
joint_ifs = ast.BoolOp(op=ast.And(), values=ifs)
state, joint_ifs_result = _peval_expression(state, joint_ifs, ctx)
if is_known_value(joint_ifs_result):
return state, joint_ifs_result
else:
return state, joint_ifs_result.values
else:
return state, KnownValue(value=True)
def translate_pat_Call_constructor(self, ctx, pat, scrutinee_trans):
scrutinee_trans_copy = astx.copy_node(scrutinee_trans)
args, keywords = pat.args, pat.keywords
idx = self.idx
conditions = []
binding_translations = _util.odict()
for i, arg in enumerate(args):
n = _util.odict_idx_of(idx, i)
elt_scrutinee_trans = astx.make_Subscript_Num_Index(
scrutinee_trans_copy,
n)
elt_condition, elt_binding_translations = ctx.translate_pat(
arg, elt_scrutinee_trans)
conditions.append(elt_condition)
binding_translations.update(elt_binding_translations)
for keyword in keywords:
n = _util.odict_idx_of(idx, keyword.arg)
elt_scrutinee_trans = astx.make_Subscript_Num_Index(
scrutinee_trans_copy,
n)
elt_condition, elt_binding_translations = ctx.translate_pat(
keyword.value, elt_scrutinee_trans)
conditions.append(elt_condition)
binding_translations.update(elt_binding_translations)
condition = ast.BoolOp(
op=ast.And(),
values=conditions)
return (condition, binding_translations)
def areDisjoint(a, b):
"""Are the sets of values that satisfy these two boolean constraints disjoint?"""
# The easiest way to be disjoint is to have comparisons that cover different areas
if type(a) == type(b) == ast.Compare:
aop = a.ops[0]
bop = b.ops[0]
aLeft = a.left
aRight = a.comparators[0]
bLeft = b.left
bRight = b.comparators[0]
alblComp = compareASTs(aLeft, bLeft, checkEquality=True)
albrComp = compareASTs(aLeft, bRight, checkEquality=True)
arblComp = compareASTs(aRight, bLeft, checkEquality=True)
arbrComp = compareASTs(aRight, bRight, checkEquality=True)
altype = type(aLeft) in [ast.Num, ast.Str]
artype = type(aRight) in [ast.Num, ast.Str]
bltype = type(bLeft) in [ast.Num, ast.Str]
brtype = type(bRight) in [ast.Num, ast.Str]
if (type(aop) == ast.Eq and type(bop) == ast.NotEq) or \
(type(bop) == ast.Eq and type(aop) == ast.NotEq):
# x == y, x != y
if (alblComp == 0 and arbrComp == 0) or (albrComp == 0 and arblComp == 0):
return True
elif type(aop) == type(bop) == ast.Eq:
if (alblComp == 0 and arbrComp == 0) or (albrComp == 0 and arblComp == 0):
return False
# x = num1, x = num2
elif alblComp == 0 and artype and brtype:
return True
elif albrComp == 0 and artype and bltype:
return True
elif arblComp == 0 and altype and brtype:
return True
elif arbrComp == 0 and altype and bltype:
return True
elif (type(aop) == ast.Lt and type(bop) == ast.GtE) or \
(type(aop) == ast.Gt and type(bop) == ast.LtE) or \
(type(aop) == ast.LtE and type(bop) == ast.Gt) or \
(type(aop) == ast.GtE and type(bop) == ast.Lt) or \
(type(aop) == ast.Is and type(bop) == ast.IsNot) or \
(type(aop) == ast.IsNot and type(bop) == ast.Is) or \
(type(aop) == ast.In and type(bop) == ast.NotIn) or \
(type(aop) == ast.NotIn and type(bop) == ast.In):
if alblComp == 0 and arbrComp == 0:
return True
elif (type(aop) == ast.Lt and type(bop) == ast.LtE) or \
(type(aop) == ast.Gt and type(bop) == ast.GtE) or \
(type(aop) == ast.LtE and type(bop) == ast.Lt) or \
(type(aop) == ast.GtE and type(bop) == ast.Gt):
if albrComp == 0 and arblComp == 0:
return True
elif type(a) == type(b) == ast.BoolOp:
return False # for now- TODO: when is this not true?
elif type(a) == ast.UnaryOp and type(a.op) == ast.Not:
if compareASTs(a.operand, b, checkEquality=True) == 0:
return True
elif type(b) == ast.UnaryOp and type(b.op) == ast.Not:
if compareASTs(b.operand, a, checkEquality=True) == 0:
return True
return False
def deMorganize(a):
"""Apply De Morgan's law throughout the code in order to canonicalize"""
if not isinstance(a, ast.AST):
return a
# We only care about statements beginning with not
if type(a) == ast.UnaryOp and type(a.op) == ast.Not:
oper = a.operand
top = type(oper)
# not (blah and gah) == (not blah or not gah)
if top == ast.BoolOp:
oper.op = negate(oper.op)
for i in range(len(oper.values)):
oper.values[i] = deMorganize(negate(oper.values[i]))
oper.negated = not oper.negated if hasattr(oper, "negated") else True
transferMetaData(a, oper)
return oper
# not a < b == a >= b
elif top == ast.Compare:
oper.left = deMorganize(oper.left)
oper.ops = [negate(oper.ops[0])]
oper.comparators = [deMorganize(oper.comparators[0])]
oper.negated = not oper.negated if hasattr(oper, "negated") else True
transferMetaData(a, oper)
return oper
# not not blah == blah
elif top == ast.UnaryOp and type(oper.op) == ast.Not:
oper.operand = deMorganize(oper.operand)
if eventualType(oper.operand) != bool:
return a
oper.operand.negated = not oper.operand.negated if hasattr(oper.operand, "negated") else True
return oper.operand
elif top == ast.NameConstant:
if oper.value in [True, False]:
oper = negate(oper)
transferMetaData(a, oper)
return oper
elif oper.value == None:
tmp = ast.NameConstant(True)
transferMetaData(a, tmp)
tmp.negated = True
return tmp
else:
log("Unknown NameConstant: " + str(oper.value), "bug")
return applyToChildren(a, deMorganize)
##### CLEANUP FUNCTIONS #####
def negate(op):
"""Return the negation of the provided operator"""
if op == None:
return None
top = type(op)
neg = not op.negated if hasattr(op, "negated") else True
if top == ast.And:
newOp = ast.Or()
elif top == ast.Or:
newOp = ast.And()
elif top == ast.Eq:
newOp = ast.NotEq()
elif top == ast.NotEq:
newOp = ast.Eq()
elif top == ast.Lt:
newOp = ast.GtE()
elif top == ast.GtE:
newOp = ast.Lt()
elif top == ast.Gt:
newOp = ast.LtE()
elif top == ast.LtE:
newOp = ast.Gt()
elif top == ast.Is:
newOp = ast.IsNot()
elif top == ast.IsNot:
newOp = ast.Is()
elif top == ast.In:
newOp = ast.NotIn()
elif top == ast.NotIn:
newOp = ast.In()
elif top == ast.NameConstant and op.value in [True, False]:
op.value = not op.value
op.negated = neg
return op
elif top == ast.Compare:
if len(op.ops) == 1:
op.ops[0] = negate(op.ops[0])
op.negated = neg
return op
else:
values = []
allOperands = [op.left] + op.comparators
for i in range(len(op.ops)):
values.append(ast.Compare(allOperands[i], [negate(op.ops[i])],
[allOperands[i+1]], multiCompPart=True))
newOp = ast.BoolOp(ast.Or(multiCompOp=True), values, multiComp=True)
elif top == ast.UnaryOp and type(op.op) == ast.Not and \
eventualType(op.operand) == bool: # this can mess things up type-wise
return op.operand
else:
# this is a normal value, so put a not around it
newOp = ast.UnaryOp(ast.Not(addedNot=True), op)
transferMetaData(op, newOp)
newOp.negated = neg
return newOp
def rewrite_expr_z3_py_ast(r, is_py_ast=True):
if verbose and False:
print('rewrite_expr_z3_py_ast:', r)
# Rewrites py_ast expression to a str expression that could be used in z3
# Return (z3_expr_str, z3_varnames)
z3_expr_str = (py_ast.dump_ast(r) if is_py_ast else r).strip()
z3_expr_str = z3_expr_str.replace('.', '_').replace('[', '_').replace(']', '_')
rp = py_ast.get_ast(z3_expr_str).body[0].value
nodes = py_ast.find_all(rp, ast.UnaryOp)
while nodes != []:
node = nodes[0]
if isinstance(node.op, ast.Not):
if rp == node:
rp = py_ast.get_ast('z3.Not(' + py_ast.dump_ast(node.operand) + ')').body[0].value
else:
py_ast.replace_node(rp, node, py_ast.get_ast('z3.Not(' + py_ast.dump_ast(node.operand) + ')').body[0].value)
nodes = py_ast.find_all(rp, ast.UnaryOp)
else:
nodes = nodes[1:]
nodes = py_ast.find_all(rp, ast.BoolOp)
while nodes != []:
node = nodes[0]
if isinstance(node.op, ast.And):
rp_str = 'z3.And('
for value in node.values:
rp_str += py_ast.dump_ast(value) + ', '
rp_str = rp_str.rstrip(', ')
rp_str += ')'
if rp == node:
rp = py_ast.get_ast(rp_str).body[0].value
else:
py_ast.replace_node(rp, node, py_ast.get_ast(rp_str).body[0].value)
elif isinstance(node.op, ast.Or):
rp_str = 'z3.Or('
for value in node.values:
rp_str += py_ast.dump_ast(value) + ', '
rp_str = rp_str.rstrip(', ')
rp_str += ')'
if rp == node:
rp = py_ast.get_ast(rp_str).body[0].value
else:
py_ast.replace_node(rp, node, py_ast.get_ast(rp_str).body[0].value)
nodes = py_ast.find_all(rp, ast.BoolOp)
z3_expr_str = py_ast.dump_ast(rp)
z3_vars = set()
for node in py_ast.find_all(rp, ast.Name):
z3_vars.add(node.id)
if 'z3' in z3_vars:
z3_vars.remove('z3')
return (z3_expr_str, z3_vars)
def infer(node, context, solver, from_call=False):
"""Infer the type of a given AST node"""
if isinstance(node, ast.Num):
return infer_numeric(node, solver)
elif isinstance(node, ast.Str):
return solver.z3_types.string
elif (sys.version_info[0] >= 3 and sys.version_info[1] >= 6 and
(isinstance(node, ast.FormattedValue) or isinstance(node, ast.JoinedStr))):
# Formatted strings were introduced in Python 3.6
return solver.z3_types.string
elif isinstance(node, ast.Bytes):
return solver.z3_types.bytes
elif isinstance(node, ast.List):
return infer_list(node, context, solver)
elif isinstance(node, ast.Dict):
return infer_dict(node, context, solver)
elif isinstance(node, ast.Tuple):
return infer_tuple(node, context, solver)
elif isinstance(node, ast.NameConstant):
return infer_name_constant(node, solver)
elif isinstance(node, ast.Set):
return infer_set(node, context, solver)
elif isinstance(node, ast.BinOp):
return infer_binary_operation(node, context, solver)
elif isinstance(node, ast.BoolOp):
return infer_boolean_operation(node, context, solver)
elif isinstance(node, ast.UnaryOp):
return infer_unary_operation(node, context, solver)
elif isinstance(node, ast.IfExp):
return infer_if_expression(node, context, solver)
elif isinstance(node, ast.Subscript):
return infer_subscript(node, context, solver)
elif sys.version_info[0] >= 3 and sys.version_info[1] >= 5 and isinstance(node, ast.Await):
# Await and Async were introduced in Python 3.5
return infer(node.value, context, solver)
elif isinstance(node, ast.Yield):
return infer(node.value, context, solver)
elif isinstance(node, ast.Compare):
return infer_compare(node, context, solver)
elif isinstance(node, ast.Name):
return infer_name(node, context)
elif isinstance(node, ast.ListComp):
return infer_sequence_comprehension(node, solver.z3_types.list, context, solver)
elif isinstance(node, ast.SetComp):
return infer_sequence_comprehension(node, solver.z3_types.set, context, solver)
elif isinstance(node, ast.DictComp):
return infer_dict_comprehension(node, context, solver)
elif isinstance(node, ast.Call):
return infer_func_call(node, context, solver)
elif isinstance(node, ast.Attribute):
return infer_attribute(node, context, from_call, solver)
elif isinstance(node, ast.Lambda):
return _infer_lambda(node, context, solver)
raise NotImplementedError("Inference for expression {} is not implemented yet.".format(type(node).__name__))
def peval_compare(state, ctx, node):
if len(node.ops) == 1:
return peval_single_compare(state, ctx, node.ops[0], node.left, node.comparators[0])
values = []
for value_node in [node.left] + node.comparators:
state, value = _peval_expression(state, value_node, ctx)
values.append(value)
pair_values = []
lefts = [node.left] + node.comparators[:-1]
rights = node.comparators
for left, op, right in zip(lefts, node.ops, rights):
state, pair_value = peval_single_compare(state, ctx, op, left, right)
pair_values.append(pair_value)
state, result = peval_boolop(state, ctx, ast.And(), pair_values)
if is_known_value(result):
return state, result
if type(result) != ast.BoolOp:
return state, result
# Glueing non-evaluated comparisons back together.
nodes = [result.values[0]]
for value in result.values[1:]:
last_node = nodes[-1]
if (type(last_node) == ast.Compare
and type(value) == ast.Compare
and ast_equal(last_node.comparators[-1], value.left)):
nodes[-1] = ast.Compare(
left=last_node.left,
ops=last_node.ops + value.ops,
comparators=last_node.comparators + value.comparators)
else:
nodes.append(value)
if len(nodes) == 1:
return state, nodes[0]
else:
return state, ast.BoolOp(op=ast.And(), values=nodes)
