Skip to content

Commit

Permalink
Merge branch 'unstable'
Browse files Browse the repository at this point in the history
  • Loading branch information
@jesusjda
jesusjda committed Jul 9, 2019
2 parents 92927bf + 7bd035f commit 2282006
Show file tree
Hide file tree
Showing 8 changed files with 314 additions and 56 deletions.
2 changes: 1 addition & 1 deletion .pydevproject
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,6 @@
<pydev_pathproperty name="org.python.pydev.PROJECT_SOURCE_PATH">
<path>/${PROJECT_DIR_NAME}</path>
</pydev_pathproperty>
<pydev_property name="org.python.pydev.PYTHON_PROJECT_VERSION">python interpreter</pydev_property>
<pydev_property name="org.python.pydev.PYTHON_PROJECT_VERSION">python 3.0</pydev_property>
<pydev_property name="org.python.pydev.PYTHON_PROJECT_INTERPRETER">Default</pydev_property>
</pydev_project>
5 changes: 3 additions & 2 deletions CFRefinement.py
100644 → 100755
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ def threshold_type(value):
def setArgumentParser():
desc = _name + ": Control Flow refinement."
absdomains = ["none", "interval", "polyhedra"]
output_formats = ["fc", "dot", "svg", "koat", "pl", "smt2"]
argParser = argparse.ArgumentParser(
description=desc,
formatter_class=argparse.RawTextHelpFormatter)
Expand All @@ -31,8 +32,8 @@ def setArgumentParser():
action='store_true', help="Shows the version.")
argParser.add_argument("--ei-out", required=False, action='store_true',
help="Shows the output supporting ei")
argParser.add_argument("-of", "--output_formats", required=False, nargs='+',
choices=["fc", "dot", "koat", "pl", "svg"], default=["fc", "dot", "svg"],
argParser.add_argument("-of", "--output-formats", required=False, nargs='+',
choices=output_formats, default=output_formats[:3],
help="Formats to print the graphs.")
argParser.add_argument("-od", "--output-destination", required=False,
help="Folder to save output files.")
Expand Down
85 changes: 50 additions & 35 deletions irankfinder.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,14 +54,52 @@ def nontermination_alg_desc():
"\n\t".join(NTAM.options(True)))


def setCFRArgumentsParser(group):
group.add_argument("-cfr-it", "--cfr-iterations", type=int, choices=range(0, 5),
help="# times to apply cfr", default=0)
group.add_argument("-cfr-mx-t", "--cfr-max-tries", type=int, choices=range(0, 5),
help="max tries to apply cfr on scc level", default=4)
group.add_argument("-cfr-st-before", "--cfr-strategy-before", action='store_true',
help="")
group.add_argument("-cfr-st-scc", "--cfr-strategy-scc", action='store_true',
help="")
group.add_argument("-cfr-st-after", "--cfr-strategy-after", action='store_true',
help="")
group.add_argument("-cfr-usr", "--cfr-user-properties", action='store_true',
help="")
group.add_argument("-cfr-cone", "--cfr-cone-properties", action='store_true',
help="")
group.add_argument("-cfr-head", "--cfr-head-properties", action='store_true',
help="")
group.add_argument("-cfr-head-var", "--cfr-head-var-properties", action='store_true',
help="")
group.add_argument("-cfr-call", "--cfr-call-properties", action='store_true',
help="")
group.add_argument("-cfr-call-var", "--cfr-call-var-properties", action='store_true',
help="")
group.add_argument("-cfr-john", "--cfr-john-properties", action='store_true',
help="")
group.add_argument("-cfr-split", "--cfr-split-properties", action='store_true',
help="")
group.add_argument("-cfr-inv", "--cfr-invariants", action='store_true',
help="CFR with Invariants.")
group.add_argument("-cfr-nodes", "--cfr-nodes", required=False, nargs="*",
default=[], help=".")
group.add_argument("-cfr-nodes-mode", "--cfr-nodes-mode", required=False,
default="all", choices=["john", "cyclecutnodes", "all", "user"], help=".")


