From 3e9a07d973738c1c77b4223f89086a0fc6e0a9a3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 8 Jun 2020 23:20:33 +0200
Subject: [PATCH] [Analysis-scripts] update make-template

---
 bin/frama-c-script                       |   5 +-
 share/analysis-scripts/make_template.py  | 138 +++++++++++++++--------
 tests/fc_script/main.c                   |   2 +-
 tests/fc_script/make_template.input      |   5 +-
 tests/fc_script/oracle/GNUmakefile       |  76 +++++--------
 tests/fc_script/oracle/make_template.res |  13 ++-
 6 files changed, 133 insertions(+), 106 deletions(-)

diff --git a/bin/frama-c-script b/bin/frama-c-script
index a3dfda783a2..7fa99649748 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -36,7 +36,7 @@ usage() {
    echo ""
    echo "  - make-template [dir]"
    echo "      Interactively prepares a template for running analysis scripts,"
-   echo "      writing it to [dir/GNUmakefile]. [dir] is [.] if omitted."
+   echo "      writing it to [dir/GNUmakefile]. [dir] is [.frama-c] if omitted."
    echo ""
    echo "  - make-path"
    echo "      [for Frama-C developers and advanced users without Frama-C in the path]"
@@ -232,7 +232,8 @@ case "$command" in
         ;;
     "make-template")
         shift;
-        ${FRAMAC_SHARE}/analysis-scripts/make_template.py "$0" "$@";
+        export FRAMAC="${DIR}/frama-c"
+        ${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@";
         ;;
     "make-path")
         shift;
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
index bf862b7b51c..c660b9b0135 100755
--- a/share/analysis-scripts/make_template.py
+++ b/share/analysis-scripts/make_template.py
@@ -28,6 +28,9 @@
 import sys
 import os
 import re
+import shutil
+import shlex
+import glob
 from subprocess import Popen, PIPE
 from pathlib import Path
 
@@ -35,31 +38,45 @@ MIN_PYTHON = (3, 6) # for glob(recursive) and automatic Path conversions
 if sys.version_info < MIN_PYTHON:
     sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
 
-if len(sys.argv) > 3:
-    print("usage: %s path-to-frama-c-script [dir]" % sys.argv[0])
-    print("       creates a GNUmakefile for running Frama-C on a set of files,")
-    print("       interactively filling a template.")
+if len(sys.argv) > 2:
+    print(f"usage: {sys.argv[0]} [dir]")
+    print("       creates a Frama-C makefile in [dir] (default: .frama-c)")
     sys.exit(1)
 
-if not os.path.isfile(sys.argv[1]):
-    print("error: path to frama-c-script is not a file: " + sys.argv[1])
-    sys.exit(1)
+framac="frama-c"
+if not shutil.which(framac):
+    if os.environ.get("FRAMAC"):
+        framac = os.environ["FRAMAC"]
+    else:
+        sys.exit("error: frama-c must be in the PATH, "\
+                 "or in environment variable FRAMAC")
 
 jcdb = Path("compile_commands.json")
 
+dir = Path(sys.argv[1] if len(sys.argv) == 2 else ".frama-c")
+fc_stubs_c = dir / "fc_stubs.c"
+gnumakefile = dir / "GNUmakefile"
+
+print(f"Preparing template: {gnumakefile}")
+
+# relative prefix, due to GNUmakefile possibly being in a sub-directory of PWD
+relprefix = os.path.relpath(os.getcwd(), dir)
+
 if "PTESTS_TESTING" in os.environ:
     print("Running ptests: setting up mock files...")
     jcdb.touch()
+    Path(dir).mkdir(parents=True, exist_ok=True)
+    fc_stubs_c.touch()
+    gnumakefile.touch()
 
-bindir = Path(os.path.dirname(os.path.abspath(sys.argv[1])))
+bindir = Path(os.path.dirname(os.path.abspath(framac)))
 frama_c_config = bindir / "frama-c-config"
 process = Popen([frama_c_config, "-print-share-path"], stdout=PIPE)
 (output, err) = process.communicate()
 output = output.decode('utf-8')
 exit_code = process.wait()
 if exit_code != 0:
