cement

#!/usr/bin/env python3

import sys
import os
import argparse
import subprocess
import shutil
import logging
import xml.etree.ElementTree as ET

parser = argparse.ArgumentParser()
parser.add_argument("-v", "--verbose", help="verbose output", action="store_true")
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_gcc_version():
    return subprocess.check_output(["gcc", "-dumpversion"]).decode('utf-8').strip().split('.')[0]

def get_component_name(libname):
    return libname[13:-3]

def build_init(root, outdir, default_args, platform, logger):
    args = default_args + ["-P", f"core",
            "-aP", root,
            "-aP", root + f"/src/core/{platform}",
            "-aP", root + "/lib",
            "-XGNEISS_ROOT=" + root,
            "-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)
    return gprbuild(args)

def build_component(name, root, paths, outdir, default_args, logger):
    args = default_args + ["-P", name, "-aP", root,
                           "-XGNEISS_ROOT=" + root,
                           "-XCEMENT_OBJECT_DIR=" + os.path.join(outdir, os.path.join("components", name)),
                           "-XCEMENT_LIB_OBJECT_DIR=" + os.path.join(outdir, "libobjects/"),
                           "-XCEMENT_LIBRARY_DIR=" + os.path.join(outdir, "libs"),
                           "-XCEMENT_COMPONENT_DIR=" + os.path.join(outdir, "libcomponents")]
    for p in paths:
        args.extend(["-aP", p])
    logger.debug(args)
    return gprbuild(args)

def gprbuild(args, env=None):
    return subprocess.call(["gprbuild"] + args, env=env)

def find(name, path):
    for root, dirs, files in os.walk(path):
        if name in files:
            return os.path.join(root, name)

def extract_init(build_dir, target_dir, platform):
    try:
        os.mkdir(target_dir)
    except FileExistsError:
        pass
    shutil.copy2(find("core", os.path.join(build_dir, f"core_{platform}")), target_dir)

def extract_components(build_dir, target_dir, components):
    try:
        os.mkdir(target_dir)
    except FileExistsError:
        pass
    for c in components:
        shutil.copy2(find(c, os.path.join(build_dir, "libcomponents")), target_dir)

def get_component_files(xml_file):
    config_root = ET.parse(xml_file).getroot()
    components = set()
    for c_tag in config_root.findall("component"):
        c = c_tag.get("file")
        if c.startswith("libcomponent_") and c.endswith(".so"):
            components.add(c)
        else:
            raise ValueError(c)
    return components

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"),
                    "-XGCC_VERSION=" + get_gcc_version()]
    if args.verbose:
        default_args.append("-v")
    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 + "...")
        if build_component(get_component_name(c),
                           gneiss_root,
                           [os.path.abspath(p) for p in paths],
                           build_dir,
                           default_args,
                           logger) > 0:
            logger.error("Preparation of " + c + " failed")
            exit(1)
    logger.info("Compiling init...")
    default_args = ["-p", "-XCEMENT_BUILD_STEP=compile",
                    "-XGCC_VERSION=" + get_gcc_version()]
    if verbose:
        default_args.append("-v")
    if build_init(gneiss_root, build_dir, default_args, platform, logger) > 0:
        logger.error("Compilation of init failed")
        exit(1)
    for c in components:
        logger.info("Compiling " + c + "...")
        if build_component(get_component_name(c),
                           gneiss_root,
                           [os.path.abspath(p) for p in args.paths],
                           build_dir,
                           default_args,
                           logger) > 0:
            logger.error("Compilation of " + c + " failed")
            exit(1)
    logger.info("Extracting results...")
    try:
        os.mkdir(root_dir)
    except FileExistsError:
        pass
    bindir = os.path.join(root_dir, "bin")
    try:
        os.mkdir(bindir)
    except FileExistsError:
        pass
    libdir = os.path.join(root_dir, "lib")
    try:
        os.mkdir(libdir)
    except FileExistsError:
        pass
    extract_init(build_dir, bindir, platform)
    extract_components(build_dir, libdir, components)
    logger.info("Finished.")

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")]
    args = ["-P", name,
            "-XGNEISS_ROOT=" + root,
            "-XCEMENT_OBJECT_DIR=" + os.path.join(build_dir, name[:-4] + "_obj"),
            "-XCEMENT_LIB_OBJECT_DIR=" + os.path.join(build_dir, name[:-4] + "_libobj"),
            "-XCEMENT_LIBRARY_DIR=" + os.path.join(build_dir, name[:-4] + "_lib"),
            "-XCEMENT_COMPONENT_DIR=" + os.path.join(build_dir, name[:-4] + "_component"),
            "-XGCC_VERSION=" + get_gcc_version()]
    project_path_file = "/tmp/cement_gpr_project_path." + str(os.getpid())
    with open(project_path_file, "w+") as ppf:
        for path in [root] + paths:
            ppf.write(os.path.abspath(path) + "\n")
    env = os.environ.copy()
    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"])
    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:])
    logger = logging.getLogger("Cement")
    logger.setLevel(logging.DEBUG if args.verbose else logging.INFO);
    fmt = logging.Formatter("%(levelname)s: %(message)s")
    sh = logging.StreamHandler()
    sh.setFormatter(fmt)
    logger.addHandler(sh)
    gprargs = ["-XGNEISS_ROOT=" + os.path.abspath(args.gneiss_root)]
    logger.info("Gneiss root at " + gprargs[0])
    build_dir = os.path.abspath(args.build_dir)
    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.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(f"Command {args.command} not implemented")
        exit(1)