def setArgumentParser():
desc = _name + ": a Ranking Function finder on python."
dt_options = ["never", "iffail", "always"]
domains = ["Z", "Q", "user"]
dt_scheme_options = ["default", "inhomogeneous"]
absdomains = ["none", "interval", "polyhedra"]
output_formats = ["fc", "dot", "svg", "koat", "pl", "smt2"]
argParser = argparse.ArgumentParser(
description=desc,
formatter_class=argparse.RawTextHelpFormatter)
setCFRArgumentsParser(argParser.add_argument_group('cfr', "CFR parameters"))
# Output Parameters
argParser.add_argument("-v", "--verbosity", type=int, choices=range(0, 5),
help="increase output verbosity", default=0)
Expand All @@ -70,7 +108,7 @@ def setArgumentParser():
argParser.add_argument("-od", "--output-destination", required=False,
help="Folder to save output files.")
argParser.add_argument("-of", "--output-formats", required=False, nargs='+',
choices=["fc", "dot", "koat", "pl", "svg"], default=["fc", "dot", "svg"],
choices=output_formats, default=output_formats[:3],
help="Formats to print the graphs.")
argParser.add_argument("-si", "--show-with-invariants", required=False, default=False,
action='store_true', help="add invariants to the output formats")
Expand All @@ -81,6 +119,9 @@ def setArgumentParser():
argParser.add_argument("--print-graphs", required=False, action='store_true',
help="Shows the output in fc and svg format")
# Algorithm Parameters
argParser.add_argument("-d", "--domain", required=False,
choices=domains, default=domains[0],
help="Domain of the variables")
argParser.add_argument("-dt", "--different-template", required=False,
choices=dt_options, default=dt_options[0],
help="Use different templates on each node")
Expand All @@ -101,39 +142,6 @@ def setArgumentParser():
help="Check Invariants with the assertions defined")
argParser.add_argument("-rfs-as-cfr-props", "--rfs-as-cfr-props", action='store_true',
help="Print a graph with rfs as user props.")
# CFR Parameters
argParser.add_argument("-cfr-it", "--cfr-iterations", type=int, choices=range(0, 5),
help="# times to apply cfr", default=0)
argParser.add_argument("-cfr-mx-t", "--cfr-max-tries", type=int, choices=range(0, 5),
help="max tries to apply cfr on scc level", default=4)
argParser.add_argument("-cfr-st-before", "--cfr-strategy-before", action='store_true',
help="")
argParser.add_argument("-cfr-st-scc", "--cfr-strategy-scc", action='store_true',
help="")
argParser.add_argument("-cfr-st-after", "--cfr-strategy-after", action='store_true',
help="")
argParser.add_argument("-cfr-usr", "--cfr-user-properties", action='store_true',
help="")
argParser.add_argument("-cfr-cone", "--cfr-cone-properties", action='store_true',
help="")
argParser.add_argument("-cfr-head", "--cfr-head-properties", action='store_true',
help="")
argParser.add_argument("-cfr-head-var", "--cfr-head-var-properties", action='store_true',
help="")
argParser.add_argument("-cfr-call", "--cfr-call-properties", action='store_true',
help="")
argParser.add_argument("-cfr-call-var", "--cfr-call-var-properties", action='store_true',
help="")
argParser.add_argument("-cfr-john", "--cfr-john-properties", action='store_true',
help="")
argParser.add_argument("-cfr-split", "--cfr-split-properties", action='store_true',
help="")
argParser.add_argument("-cfr-inv", "--cfr-invariants", action='store_true',
help="CFR with Invariants.")
argParser.add_argument("-cfr-nodes", "--cfr-nodes", required=False, nargs="*",
default=[], help=".")
argParser.add_argument("-cfr-nodes-mode", "--cfr-nodes-mode", required=False,
default="all", choices=["john", "cyclecutnodes", "all", "user"], help=".")
argParser.add_argument("-scc-pl", "--print-scc-prolog", required=False,
help="File where print, on certain format, sccs that we don't know if terminate.")
# IMPORTANT PARAMETERS
Expand All @@ -142,6 +150,9 @@ def setArgumentParser():
argParser.add_argument("-nt", "--nontermination", type=nontermination_alg,
nargs='*', required=False, default=[],
help=nontermination_alg_desc())
argParser.add_argument("-nt-reach", "--nt-reachability", required=False,
default=False, action='store_true',
help="Analyse reachability when NT algorithms says NO.")
argParser.add_argument("-t", "--termination", type=termination_alg, default=[],
nargs='*', required=False,
help=termination_alg_desc())
Expand Down Expand Up @@ -188,7 +199,8 @@ def parse_file(f):
return genericparser.parse(f)


