Issue 160, 161, 153, 164, 165, 167: Proof properties for applications

cement

@@ -9,23 +9,38 @@ import logging
 import xml.etree.ElementTree as ET
 
 parser = argparse.ArgumentParser()
-parser.add_argument("config", help="gneiss config file")
-parser.add_argument("gneiss_root", help="gneiss repository")
-parser.add_argument("-b", "--build_dir", help="build directory", default="build")
-parser.add_argument("-r", "--root_fs", help="use separate rootfs", default="build")
 parser.add_argument("-v", "--verbose", help="verbose output", action="store_true")
-parser.add_argument("paths", help="component search paths", nargs="*")
+subparsers = parser.add_subparsers(dest='command')
+build_parser = subparsers.add_parser("build")
+build_parser.add_argument("config", help="gneiss config file")
+build_parser.add_argument("gneiss_root", help="gneiss repository")
+build_parser.add_argument("-b", "--build_dir", help="build directory", default="build")
+build_parser.add_argument("-r", "--root_fs", help="use separate rootfs", default="build")
+build_parser.add_argument("-p", "--platform", help="target platform", default="linux")
+build_parser.add_argument("paths", help="component search paths", nargs="*")
+edit_parser = subparsers.add_parser("edit")
+edit_parser.add_argument("project", help="GPR project file")
+edit_parser.add_argument("gneiss_root", help="gneiss repository")
+edit_parser.add_argument("-b", "--build_dir", help="build directory", default="build")
+edit_parser.add_argument("paths", help="component search paths", nargs="*")
+prove_parser = subparsers.add_parser("prove")
+prove_parser.add_argument("project", help="GPR project file")
+prove_parser.add_argument("gneiss_root", help="gneiss repository")
+prove_parser.add_argument("-b", "--build_dir", help="build directory", default="build")
+prove_parser.add_argument("-u", "--unit", help="ada unit")
+prove_parser.add_argument("-s", "--steps", help="prove steps", default="8000")
+prove_parser.add_argument("paths", help="component search paths", nargs="*")
 
 def get_component_name(libname):
     return libname[13:-3]
 