-    print("error running frama-c-config")
-    sys.exit(1)
+    sys.exit("error running frama-c-config")
 sharedir = Path(output)
 
 def get_known_machdeps():
@@ -68,35 +85,53 @@ def get_known_machdeps():
     output = output.decode('utf-8')
     exit_code = process.wait()
     if exit_code != 0:
-        print("error getting machdeps: " + output)
-        sys.exit(1)
+        sys.exit("error getting machdeps: " + output)
     match = re.match("\[kernel\] supported machines are (.*) \(default is (.*)\).", output, re.DOTALL)
     if not match:
-        print("error getting known machdeps: " + output)
-        sys.exit(1)
+        sys.exit("error getting known machdeps: " + output)
     machdeps = match.group(1).split()
     default_machdep = match.group(2)
     return (default_machdep, machdeps)
 
-dir = Path(sys.argv[2] if len(sys.argv) == 3 else ".")
-gnumakefile = dir / "GNUmakefile"
-
 def check_path_exists(path):
     if os.path.exists(path):
-        yn = input("warning: {} already exists. Overwrite? [y/N] ".format(path))
+        yn = input(f"warning: {path} already exists. Overwrite? [y/N] ")
         if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
             print("Exiting without overwriting.")
             sys.exit(0)
+    pathdir = os.path.dirname(path)
+    if not os.path.exists(pathdir):
+        yn = input(f"warning: directory '{pathdir}' does not exit. Create it? [y/N] ")
+        if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
+            print("Exiting without creating.")
+            sys.exit(0)
+        Path(pathdir).mkdir(parents=True, exist_ok=False)
 
 check_path_exists(gnumakefile)
 main = input("Main target name: ")
 if not re.match("^[a-zA-Z_0-9]+$", main):
-    print("error: invalid main target name")
-    sys.exit(1)
-
-sources = input("Source files separated by spaces (default if empty: *.c): ")
-if not sources:
-    sources="*.c"
+    sys.exit("error: invalid main target name (can only contain letters, digits, dash or underscore)")
+
+def expand_and_normalize_sources(expression, relprefix):
+    subexps = shlex.split(expression)
+    sources_lists = [glob.glob(exp, recursive=True) for exp in subexps]
+    sources = sorted(set([item for sublist in sources_lists for item in sublist]))
+    return [f"  {source} \\" if os.path.isabs(source) else f"  {relprefix}/{source} \\" for source in sources]
+
+while True:
+    sources = input("Source files (default: **/*.c): ")
+    if not sources:
+        sources="**/*.c"
+    source_list = expand_and_normalize_sources(sources, relprefix)
+    if not source_list:
+        print(f"error: no sources were matched for '{sources}'.")
+    else:
+        print(f"The following sources were matched (relative to {dir}):")
+        print("\n".join(source_list))
+        print()
+        yn = input("Is this ok? [Y/n] ")
+        if yn == "" or not (yn[0] == "N" or yn[0] == "n"):
+            break
 
 json_compilation_database = None
 if jcdb.is_file():
@@ -110,20 +145,19 @@ add_main_stub = False
 yn = input("Add stub for function main (only needed if it uses command-line arguments)? [y/N] ")
 if yn != "" and (yn[0] == "Y" or yn[0] == "y"):
     add_main_stub = True
-    sources = "fc_stubs.c " + sources
 
 print("Please define the architectural model (machdep) of the target machine.")
 (default_machdep, machdeps) = get_known_machdeps()
 print("Known machdeps: " + " ".join(machdeps))
 machdep_chosen = False
 while not machdep_chosen:
-    machdep = input("Please enter the machdep [" + default_machdep + "]: ")
+    machdep = input(f"Please enter the machdep [{default_machdep}]: ")
     if not machdep:
         machdep = default_machdep
         machdep_chosen = True
     else:
         if not (machdep in machdeps):