def launch_file(config, f, out):
def launch_file(gconfig, f, out):
config = dict(gconfig)
aux_p = f.split('/')
aux_c = len(aux_p) - 1
while aux_c > 0:
Expand All @@ -210,6 +222,8 @@ def launch_file(config, f, out):
OM.printerrf("Parser Error: {}\n{}".format(type(e).__name__, str(e)))
# raise Exception() from e
return
if "domain" in config and config["domain"] == "user":
config["domain"] = cfg.get_info("domain")
nodeproperties.invariant.set_configuration(config)
OM.restart(odest=out, cdest=r)
remove_no_important_variables(cfg, doit=config["remove_no_important_variables"])
Expand Down Expand Up @@ -305,6 +319,7 @@ def check_assertions(config, cfg):
OM.printf("Refining graph...")
from partialevaluation import control_flow_refinement
cfg = control_flow_refinement(cfg, config)
cfg.remove_unsat_edges()
OM.printf("Computing and checking invariants...")
nodeproperties.invariant.compute_invariants(cfg, check=True, add_to_polyhedron=False)
showgraph(cfg, config, sufix="cfr_before", console=config["print_graphs"], writef=False, output_formats=["fc", "svg"])
Expand Down
46 changes: 41 additions & 5 deletions termination/__init__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
from partialevaluation import control_flow_refinement
from partialevaluation import prepare_scc
from .algorithm.utils import compute_way_nodes
from termination.algorithm.utils import check_determinism

__all__ = ["NonTermination_Algorithm_Manager", "Termination_Algorithm_Manager", "Output_Manager", "Result", "TerminationResult", "analyse"]

Expand Down Expand Up @@ -97,7 +98,7 @@ def analyse(config, cfg):
if not R or not R.get_status().is_terminate():
# analyse NON-termination
if can_be_nonterminate:
R_nt = analyse_scc_nontermination(nt_algs, scc)
R_nt = analyse_scc_nontermination(nt_algs, cfg, scc, domain=config["domain"], do_reachability=config["nt_reachability"])
if R_nt and R_nt.get_status().is_nonterminate():
R_nt.set_response(graph=scc)
nonterminating_sccs.append(R_nt)
Expand Down Expand Up @@ -163,20 +164,27 @@ def analyse(config, cfg):
CFGs = new_sccs + CFGs
else:
stop_all = True

determ = None
status = TerminationResult.UNKNOWN
if can_be_nonterminate and len(nonterminating_sccs) > 0:
status = TerminationResult.NONTERMINATE
elif len(maybe_sccs) > 0:
determ = True
for scc in maybe_sccs:
determ = check_determinism(scc.get_edges(), scc.get_info("global_vars"))
if not determ:
break
status = TerminationResult.UNKNOWN
elif can_be_terminate:
status = TerminationResult.TERMINATE
response = Result()

response.set_response(status=status,
rfs=dict(rfs),
terminate=terminating_sccs[:],
nonterminate=nonterminating_sccs[:],
unknown_sccs=maybe_sccs[:],
deterministic=determ,
graph=original_cfg)
return response

Expand Down Expand Up @@ -211,7 +219,7 @@ def prepare_cfr_config(config):
return cfr, cfr_before, cfr_scc, cfr_after


def analyse_scc_nontermination(algs, scc, close_walk_depth=20):
def analyse_scc_nontermination(algs, cfg, scc, close_walk_depth=20, domain="Z", do_reachability=False):
cw_algs = [a for a in algs if a.use_close_walk()]
nt_algs = [a for a in algs if not a.use_close_walk()]
if len(nt_algs) > 0:
Expand All @@ -220,15 +228,43 @@ def analyse_scc_nontermination(algs, scc, close_walk_depth=20):
if response.get_status().is_nonterminate():
return response
if len(cw_algs) > 0:
for cw in scc.get_close_walks(close_walk_depth):
for cw in scc.get_close_walks(close_walk_depth, 1, linear=True):
OM.printif(1, "\nAnalysing Close Walk: {}.".format([t["name"] for t in cw]))
determ = check_determinism(cw, scc.get_info("global_vars"))
if not determ and domain == "Z":
OM.printif(1, "\t- Skiping because is not DET and domain is Z.")
continue
for a in cw_algs:
response = a.run(scc, cw)
response = a.run(scc, cw, domain)
response.set_response(reachability=False)
if do_reachability:
response = analyse_reachability(cfg, cw, response, domain)
if response.get_status().is_nonterminate():
response.set_response(deterministic=determ)
return response
return False


def analyse_reachability(cfg, cw, response, domain):
if not response.get_status().is_nonterminate():
return response
ntargument = None
if response.has("nt_argument"):
ntargument = response.get("nt_argument")
else:
raise Exception("no nt argument...")
from termination.algorithm.nonTermination import reachability
from genericparser import constants as gconsts
targets = list(set([tr["source"] for tr in cw]))

if reachability(cfg, ntargument, targets, domain=domain):
response.set_response(reachability=True)
return response
response.set_response(status=TerminationResult.UNKNOWN,
info="NTargument not reachable")
return response