-def build_init(root, outdir, default_args, logger):
-    args = default_args + ["-P", "init",
+def build_init(root, outdir, default_args, platform, logger):
+    args = default_args + ["-P", f"core",
             "-aP", root,
-            "-aP", root + "/init",
+            "-aP", root + f"/src/core/{platform}",
             "-aP", root + "/lib",
             "-XGNEISS_ROOT=" + root,
-            "-XCEMENT_OBJECT_DIR=" + os.path.join(outdir, "init"),
+            "-XCEMENT_OBJECT_DIR=" + os.path.join(outdir, f"core_{platform}"),
             "-XCEMENT_LIB_OBJECT_DIR=" + os.path.join(outdir, "libobjects/"),
             "-XCEMENT_LIBRARY_DIR=" + os.path.join(outdir, "libs")]
     logger.debug(args)
@@ -51,12 +66,12 @@ def find(name, path):
         if name in files:
             return os.path.join(root, name)
 
-def extract_init(build_dir, target_dir):
+def extract_init(build_dir, target_dir, platform):
     try:
         os.mkdir(target_dir)
     except FileExistsError:
         pass
-    shutil.copy2(find("init", os.path.join(build_dir, "init")), target_dir)
+    shutil.copy2(find("core", os.path.join(build_dir, f"core_{platform}")), target_dir)
 
 def extract_components(build_dir, target_dir, components):
     try:
@@ -77,15 +92,15 @@ def get_component_files(xml_file):
             raise ValueError(c)
     return components
 
-def gpr_compile(config, gneiss_root, build_dir, root_dir, paths, logger, verbose):
+def gpr_compile(config, gneiss_root, build_dir, root_dir, paths, platform, logger, verbose):
     logger.info("Compiling...")
     components = get_component_files(config)
     logger.info("Preparing init...")
     default_args = ["-p", "-XCEMENT_BUILD_STEP=prepare", "--db", os.path.join(gneiss_root, "gprconfig_db")]
     if args.verbose:
         default_args.append("-v")
-    if build_init(gneiss_root, build_dir, default_args, logger) > 0:
-        logger.error("Preparation of init failed")
+    if build_init(gneiss_root, build_dir, default_args, platform, logger) > 0:
+        logger.error("Preparation of core failed")
         exit(1)
     for c in components:
         logger.info("Preparing " + c + "...")
@@ -101,7 +116,7 @@ def gpr_compile(config, gneiss_root, build_dir, root_dir, paths, logger, verbose
     default_args = ["-p", "-XCEMENT_BUILD_STEP=compile"]
     if verbose:
         default_args.append("-v")
-    if build_init(gneiss_root, build_dir, default_args, logger) > 0:
+    if build_init(gneiss_root, build_dir, default_args, platform, logger) > 0:
         logger.error("Compilation of init failed")
         exit(1)
     for c in components:
@@ -129,12 +144,11 @@ def gpr_compile(config, gneiss_root, build_dir, root_dir, paths, logger, verbose
         os.mkdir(libdir)
     except FileExistsError:
         pass
-    extract_init(build_dir, bindir)
+    extract_init(build_dir, bindir, platform)
     extract_components(build_dir, libdir, components)
     logger.info("Finished.")
 
-def gpr_edit(name, root, build_dir, paths, logger):
-    logger.info("Editing...")
+def gpr_prepare(name, root, build_dir, paths):
     step_compile = ["-XCEMENT_BUILD_STEP=compile"]
     step_prepare = ["-XCEMENT_BUILD_STEP=prepare",
                     "--db", os.path.join(root, "gprconfig_db")]
@@ -152,12 +166,32 @@ def gpr_edit(name, root, build_dir, paths, logger):
     env["GPR_PROJECT_PATH_FILE"] = project_path_file
     gprbuild(["-p"] + args + step_prepare, env);
     gprbuild(["-p"] + args + step_compile, env);
+    return args, env, project_path_file
+
+
+def gpr_edit(name, root, build_dir, paths, logger):
+    logger.info("Editing...")
+    args, env, project_path_file = gpr_prepare(name, root, build_dir, paths)
+    logger.debug(args)
+    logger.debug(env["GPR_PROJECT_PATH_FILE"])
+    proc = subprocess.Popen(["gnatstudio"] + args + ["-XCEMENT_BUILD_STEP=compile"], env=env)
+    logger.debug(f"Popen: {proc.args}")
+    proc.communicate()
+    os.remove(project_path_file)
+
+def gpr_prove(name, root, build_dir, paths, steps, unit, logger):
+    logger.info("Editing...")
+    args, env, project_path_file = gpr_prepare(name, root, build_dir, paths)
     logger.debug(args)
     logger.debug(env["GPR_PROJECT_PATH_FILE"])
-    proc = subprocess.Popen(["gnatstudio"] + args + step_compile, env=env)
+    args.extend(["-j0", f"--steps={steps}", "--checks-as-errors", "--prover=cvc4,z3,altergo"])
+    if unit:
+        args.extend(["-u", unit])
+    proc = subprocess.Popen(["gnatprove"] + args + ["-XCEMENT_BUILD_STEP=compile"], env=env)
     logger.debug(f"Popen: {proc.args}")
     proc.communicate()
     os.remove(project_path_file)
+    return proc.returncode
 
 if __name__ == "__main__":
     args = parser.parse_args(sys.argv[1:])
@@ -170,17 +204,20 @@ if __name__ == "__main__":
     gprargs = ["-XGNEISS_ROOT=" + os.path.abspath(args.gneiss_root)]
     logger.info("Gneiss root at " + gprargs[0])
     build_dir = os.path.abspath(args.build_dir)
-    root_dir = os.path.abspath(args.root_fs)
-    if args.config.endswith(".xml"):
+    if args.command == "build":
+        root_dir = os.path.abspath(args.root_fs)
         gpr_compile(args.config,
                     os.path.abspath(args.gneiss_root),
                     build_dir,
                     root_dir,
                     args.paths,
+                    args.platform,
                     logger,
                     args.verbose)
-    elif args.config.endswith(".gpr"):
-        gpr_edit(args.config, os.path.abspath(args.gneiss_root), build_dir, args.paths, logger)
+    elif args.command == "edit":
+        gpr_edit(args.project, os.path.abspath(args.gneiss_root), build_dir, args.paths, logger)
+    elif args.command == "prove":
+        exit(gpr_prove(args.project, os.path.abspath(args.gneiss_root), build_dir, args.paths, args.steps, args.unit, logger))
     else:
-        logger.error("Unknown file type: " + args.config)
+        logger.error(f"Command {args.command} not implemented")
         exit(1)