-            yn = input("'{}' is not a standard machdep. Proceed anyway? [y/N]".format(machdep))
+            yn = input(f"'{machdep}' is not a standard machdep. Proceed anyway? [y/N]")
             if yn != "" and (yn[0] == "Y" or yn[0] == "y"):
                 machdep_chosen = True
         else:
@@ -135,17 +169,21 @@ def insert_line_after(lines, line_pattern, newline):
         if re_line.search(lines[i]):
             lines.insert(i+1, newline)
             return lines
-    print("error: no lines found matching pattern: " + line_pattern)
-    sys.exit(1)
+    sys.exit(f"error: no lines found matching pattern: {line_pattern}")
 
-def replace_line(lines, line_pattern, value):
+def replace_line(lines, line_pattern, value, all_occurrences=False):
+    replaced = False
     re_line = re.compile(line_pattern)
     for i in range(0, len(lines)):
         if re_line.search(lines[i]):
             lines[i] = value
-            return lines
-    print("error: no lines found matching pattern: " + line_pattern)
-    sys.exit(1)
+            replaced = True
+            if not all_occurrences:
+                return lines
+    if replaced:
+        return lines
+    else:
+        sys.exit(f"error: no lines found matching pattern: {line_pattern}")
 
 def remove_lines_between(lines, start_pattern, end_pattern):
     re_start = re.compile(start_pattern)
@@ -159,34 +197,34 @@ def remove_lines_between(lines, start_pattern, end_pattern):
             last_to_remove = i
             break
     if first_to_remove == -1:
-        print("error: could not find start pattern: " + start_pattern)
-        sys.exit(1)
+        sys.exit("error: could not find start pattern: " + start_pattern)
     elif last_to_remove == -1:
-        print("error: could not find end pattern: " + end_pattern)
-        sys.exit(1)
+        sys.exit("error: could not find end pattern: " + end_pattern)
     return (lines[:first_to_remove-1] if first_to_remove > 0 else []) + (lines[last_to_remove+1:] if last_to_remove < len(lines)-1 else [])
 
 with open(sharedir / "analysis-scripts" / "template.mk") as f:
     lines = list(f)
-    lines = replace_line(lines, "^MAIN_TARGET :=", "MAIN_TARGET := {}\n".format(main))
-    lines = remove_lines_between(lines, "Remove these lines.*main target", "^endif")
-    lines = replace_line(lines, "^\$\(MAIN_TARGET\).parse:", "$(MAIN_TARGET).parse: {}\n".format(sources))
-    if json_compilation_database:
-      lines = insert_line_after(lines, "^FCFLAGS", "  -json-compilation-database {} \\\n".format(json_compilation_database))
-    lines = insert_line_after(lines, "^FCFLAGS", "  -machdep {} \\\n".format(machdep))
+    lines = replace_line(lines, "^MACHDEP = .*", f"MACHDEP = {machdep}\n")
     if add_main_stub:
-        check_path_exists("fc_stubs.c")
-        from shutil import copyfile
-        copyfile(sharedir / "analysis-scripts" / "fc_stubs.c", "fc_stubs.c")
+        lines = insert_line_after(lines, "^main.parse: \\\\", f"  fc_stubs.c \\\n")
+        check_path_exists(fc_stubs_c)
+        shutil.copyfile(sharedir / "analysis-scripts" / "fc_stubs.c", fc_stubs_c)
         lines = insert_line_after(lines, "^FCFLAGS", "  -main eva_main \\\n")
