Merge pull request #1 from jesusjda/unstable

pre v1.2

.gitignore

@@ -1,3 +1,6 @@
+# Launch script
+irankfinder.sh
+
 # Subproyects
 pyParser/
 pyLPi/

.pydevproject

@@ -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 3.0</pydev_property>
+<pydev_property name="org.python.pydev.PYTHON_PROJECT_VERSION">python interpreter</pydev_property>
 <pydev_property name="org.python.pydev.PYTHON_PROJECT_INTERPRETER">Default</pydev_property>
 </pydev_project>

CFRefinement.py

@@ -3,15 +3,23 @@
 import argparse
 import genericparser
 from termination import Output_Manager as OM
-from irankfinder import control_flow_refinement
-from irankfinder import compute_invariants
-from irankfinder import showgraph
+from partialevaluation import control_flow_refinement
+from nodeproperties import invariant
+from termination.algorithm.utils import showgraph
 
-_version = "1.0"
+_version = "1.2"
 _name = "CFRefinement"
 
+
+def threshold_type(value):
+    from nodeproperties.thresholds import threshold_options
+    if value in threshold_options():
+        return value
+    raise argparse.ArgumentTypeError("{} is not a valid threshold mode.".format(value))
+
+
 def setArgumentParser():
-    desc = _name+": Control Flow refinement."
+    desc = _name + ": Control Flow refinement."
     absdomains = ["none", "interval", "polyhedra"]
     argParser = argparse.ArgumentParser(
         description=desc,
@@ -30,65 +38,84 @@ def setArgumentParser():
                            help="Folder to save output files.")
     argParser.add_argument("-si", "--show-with-invariants", required=False, default=False,
                            action='store_true', help="add invariants to the output formats")
-
     # CFR Parameters
-    argParser.add_argument("-cfr-au", "--cfr-automatic-properties", required=False,
-                           type=int, choices=range(0,5), default=4, help="")
-    argParser.add_argument("-cfr-it", "--cfr-iterations", type=int, choices=range(0, 5),
-                           help="# times to apply cfr", default=1)
-    # argParser.add_argument("-cfr-it-st", "--cfr-iteration-strategy", required=False,
-    #                       choices=["acumulate", "inmutate", "recompute"], default="recompute",
-    #                       help="")
     argParser.add_argument("-cfr-usr", "--cfr-user-properties", action='store_true',
                            help="")
-    argParser.add_argument("-cfr-inv", "--cfr-invariants", required=False, choices=absdomains,
+    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-it", "--cfr-iterations", type=int, choices=range(0, 5),
+                           help="# times to apply cfr", default=1)
+
+    argParser.add_argument("-cfr-inv", "--cfr-invariants", action='store_true',
                            default="none", 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("-i", "--invariants", required=False, choices=absdomains,
                            default="none", help="Compute Invariants.")
-    argParser.add_argument("-ithre", "--invariants-threshold", required=False,
-                           action='store_true', help="Use user thresholds.")
-    argParser.add_argument("-cfr-sc", "--cfr-simplify-constraints", required=False,
-                           default=False, action='store_true',
-                           help="Simplify constraints when CFR")
-    argParser.add_argument("-cfr-inv-thre", "--cfr-invariants-threshold", required=False,
-                           default=False, action='store_true',
-                           help="Use user thresholds for CFR invariants.")
+    argParser.add_argument("-inv-thre", "--invariants-threshold", required=False, default=[], nargs="+",
+                           type=threshold_type, help="Use thresholds.")
+    argParser.add_argument("-inv-wide-nodes", "--invariant-widening-nodes", required=False, nargs="*",
+                           default=[], help=".")
+    argParser.add_argument("-inv-wide-nodes-mode", "--invariant-widening-nodes-mode", required=False,
+                           default="all", choices=["cyclecutnodes", "all", "user"], help=".")
     # IMPORTANT PARAMETERS
     argParser.add_argument("-f", "--files", nargs='+', required=True,
                            help="File to be analysed.")
-    argParser.add_argument("--tmpdir", required=False, default=None,
+    argParser.add_argument("--tmpdir", required=False, default="/tmp",
                            help="Temporary directory.")
     return argParser
 
+
 def extractname(filename):
     f = os.path.split(filename)
-    b = os.path.split(f[0])
     c = os.path.splitext(f[1])
-    return os.path.join(b[1], c[0])
+    return c[0]
+
 
 def launch(config):
     for f in config["files"]:
         launch_file(config, f)
         OM.show_output()
 
+
 def launch_file(config, f):
+    writef = config["output_destination"] is not None
+    console = not writef or config["ei_out"]
+    invariant.set_configuration(config)
+    sufix = ""
     try:
         config["name"] = extractname(f)
-        pe_cfg = control_flow_refinement(genericparser.parse(f), config,
-                                         au_prop=config["cfr_automatic_properties"],
-                                         console=True, writef=True)
+        cfg = genericparser.parse(f)
+        cfg.build_polyhedrons()
+        invariant.compute_invariants(cfg, add_to_polyhedron=True)
+        pe_cfg = control_flow_refinement(cfg, config,
+                                         console=console, writef=writef)
         if config["invariants"] != "none":
             config["show_with_invariants"] = True
-            compute_invariants(pe_cfg, abstract_domain=config["invariants"],
-                               use_threshold=config["invariants_threshold"])
+            invariant.compute_invariants(pe_cfg, add_to_polyhedron=True)
             if config["cfr_iterations"] > 0:
-                sufix = "_cfr"+str(config["cfr_iterations"])
-            sufix += "_with_inv"+str(config["invariants"])
-            showgraph(pe_cfg, config, sufix=sufix, invariant_type=config["invariants"], console=True, writef=True)
+                sufix += "_cfr" + str(config["cfr_iterations"])
+            sufix += "_with_inv" + str(config["invariants"])
+            showgraph(pe_cfg, config, sufix=sufix, invariant_type=config["invariants"], console=console, writef=writef)
     except Exception as e:
-        OM.printf("Exception  -> "+str(e))
+        OM.printf("Exception  -> " + str(e))
         raise Exception() from e
 
+
 if __name__ == "__main__":
     try:
         argv = sys.argv[1:]
@@ -103,4 +130,3 @@ def launch_file(config, f):
     except Exception as e:
         OM.show_output()
         raise Exception() from e
-

CHANGES.txt

@@ -1,3 +1,17 @@
+v1.2 2019/01/23 (remove ppl dependecy at this level)
+- invariants and all nodeproperties are now independent from ppl.
+- all the algorithms are now independent from ppl.
+- minor other improvements.
+- pep8.
+v1.1 2018/12/19
+- check assertions of cfgs and refined cfgs
+- properties of projection are computed now on python side
+- remove no important variables has been moved.
+- partialevaluation now can handle simple sccs calling "prepare" first.
+- analyse termination and nontermination in one single call.
+- three possible strategies to apply CFR. After, at scc level and Before.
+- algorithm to compute nodes on the way to a set of nodes.
+- 'print-graphs' argument to print the fc and svg of the cfg and their correspoinding refined graphs.
 v0.5 2018/10/02
 
 v0.2 2018/09/19