From 801d2ae678e282b4cb99aa1c48dd1643f88b7eca Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 9 Jun 2020 11:41:32 +0200
Subject: [PATCH] [Analysis-scripts] improve template, make-template,
make-path; refactor find-fun
---
Makefile | 2 +
bin/frama-c-script | 11 +++++
headers/header_spec.txt | 1 +
share/analysis-scripts/analysis.mk | 1 +
share/analysis-scripts/find_fun.py | 31 +++---------
share/analysis-scripts/function_finder.py | 59 +++++++++++++++++++++++
share/analysis-scripts/make_template.py | 44 ++++++++++++++---
share/analysis-scripts/template.mk | 6 ++-
tests/fc_script/oracle/GNUmakefile | 9 ++--
tests/fc_script/oracle/make_template.res | 16 +++---
10 files changed, 137 insertions(+), 43 deletions(-)
create mode 100644 share/analysis-scripts/function_finder.py
diff --git a/Makefile b/Makefile
index c39e2faff05..432c0e8363f 100644
--- a/Makefile
+++ b/Makefile
@@ -265,6 +265,7 @@ DISTRIB_FILES:=\
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
share/analysis-scripts/frama_c_results.py \
+ share/analysis-scripts/function_finder.py \
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/make_template.py \
@@ -1947,6 +1948,7 @@ install:: install-lib-$(OCAMLBEST)
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
share/analysis-scripts/frama_c_results.py \
+ share/analysis-scripts/function_finder.py \
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/make_template.py \
diff --git a/bin/frama-c-script b/bin/frama-c-script
index 1bea554e641..7922e89f720 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -125,6 +125,17 @@ make_path() {
if [ "$#" -gt 0 ]; then
dir="$1"
fi
+ if [ ! -d "$dir" ]; then
+ read -p "Directory '$dir' does not exist. Create it? [y/N] " yn
+ case $yn in
+ [Yy])
+ mkdir -p "$dir"
+ ;;
+ *)
+ echo "Exiting without creating."
+ exit 0;;
+ esac
+ fi
cat <<EOF > "${dir}/path.mk"
FRAMAC_DIR=${DIR}
ifeq (\$(wildcard \$(FRAMAC_DIR)),)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index ca66567d661..a201e0f32e7 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -122,6 +122,7 @@ share/analysis-scripts/cmd-dep.sh: .ignore
share/analysis-scripts/concat-csv.sh: .ignore
share/analysis-scripts/find_fun.py: .ignore
share/analysis-scripts/flamegraph.pl: CDDL
+share/analysis-scripts/function_finder.py: .ignore
share/analysis-scripts/git_utils.py: .ignore
share/analysis-scripts/list_files.py: .ignore
share/analysis-scripts/make_template.py: .ignore
diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk
index 442a2533434..fa832425b12 100644
--- a/share/analysis-scripts/analysis.mk
+++ b/share/analysis-scripts/analysis.mk
@@ -113,6 +113,7 @@ fc_list = $(subst $(space),$(comma),$(strip $1))
FRAMAC ?= frama-c
FRAMAC_SCRIPT = $(FRAMAC)-script
FRAMAC_GUI ?= frama-c-gui
+MACHDEP ?= x86_32
SLEVEL ?=
EVAFLAGS ?= \
-eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state \
diff --git a/share/analysis-scripts/find_fun.py b/share/analysis-scripts/find_fun.py
index 62692663c2d..5cb0b65863a 100755
--- a/share/analysis-scripts/find_fun.py
+++ b/share/analysis-scripts/find_fun.py
@@ -29,6 +29,7 @@ import sys
import os
import re
import glob
+import function_finder
MIN_PYTHON = (3, 5) # for glob(recursive)
if sys.version_info < MIN_PYTHON:
@@ -67,36 +68,16 @@ for d in dirs:
files += glob.glob(d + "/**/*.[ich]", recursive=True)
print("Looking for '%s' inside %d file(s)..." % (fname, len(files)))
-#print("\n".join(files))
-
-# To minimize the amount of false positives, we try to match the following:
-# - the line must begin with a C identifier (declarations and definitions in C
-# rarely start with spaces in the line), or with the function name itself
-# (supposing the return type is in the previous line)
-# - any number of identifiers are allowed (to allow for 'struct', 'volatile',
-# 'extern', etc)
-# - asterisks are allowed both before and after identifiers, except for the
-# first one (to allow for 'char *', 'struct **ptr', etc)
-# - identifiers are allowed after the parentheses, to allow for some macros/
-# modifiers
possible_declarators = []
possible_definers = []
-c_identifier = "[a-zA-Z_][a-zA-Z0-9_]*"
-c_id_maybe_pointer = c_identifier + "\**"
-type_prefix = c_id_maybe_pointer + "(?:\s+\**" + c_id_maybe_pointer + ")*\s+\**"
-parentheses_suffix = "\s*\([^)]*\)"
-re_fun = re.compile("^(?:" + type_prefix + "\s*)?" + fname + parentheses_suffix
- + "\s*(?:" + c_identifier + ")?\s*(;|{)", flags=re.MULTILINE)
+re_fun = function_finder.prepare(fname)
for f in files:
- with open(f, encoding="ascii", errors='ignore') as content_file:
- content = content_file.read()
- has_decl_or_def = re_fun.search(content)
- if has_decl_or_def is not None:
- is_decl = has_decl_or_def.group(1) == ";"
- if is_decl:
+ found = function_finder.find(re_fun, f)
+ if found:
+ if found == 1:
possible_declarators.append(f)
- else:
+ else:
possible_definers.append(f)
if possible_declarators == [] and possible_definers == []:
diff --git a/share/analysis-scripts/function_finder.py b/share/analysis-scripts/function_finder.py
new file mode 100644
index 00000000000..ee43f29adfb
--- /dev/null
+++ b/share/analysis-scripts/function_finder.py
@@ -0,0 +1,59 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Exports find_function_in_file, to be used by other scripts
+
+import re
+
+# To minimize the amount of false positives, we try to match the following:
+# - the line must begin with a C identifier (declarations and definitions in C
+# rarely start with spaces in the line), or with the function name itself
+# (supposing the return type is in the previous line)
+# - any number of identifiers are allowed (to allow for 'struct', 'volatile',
+# 'extern', etc)
+# - asterisks are allowed both before and after identifiers, except for the
+# first one (to allow for 'char *', 'struct **ptr', etc)
+# - identifiers are allowed after the parentheses, to allow for some macros/
+# modifiers
+
+# Precomputes the regex for 'fname'
+def prepare(fname):
+ c_identifier = "[a-zA-Z_][a-zA-Z0-9_]*"
+ c_id_maybe_pointer = c_identifier + "\**"
+ type_prefix = c_id_maybe_pointer + "(?:\s+\**" + c_id_maybe_pointer + ")*\s+\**"
+ parentheses_suffix = "\s*\([^)]*\)"
+ re_fun = re.compile("^(?:" + type_prefix + "\s*)?" + fname + parentheses_suffix
+ + "\s*(?:" + c_identifier + ")?\s*(;|{)", flags=re.MULTILINE)
+ return re_fun
+
+# Returns 0 if not found, 1 if declaration, 2 if definition
+def find(prepared_re, f):
+ with open(f, encoding="ascii", errors='ignore') as content_file:
+ content = content_file.read()
+ has_decl_or_def = prepared_re.search(content)
+ if has_decl_or_def is None:
+ return 0
+ else:
+ is_decl = has_decl_or_def.group(1) == ";"
+ return 1 if is_decl else 2
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
index c660b9b0135..0958a86035c 100755
--- a/share/analysis-scripts/make_template.py
+++ b/share/analysis-scripts/make_template.py
@@ -33,6 +33,7 @@ import shlex
import glob
from subprocess import Popen, PIPE
from pathlib import Path
+import function_finder
MIN_PYTHON = (3, 6) # for glob(recursive) and automatic Path conversions
if sys.version_info < MIN_PYTHON:
@@ -43,8 +44,10 @@ if len(sys.argv) > 2:
print(" creates a Frama-C makefile in [dir] (default: .frama-c)")
sys.exit(1)
-framac="frama-c"
-if not shutil.which(framac):
+framac_in_path = True
+framac = shutil.which("frama-c")
+if not framac:
+ framac_in_path = False
if os.environ.get("FRAMAC"):
framac = os.environ["FRAMAC"]
else:
@@ -112,11 +115,32 @@ main = input("Main target name: ")
if not re.match("^[a-zA-Z_0-9]+$", main):
sys.exit("error: invalid main target name (can only contain letters, digits, dash or underscore)")
+main_fun_finder_re = function_finder.prepare("main")
+
+# returns 0 if none, 1 if declaration, 2 if definition
+def defines_or_declares_main(f):
+ return function_finder.find(main_fun_finder_re, f)
+
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]
+ return sources
+
+def rel_prefix(f):
+ return f"{f}" if os.path.isabs(f) else f"{relprefix}/{f}"
+
+def sources_list_for_makefile(sources):
+ return "\n".join([f" {rel_prefix(source)} \\" for source in sources])
+
+def main_suffix(f):
+ main = defines_or_declares_main(f)
+ if main == 2:
+ return "\t# defines 'main'"
+ elif main == 1:
+ return "\t# declares 'main'"
+ else:
+ return ""
while True:
sources = input("Source files (default: **/*.c): ")
@@ -127,8 +151,11 @@ while True:
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("\n".join([" " + rel_prefix(source) + main_suffix(source) for source in source_list]))
print()
+ definitions_of_main = len([source for source in source_list if defines_or_declares_main(source)])
+ if definitions_of_main > 1:
+ print("warning: 'main' seems to be defined multiple times.")
yn = input("Is this ok? [Y/n] ")
if yn == "" or not (yn[0] == "N" or yn[0] == "n"):
break
@@ -137,7 +164,7 @@ json_compilation_database = None
if jcdb.is_file():
yn = input("compile_commands.json exists, add option -json-compilation-database? [Y/n] ")
if yn == "" or not (yn[0] == "N" or yn[0] == "n"):
- json_compilation_database = "."
+ json_compilation_database = f"{relprefix}/compile_commands.json"
else:
print("Option not added; you can later add it to FCFLAGS.")
@@ -213,7 +240,7 @@ with open(sharedir / "analysis-scripts" / "template.mk") as f:
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")
+ lines = replace_line(lines, "^ main.c \\\\", sources_list_for_makefile(source_list) + "\n")
if json_compilation_database:
lines = insert_line_after(lines, "^FCFLAGS", f" -json-compilation-database {json_compilation_database} \\\n")
if relprefix != "..":
@@ -223,6 +250,11 @@ gnumakefile.write_text("".join(lines))
print(f"Template created: {gnumakefile}")
+if not framac_in_path:
+ print(f"Frama-C not in path, adding path.mk to {dir}")
+ frama_c_script = bindir / "frama-c-script"
+ os.system(f"{frama_c_script} make-path {dir}")
+
if "PTESTS_TESTING" in os.environ:
print("Running ptests: cleaning up after tests...")
jcdb.unlink()
diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk
index 63cc973ba42..44f6271ce9c 100644
--- a/share/analysis-scripts/template.mk
+++ b/share/analysis-scripts/template.mk
@@ -12,10 +12,11 @@ include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
MACHDEP = x86_32
## Preprocessing flags (for -cpp-extra-args)
-CPPFLAGS +=
+CPPFLAGS += \
## General flags
FCFLAGS += \
+ -add-symbolic-path=.:.. \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
@@ -24,7 +25,8 @@ EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
## GUI-only flags
-FCGUIFLAGS +=
+FCGUIFLAGS += \
+ -add-symbolic-path=.:.. \
## Analysis targets (suffixed with .eva)
TARGETS = main.eva
diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile
index 36b3398ec2a..35feb31e056 100644
--- a/tests/fc_script/oracle/GNUmakefile
+++ b/tests/fc_script/oracle/GNUmakefile
@@ -12,13 +12,13 @@ include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
MACHDEP = x86_64
## Preprocessing flags (for -cpp-extra-args)
-CPPFLAGS +=
+CPPFLAGS += \
## General flags
FCFLAGS += \
- -machdep x86_64 \
- -json-compilation-database . \
+ -json-compilation-database ../compile_commands.json \
-main eva_main \
+ -add-symbolic-path=.:.. \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
@@ -27,7 +27,8 @@ EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
## GUI-only flags
-FCGUIFLAGS +=
+FCGUIFLAGS += \
+ -add-symbolic-path=.:.. \
## Analysis targets (suffixed with .eva)
TARGETS = fc_script_main.eva
diff --git a/tests/fc_script/oracle/make_template.res b/tests/fc_script/oracle/make_template.res
index 26616f9c038..8d4a89eefce 100644
--- a/tests/fc_script/oracle/make_template.res
+++ b/tests/fc_script/oracle/make_template.res
@@ -1,13 +1,17 @@
+Preparing template: result/GNUmakefile
Running ptests: setting up mock files...
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 \
+ ../for-find-fun.c
+ ../for-find-fun2.c
+ ../main.c # defines 'main'
+ ../main2.c
+ ../main3.c # defines 'main'
+warning: 'main' seems to be defined multiple times.
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]: warning: result/fc_stubs.c already exists. Overwrite? [y/N] Created stub for main function: result/fc_stubs.c
+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] Wrote to: result/path.mk
+Created stub for main function: result/fc_stubs.c
Template created: result/GNUmakefile
+Frama-C not in path, adding path.mk to result
Running ptests: cleaning up after tests...
--
GitLab