-        print("Created stub for main function: fc_stubs.c")
+        print(f"Created stub for main function: {dir / 'fc_stubs.c'}")
+    lines = replace_line(lines, "^main.parse: \\\\", f"{main}.parse: \\\n")
+    lines = replace_line(lines, "^TARGETS = main.eva", f"TARGETS = {main}.eva\n")
+    lines = replace_line(lines, "^  main.c \\\\", "\n".join(source_list) + "\n")
+    if json_compilation_database:
+      lines = insert_line_after(lines, "^FCFLAGS", f"  -json-compilation-database {json_compilation_database} \\\n")
+    if relprefix != "..":
+        lines = replace_line(lines, "^  -add-symbolic-path=.:.. \\\\", f"  -add-symbolic-path=.:{relprefix} \\\n", all_occurrences=True)
 
 gnumakefile.write_text("".join(lines))
 
-print("Template created: " + gnumakefile.name)
+print(f"Template created: {gnumakefile}")
 
 if "PTESTS_TESTING" in os.environ:
     print("Running ptests: cleaning up after tests...")
     jcdb.unlink()
-    if add_main_stub:
-        Path("fc_stubs.c").unlink()
+    fc_stubs_c.unlink()
+    # gnumakefile is not erased because we want it as an oracle
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
index 74219d5a718..d3e15e1b85e 100644
--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -1,6 +1,6 @@
 /* run.config
    NOFRAMAC: testing frama-c-script, not frama-c itself
-   EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= bin/frama-c-script make-template @PTEST_DIR@/result < @PTEST_DIR@/make_template.input > @PTEST_DIR@/result/make_template.res 2> @PTEST_DIR@/result/make_template.err
+   EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err cd @PTEST_DIR@ && PTESTS_TESTING= ../../bin/frama-c-script make-template result < make_template.input > result/make_template.res 2> result/make_template.err
    EXECNOW: LOG list_files.res LOG list_files.err bin/frama-c-script list-files @PTEST_DIR@/list_files.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
    EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 bin/frama-c-script flamegraph @PTEST_DIR@/flamegraph.txt @PTEST_DIR@/result > @PTEST_DIR@/result/flamegraph.res 2> @PTEST_DIR@/result/flamegraph.err && rm -f @PTEST_DIR@/result/flamegraph.svg
    EXECNOW: LOG find_fun1.res LOG find_fun1.err bin/frama-c-script find-fun main2 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun1.res 2> @PTEST_DIR@/result/find_fun1.err
diff --git a/tests/fc_script/make_template.input b/tests/fc_script/make_template.input
index 62488cfcb33..6963df94935 100644
--- a/tests/fc_script/make_template.input
+++ b/tests/fc_script/make_template.input
@@ -1,7 +1,10 @@
+y
 fc_script_main
-file1.c file*.c dir/more_files.c
+for-find*.c main*.c
+y
 y
 y
 invalid_machdep
 n
 x86_64
+y
diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile
index 44f773a61a3..36b3398ec2a 100644
--- a/tests/fc_script/oracle/GNUmakefile
+++ b/tests/fc_script/oracle/GNUmakefile
@@ -1,68 +1,46 @@
-# TEMPLATE FOR MAKEFILE TO USE IN FRAMA-C/EVA CASE STUDIES
+# Makefile template for Frama-C/Eva case studies.
+# For details and usage information, see the Frama-C User Manual.
 
-# DO NOT EDIT THE LINES BETWEEN THE '#'S
-
-###############################################################################
-# Improves analysis time, at the cost of extra memory usage
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-#
-# frama-c-path.mk contains variables which are specific to each
-# user and should not be versioned, such as the path to the
-# frama-c binaries (e.g. FRAMAC and FRAMAC_GUI).
-# It is an optional include, unnecessary if frama-c is in the PATH
--include frama-c-path.mk
-#
-# FRAMAC is defined in frama-c-path.mk when it is included, so the
-# line below will be safely ignored if this is the case
+### Prologue. Do not modify this block. #######################################
+-include path.mk
 FRAMAC ?= frama-c
-#
-# frama-c.mk contains the main rules and targets
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-#
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
 ###############################################################################
 
-# EDIT VARIABLES AND TARGETS BELOW AS NEEDED
-# The flags below are only suggestions to use with Eva, and can be removed
+# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
+
+MACHDEP = x86_64
 
-# (Optional) preprocessing flags, usually handled by -json-compilation-database
+## Preprocessing flags (for -cpp-extra-args)
 CPPFLAGS    +=
 
-# (Optional) Frama-C general flags (parsing and kernel)
+## General flags
 FCFLAGS     += \
-  -main eva_main \
   -machdep x86_64 \
   -json-compilation-database . \
+  -main eva_main \
   -kernel-warn-key annot:missing-spec=abort \
   -kernel-warn-key typing:implicit-function-declaration=abort \
 
-# (Optional) Eva-specific flags
+## Eva-specific flags
 EVAFLAGS    += \
   -eva-warn-key builtins:missing-spec=abort \
 
-# (MANDATORY) Name of the main target
-MAIN_TARGET := fc_script_main
+## GUI-only flags
+FCGUIFLAGS +=
 
-# Add other targets if needed
-TARGETS = $(MAIN_TARGET).eva
+## Analysis targets (suffixed with .eva)
+TARGETS = fc_script_main.eva
 
-# Default target
-all: $(TARGETS)
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+fc_script_main.parse: \
+  fc_stubs.c \
+  ../for-find-fun.c \
+  ../for-find-fun2.c \
+  ../main.c \
+  ../main2.c \
+  ../main3.c \
 
-# (MANDATORY) List of source files used by MAIN_TARGET.
-# If there is a JSON compilation database,
-# 'frama-c-script list-files' can help obtain it
-$(MAIN_TARGET).parse: fc_stubs.c file1.c file*.c dir/more_files.c
-
-
-# The following targets are optional and provided for convenience only
-parse: $(TARGETS:%.eva=%.parse)
-loop: $(TARGETS:%.eva=%.parse.loop) $(TARGETS:%=%.loop)
-gui: $(MAIN_TARGET).eva.gui
-
-# Run 'make <TARGET>.eva.loop' to obtain a .loop file, fine-tune it by hand,
-# then rename it to <TARGET>.slevel to prevent it from being overwritten.
-# If such file exists, use it to define per-function slevel values.
-ifneq (,$(wildcard $(MAIN_TARGET).slevel))
-$(MAIN_TARGET).eva: \
-  EVAFLAGS += $(shell cat $(MAIN_TARGET).slevel | tr -d '\n\\')
-endif
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
+###############################################################################
diff --git a/tests/fc_script/oracle/make_template.res b/tests/fc_script/oracle/make_template.res
index 9f38d9c7e74..26616f9c038 100644
--- a/tests/fc_script/oracle/make_template.res
+++ b/tests/fc_script/oracle/make_template.res
@@ -1,6 +1,13 @@
 Running ptests: setting up mock files...
-Main target name: Source files separated by spaces (default if empty: *.c): compile_commands.json exists, add option -json-compilation-database? [Y/n] Add stub for function main (only needed if it uses command-line arguments)? [y/N] Please define the architectural model (machdep) of the target machine.
+warning: result/GNUmakefile already exists. Overwrite? [y/N] Main target name: Source files (default: **/*.c): The following sources were matched (relative to result):
+  ../for-find-fun.c \
+  ../for-find-fun2.c \
+  ../main.c \
+  ../main2.c \
+  ../main3.c \
+
+Is this ok? [Y/n] compile_commands.json exists, add option -json-compilation-database? [Y/n] Add stub for function main (only needed if it uses command-line arguments)? [y/N] Please define the architectural model (machdep) of the target machine.
 Known machdeps: x86_16 x86_32 x86_64 gcc_x86_16 gcc_x86_32 gcc_x86_64 ppc_32 msvc_x86_64
-Please enter the machdep [x86_32]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_32]: Created stub for main function: fc_stubs.c
-Template created: GNUmakefile
+Please enter the machdep [x86_32]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_32]: warning: result/fc_stubs.c already exists. Overwrite? [y/N] Created stub for main function: result/fc_stubs.c
+Template created: result/GNUmakefile
 Running ptests: cleaning up after tests...
-- 
GitLab