def analyse_scc_termination(algs, cfg, dt_modes=[False], dt_scheme="default"):
trans = cfg.get_edges()
answer = Result()
Expand Down
76 changes: 71 additions & 5 deletions termination/algorithm/nonTermination.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ def __init__(self, properties={}):
def use_close_walk(cls):
return True

def run(self, cfg, close_walk=[]):
def run(self, cfg, close_walk=[], domain="Z"):
"""
looking for a fixpoint in a close walk:
[n0] -(x, xP)-> [n1] -(xP, x2)-> [n2] -(x2, x)-> [n0]
Expand All @@ -45,7 +45,10 @@ def run(self, cfg, close_walk=[]):
if c.is_linear()]
cons += cs
tr_idx += Nvars
s = Solver()
if domain == "Z":
s = Solver(variable_type="int", coefficient_type="int")
else:
s = Solver()
s.add(cons)
point, __ = s.get_point(taken_vars)
response = Result()
Expand All @@ -55,7 +58,8 @@ def run(self, cfg, close_walk=[]):
response.set_response(status=TerminationResult.NONTERMINATE,
info="FixPoint Found",
close_walk=close_walk,
fixpoint=fixpointvalue)
fixpoint=fixpointvalue,
nt_argument=C_Polyhedron(constraints=cons, variables=taken_vars))
else:
OM.printif(1, "No fixpoint found.")
response.set_response(status=TerminationResult.UNKNOWN,
Expand Down Expand Up @@ -90,7 +94,7 @@ def generate(cls, data):
return cls(properties)
return None

def run(self, cfg, close_walk=[]):
def run(self, cfg, close_walk=[], domain="Z"):
"""
looking for a Monotonic Recurrent Set in a close walk:
[n0] -(x0, x1)-> [n1] -(x1, x2)-> [n2] -(x2, xP)-> [n0]
Expand Down Expand Up @@ -158,7 +162,8 @@ def run(self, cfg, close_walk=[]):
response.set_response(status=TerminationResult.NONTERMINATE,
info="Recurrent Set Found:",
close_walk=close_walk,
rec_set=tr_poly)
rec_set=tr_poly,
nt_argument=tr_poly)
return response
tr_poly = tr_poly_p
depth += 1
Expand Down Expand Up @@ -186,3 +191,64 @@ def get_algorithm(cls, token):
continue
return alg
raise ValueError("Not Valid token")


def reachability(cfg, goal, goal_nodes, source=None, domain="Q"):
if source is None:
from genericparser import constants
source = cfg.get_info(constants.initnode)
from lpi import Solver
from genericparser import constants as gconsts
for cons, path in bfs_paths(cfg, source, goal_nodes, goal):
if domain == "Z":
s = Solver(variable_type="int", coefficient_type="int")
else:
s = Solver()
s.add(cons)
OM.printif(3, s)
if s.is_sat():
OM.printif(1, "reachable with path", path)
OM.printif(1, s.get_point(cfg.get_info(gconsts.variables)))
return True
else:
OM.printif(1, "NO reachable with path", path)
return False


def bfs_paths(cfg, source, target, goal):
from genericparser import constants as gconsts
targets = [target] if not isinstance(target, list) else target
gvars = cfg.get_info(gconsts.variables)
N = int(len(gvars) / 2)
_vars = gvars[:N]
_pvars = gvars[N:]

def gen_names(vs, it):
return vs[:] if it == 0 else [v + "#" + str(it) for v in vs]

def gen_local(vs, it):
return gen_names(vs, "L" + str(it))

def add_tr(cons, tr, it):
tr_vars = gen_names(_vars, it - 1) + gen_names(_vars, it) + gen_local(tr[gconsts.transition.localvariables], it)
cons = cons + [c for c in tr[gconsts.transition.polyhedron].get_constraints(tr_vars)
if c.is_linear()]
return cons

trs = {t["name"]: t for t in cfg.get_edges()}
trs["#dummy"] = {"target": source}
queue = [([], ["#dummy"])]

while queue:
(cons, path) = queue.pop(0)
last = path[-1]
for tr in cfg.get_edges(source=trs[last]["target"]):
if path.count(tr["name"]) >= 2:
continue
new_cons = add_tr(cons, tr, len(path))
if tr["target"] in targets:
tr_vars = gen_names(_vars, len(path)) + _pvars + gen_local(goal.get_variables()[2 * N:], len(path))
new_cons = new_cons + goal.get_constraints(tr_vars)
yield (new_cons, path[1:] + [tr["name"]])
else:
queue.append((new_cons, path + [tr["name"]]))
Loading

0 comments on commit 2282006

Please sign in to comment.