Commit 801d2ae6 authored by Andre Maroneze's avatar Andre Maroneze Committed by Valentin Perrelle
Browse files

[Analysis-scripts] improve template, make-template, make-path; refactor find-fun

parent a3117685
......@@ -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 \
......
......@@ -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)),)
......
......@@ -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
......
......@@ -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 \
......
......@@ -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 == []:
......
#!/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
......@@ -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()
......
......@@ -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
......
......@@ -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
......
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...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment