Files
spark2014/scripts/testgen.py
2025-04-16 08:59:43 +00:00

259 lines
6.7 KiB
Python
Executable File

import os
import sys
import json
import argparse
import subprocess
def run_spark(project_file, filename, line):
print("Running gnatprove")
subprocess.run(
[
"gnatprove",
f"-P{project_file}",
"-j0",
"--output=oneline",
"-u",
"--counterexamples=on",
"--check-counterexamples=on",
"--level=2",
f"--limit-subp={filename}:{line}",
]
)
def run_gnattest(project_name, filename, line):
print(f"Running gnattest at {(filename)}:{str(line)}")
subprocess.run(
[
"gnattest",
f"-P{project_name}",
filename,
f"--gen-test-subprograms={filename}:{str(line)}",
"--gen-test-vectors",
"--gen-test-num=1",
]
)
def get_hash(project_name, filename, line):
print(
f"Retrieving {project_name} subprogram's hash16 at "
+ f"{(filename)}:{str(line)}"
)
command = ["gnattest", f"-P{project_name}", f"--dump-subp-hash={filename}:{line}"]
process = subprocess.run(command, capture_output=True, text=True)
return process.stdout.strip("\n").strip("\t")
def get_values_from_spark_JSON(JSON_file, source_file, source_line):
print(f"Retrieving counter-example's values from {os.path.abspath(JSON_file)}.")
try:
with open(JSON_file, "r") as f:
data = json.load(f)
proofs = data.get("proof", {})
for proof in proofs:
cntexmp_value = proof.get("cntexmp_value", {})
subp_file = cntexmp_value.get("subp_file")
subp_line = cntexmp_value.get("subp_line")
if subp_file == source_file and str(subp_line) == source_line:
return cntexmp_value.get("inputs", {})
return None
except FileNotFoundError:
print(f"Error: filename {JSON_file} not found.")
return None
except json.JSONDecodeError:
print(f"Error: Invalid JSON format in {JSON_file}.")
return None
except Exception as e:
print(f"An unexpected error occurred: {e}")
return None
def get_subprogram(JSON_file):
print(
"Retrieving subprogram's declaration location from "
+ f"{os.path.abspath(JSON_file)}"
)
try:
with open(JSON_file, "r") as f:
data = json.load(f)
flows = data.get("flow", {})
for flow in flows:
if flow.get("rule", {}) == "SUBPROGRAM_TERMINATION":
filename = flow.get("file", {})
line = flow.get("line", {})
return [filename, line]
sys.exit("error: subprogram not found.")
except FileNotFoundError:
print(f"Error: filename {JSON_file} not found.")
return None
except json.JSONDecodeError:
print(f"Error: Invalid JSON format in {JSON_file}.")
return None
except Exception as e:
print(f"An unexpected error occurred: {e}")
return None
def replace_values(JSON_file, subp_hash, values):
print(f"Replacing gnattest values by SPARK's in {os.path.abspath(JSON_file)}.")
try:
with open(JSON_file, "r") as f:
data = json.load(f)
subprogram = data.get(subp_hash, {})
if subprogram == {}:
sys.exit("error: hashes do not match") # This should never happen
test_vectors = data.get(subp_hash, {}).get("test_vectors", {})
param_vectors = test_vectors[0].get("param_values", {})
for value in values:
name = value.get("name", {})
val = value.get("value", {})
for param in param_vectors:
if param.get("name", {}) == name:
param["value"] = val
with open(JSON_file, "w") as f:
json.dump(data, f, indent=4)
except FileNotFoundError:
print(f"Error: filename {JSON_file} not found.")
return None
except json.JSONDecodeError:
print(f"Error: Invalid JSON format in {JSON_file}.")
return None
def generate_tests(project_name, filename, line):
print("Generating tests")
subprocess.run(
[
"gnattest",
f"-P{project_name}",
f"--gen-test-subprograms={filename}:{str(line)}",
]
)
def run(project_file, filename, line):
project_path = os.path.dirname(os.path.realpath(project_file))
os.chdir(project_path)
# SPARK step
run_spark(project_file, filename, line)
spark_filenames = []
for file in os.listdir(os.path.join(project_path, "obj/gnatprove/")):
if file.endswith(".spark"):
spark_filenames.append(file)
if spark_filenames == []:
sys.exit("could not find generated .spark file.")
ce_values = None
for spark_filename in spark_filenames:
ce_values = get_values_from_spark_JSON(
os.path.join(project_path, "obj/gnatprove/", spark_filename), filename, line
)
if ce_values is not None:
break
if ce_values is None:
sys.exit("no counter-example at " + filename + ":" + line)
print(f"counter-example values: {str(ce_values)}")
# gnattest step
[project_name, _] = [s for s in project_file.split(".") if s.strip()]
hash_value = get_hash(project_name, os.path.join("src/", filename), line)
run_gnattest(project_name, filename, line)
replace_values(
os.path.join(
project_path,
"obj",
"gnattest",
"tests",
"JSON_Tests",
f"{project_name}.json",
),
hash_value,
ce_values,
)
generate_tests(project_name, filename, line)
print(
"tests have been generated and can be found at "
+ f"{os.path.abspath(project_path + "/obj/gnattest/tests/")}"
)
# run tests
os.chdir("obj/gnattest/harness")
subprocess.run("make")
subprocess.run(["./test_runner", f"--routines={filename}:{str(line)}"])
def main():
parser = argparse.ArgumentParser(
prog="Testgen",
description="Generate a ADA test harness from gnatprove's counter-exemples",
)
parser.add_argument(
"-p",
help="Path to the project file",
required=True,
type=str,
dest="project_file",
)
parser.add_argument(
"-s",
help="file:line of the subprogram to generate tests from",
required=True,
type=str,
dest="position",
)
args = parser.parse_args()
project_path = args.project_file
[filename, line] = [s for s in args.position.split(":") if s.strip()]
run(project_path, filename, line)
if __name__ == "__main__":
main()