Skip to content
Snippets Groups Projects
Commit 8e7c6370 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[analysis-scripts] improve and distribute estimate-difficulty executable

Allow estimate-difficulty to be exported (in Linux/macOS/Windows) as
independent executable, so that it can be used without having to install
Frama-C.
parent 6988ab5c
No related branches found
No related tags found
No related merge requests found
Showing
with 579 additions and 136 deletions
......@@ -189,6 +189,15 @@ Makefile.plugin.generated
# WP/Coq Generated file
.lia.cache
# analysis-scripts
share/analysis-scripts/build
share/analysis-scripts/fced-dist
share/analysis-scripts/fced-dist-prepare*
share/analysis-scripts/fc-estimate-difficulty.*spec
share/analysis-scripts/fc-estimate-difficulty
share/analysis-scripts/fc-estimate-difficulty.exe
share/analysis-scripts/libc_metrics.json
# generated ML files
/src/libraries/utils/json.ml
......
......@@ -265,7 +265,9 @@ DISTRIB_FILES:=\
share/analysis-scripts/detect_recursion.py \
share/analysis-scripts/epilogue.mk \
share/analysis-scripts/estimate_difficulty.py \
share/analysis-scripts/external_tool.py \
share/analysis-scripts/fc_stubs.c \
share/analysis-scripts/fclog.py \
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
share/analysis-scripts/frama_c_results.py \
......@@ -1982,7 +1984,9 @@ install:: install-lib-$(OCAMLBEST)
share/analysis-scripts/clone.sh \
share/analysis-scripts/creduce.sh \
share/analysis-scripts/epilogue.mk \
share/analysis-scripts/external_tool.py \
share/analysis-scripts/fc_stubs.c \
share/analysis-scripts/fclog.py \
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
share/analysis-scripts/frama_c_results.py \
......
......@@ -123,7 +123,9 @@ share/analysis-scripts/creduce.sh: CEA_LGPL
share/analysis-scripts/detect_recursion.py: CEA_LGPL
share/analysis-scripts/epilogue.mk: CEA_LGPL
share/analysis-scripts/estimate_difficulty.py: CEA_LGPL
share/analysis-scripts/external_tool.py: CEA_LGPL
share/analysis-scripts/fc_stubs.c: .ignore
share/analysis-scripts/fclog.py: CEA_LGPL
share/analysis-scripts/frama_c_results.py: CEA_LGPL
share/analysis-scripts/cmd-dep.sh: .ignore
share/analysis-scripts/concat-csv.sh: .ignore
......
......@@ -192,7 +192,13 @@ def make_target_name(target):
# sources are pretty-printed relatively to the .frama-c directory, where the
# GNUmakefile will reside
def rel_prefix(path):
return path if os.path.isabs(path) else os.path.relpath(path, start=dot_framac_dir)
"""Return a relative path to the .frama-c directory if path is relative, or if the relativized
path will contain at most a single '..'. Otherwise, return an absolute path."""
rel = os.path.relpath(path, start=dot_framac_dir)
if rel.startswith("../.."):
return os.path.abspath(path)
else:
return rel
def pretty_sources(sources):
......@@ -255,7 +261,7 @@ def list_partition(f, l):
l1 = []
l2 = []
for e in l:
if f(l):
if f(e):
l1.append(e)
else:
l2.append(e)
......
......@@ -26,18 +26,22 @@
of analyzing a new code base with Frama-C."""
import argparse
import glob
import json
import logging
import os
from pathlib import Path
import re
import subprocess
import sys
import tempfile
import build_callgraph
import external_tool
import fclog
import source_filter
# TODO : avoid relativizing paths when introducing too many ".." ;
# TODO : accept directory as argument (--full-tree), and then do glob **/*.{c,i} inside
# TODO : try to check the presence of compiler builtins
# TODO : try to check for pragmas
# TODO : detect absence of 'main' function (library)
......@@ -47,23 +51,66 @@ parser = argparse.ArgumentParser(
Estimates the difficulty of analyzing a given code base"""
)
parser.add_argument(
"--header-dirs",
"-d",
metavar="DIR",
"paths",
nargs="+",
help="directories containing headers (default: .frama-c)",
help="source files and directories. \
If a directory <dir> is specified, it is recursively explored, as if '<dir>/**/*.[ci]' \
had been specified.",
type=Path,
)
parser.add_argument("files", nargs="+", help="source files")
args = vars(parser.parse_args())
header_dirs = args["header_dirs"]
if not header_dirs:
header_dirs = []
files = args["files"]
parser.add_argument(
"--debug",
metavar="FILE",
help="enable debug mode and redirect output to the specified file",
)
parser.add_argument(
"--verbose",
action="store_true",
help="enable verbose output; if --debug is set, output is redirected to the same file.",
)
parser.add_argument(
"--no-cloc",
action="store_true",
help="disable usage of external tool 'cloc', even if available.",
)
args = parser.parse_args()
paths = args.paths
debug = args.debug
no_cloc = args.no_cloc
verbose = args.verbose
under_test = os.getenv("PTESTS_TESTING")
# gather information from several sources
fclog.init(debug, verbose)
### Auxiliary functions #######################################################
def get_dir(path):
"""Similar to dirname, but returns the path itself if it refers to a directory"""
if path.is_dir():
return path
else:
return path.parent
def collect_files_and_local_dirs(paths):
"""Returns the list of directories (and their subdirectories) containing
the specified paths. Note that this also includes subdirectories which do not
themselves contain any .c files, but which may contain .h files."""
dirs = set()
files = set()
for p in paths:
if p.is_dir():
files = files.union(glob.glob(f"{p}/**/*.[chi]", recursive=True))
dirs.add(p)
else:
files.add(p)
dirs.add(p.parent)
local_dirs = {s[0] for d in dirs for s in os.walk(d)}
if not files:
sys.exit("error: no source files (.c/.i) found in provided paths: " + " ".join(paths))
return files, local_dirs
def extract_keys(l):
......@@ -73,8 +120,7 @@ def extract_keys(l):
def get_framac_libc_function_statuses(framac, framac_share):
if framac:
(_handler, metrics_tmpfile) = tempfile.mkstemp(prefix="fc_script_est_diff", suffix=".json")
if debug:
print("metrics_tmpfile: %s", metrics_tmpfile)
logging.debug("metrics_tmpfile: %s", metrics_tmpfile)
fc_runtime = framac_share / "libc" / "__fc_runtime.c"
fc_libc_headers = framac_share / "libc" / "__fc_libc.h"
subprocess.run(
......@@ -104,10 +150,8 @@ def get_framac_libc_function_statuses(framac, framac_share):
return (defined, spec_only)
re_include = re.compile(r'\s*#\s*include\s*("|<)([^">]+)("|>)')
def grep_includes_in_file(filename):
re_include = re.compile(r'\s*#\s*include\s*("|<)([^">]+)("|>)')
file_content = source_filter.open_and_filter(filename, not under_test)
i = 0
for line in file_content.splitlines():
......@@ -136,13 +180,59 @@ def get_includes(files):
return chevron_includes, quote_includes
def is_local_header(local_dirs, header):
for d in local_dirs:
path = Path(d)
if Path(path / header).exists():
return True
return False
def grep_keywords(keywords, filename):
with open(filename, "r") as f:
found = {}
for line in f:
if any(x in line for x in keywords):
# found one or more keywords; count them
for kw in keywords:
if kw in line:
if kw in found:
found[kw] += 1
else:
found[kw] = 1
return found
def pretty_keyword_count(found):
res = ""
for kw, count in sorted(found.items()):
if res:
res += ", "
res += f" {kw} ({count} line{'s' if count > 1 else ''})"
return res
### End of auxiliary functions ################################################
debug = os.getenv("DEBUG")
verbose = False
files, local_dirs = collect_files_and_local_dirs(paths)
score = {
"recursion": 0,
"libc": 0,
"includes": 0,
"malloc": 0,
"keywords": 0,
"asm": 0,
}
framac_bin = os.getenv("FRAMAC_BIN")
if not framac_bin:
print(
"Running script in no-Frama-C mode (set FRAMAC_BIN to the directory containing frama-c if you want to use it)."
logging.info(
"Running script in no-Frama-C mode (set FRAMAC_BIN to the directory"
+ " containing frama-c if you want to use it)."
)
framac = None
script_dir = os.path.dirname(os.path.realpath(__file__))
......@@ -153,10 +243,27 @@ else:
subprocess.check_output([framac, "-no-autoload-plugins", "-print-share-path"]).decode()
)
print("Building callgraph...")
if not no_cloc:
cloc = external_tool.get_command("cloc", "CLOC")
if cloc:
data = external_tool.run_and_check(
[cloc, "--hide-rate", "--progress-rate=0", "--csv"] + list(files), ""
)
data = data.splitlines()
[nfiles, _sum, nblank, ncomment, ncode] = data[-1].split(",")
nlines = int(nblank) + int(ncomment) + int(ncode)
logging.info(
"Processing %d file(s), approx. %d lines of code (out of %d lines)",
int(nfiles),
int(ncode),
nlines,
)
logging.info("Building callgraph...")
cg = build_callgraph.compute(files)
print("Computing data about libc/POSIX functions...")
logging.info("Computing data about libc/POSIX functions...")
libc_defined_functions, libc_specified_functions = get_framac_libc_function_statuses(
framac, framac_share
)
......@@ -185,16 +292,23 @@ for (cycle_start_loc, cycle) in recursive_cycles:
continue
reported_recursive_pairs.add(cycle[-1])
(filename, line) = cycle_start_loc
(x, y) = cycle[0]
pretty_cycle = f"{x} -> {y}"
for (x, y) in cycle[1:]:
pretty_cycle += f" -> {y}"
print(f"[recursion] found recursive cycle near {filename}:{line}: {pretty_cycle}")
def pretty_cycle(cycle):
(x, y) = cycle[0]
res = f"{x} -> {y}"
for (x, y) in cycle[1:]:
res += f" -> {y}"
return res
logging.info(
"[recursion] found recursive cycle near %s:%d: %s", filename, line, pretty_cycle(cycle)
)
score["recursion"] += 1
callees = [callee for (_, callee) in list(cg.edges.keys())]
callees = set(callees)
used_headers = set()
print(f"Estimating difficulty for {len(callees)} function calls...")
logging.info("Estimating difficulty for %d function calls...", len(callees))
warnings = 0
for callee in sorted(callees):
......@@ -203,8 +317,10 @@ for callee in sorted(callees):
global warnings
if status == "warning":
warnings += 1
if verbose or debug or status == "warning":
print(f"- {status}: {callee} ({standard}) {reason}")
if status == "warning":
logging.warning("%s (%s) %s", callee, standard, reason)
else:
logging.log(fclog.VERBOSE, "%s: %s (%s) %s", status, callee, standard, reason)
try:
is_problematic = posix_identifiers[callee]["notes"]["fc-support"] == "problematic"
......@@ -258,55 +374,56 @@ for callee in sorted(callees):
if not status_emitted:
callee_status("warning", standard, "has neither code nor spec in Frama-C's libc")
print(f"Function-related warnings: {warnings}")
logging.info("Function-related warnings: %d", warnings)
score["libc"] = warnings
if (verbose or debug) and used_headers:
print("used headers:")
for header in sorted(used_headers):
print(f" <{header}>")
logging.log(
fclog.VERBOSE,
"Used POSIX headers:\n%s",
"\n".join([f" <{header}>" for header in sorted(used_headers)]),
)
(chevron_includes, quote_includes) = get_includes(files)
def is_local_header(header_dirs, header):
for d in header_dirs:
path = Path(d)
if Path(path / header).exists():
return True
return False
print(f"Estimating difficulty for {len(chevron_includes)} '#include <header>' directives...")
logging.info(
"Estimating difficulty for %d '#include <header>' directives...", len(chevron_includes)
)
non_posix_headers = []
header_warnings = 0
for header in sorted(chevron_includes, key=str.casefold):
if not header.lower().endswith(".h"):
continue # ignore included non-header files
if header in posix_headers:
fc_support = posix_headers[header]["fc-support"]
if fc_support == "unsupported":
header_warnings += 1
print(f"- WARNING: included header <{header}> is explicitly unsupported by Frama-C")
logging.warning("included header <%s> is explicitly unsupported by Frama-C", header)
else:
if verbose or debug:
c11_or_posix = "C11" if header in c11_headers else "POSIX"
print(f"- note: included {c11_or_posix} header ")
logging.log(
fclog.VERBOSE,
"included %s header %s",
"C11" if header in c11_headers else "POSIX",
header,
)
else:
if is_local_header(header_dirs, header):
if verbose or debug:
print(f"- ok: included header <{header}> seems to be available locally")
if is_local_header(local_dirs, header):
logging.log(
fclog.VERBOSE, "ok: included header <%s> seems to be available locally", header
)
else:
non_posix_headers.append(header)
header_warnings += 1
print(f"- warning: included non-POSIX header <{header}>")
print(f"Header-related warnings: {header_warnings}")
logging.warning("included non-POSIX header <%s>", header)
logging.info("Header-related warnings: %d", header_warnings)
score["includes"] = header_warnings
# dynamic allocation
dynalloc_functions = set(["malloc", "calloc", "free", "realloc", "alloca", "mmap"])
dyncallees = dynalloc_functions.intersection(callees)
if dyncallees:
print(f"- note: calls to dynamic allocation functions: {', '.join(sorted(dyncallees))}")
logging.info("Calls to dynamic allocation functions: %s", ", ".join(sorted(dyncallees)))
score["malloc"] = len(dyncallees)
# unsupported C11-specific features
......@@ -320,21 +437,21 @@ c11_unsupported = [
"alignof", # stdalign.h may use these symbols
]
for keyword in c11_unsupported:
out = subprocess.Popen(
["grep", "-n", "\\b" + keyword + "\\b"] + files + ["/dev/null"],
stdout=subprocess.PIPE,
stderr=subprocess.STDOUT,
)
lines = out.communicate()[0].decode("utf-8").splitlines()
if lines:
n = len(lines)
print(
f"- warning: found {n} line{'s' if n > 1 else ''} with occurrences of "
f"unsupported C11 construct '{keyword}'"
)
logging.info("Checking presence of unsupported C11 features...")
for f in files:
found = grep_keywords(c11_unsupported, f)
if found:
logging.warning("unsupported keyword(s) in %s:%s", f, pretty_keyword_count(found))
score["keywords"] += len(found)
# assembly code
if "asm" in callees or "__asm" in callees or "__asm__" in callees:
print("- warning: code seems to contain inline assembly ('asm(...)')")
logging.warning("code seems to contain inline assembly ('asm(...)')")
score["asm"] = 1
logging.info(
"Overall difficulty score:\n%s",
"\n".join([k + ": " + str(v) for (k, v) in sorted(score.items())]),
)
# -*- coding: utf-8 -*-
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
"""This file provides utility functions to use external tools, either
available in the PATH or via PyInstaller."""
import os
from pathlib import Path
import shutil
import subprocess
import sys
# warnings about missing commands are disabled during testing
emit_warns = os.getenv("PTESTS_TESTING") is None
# Cache for get_command
cached_commands = {}
def resource_path(relative_path):
"""Get absolute path to resource; only used by the pyinstaller standalone distribution"""
base_path = getattr(sys, "_MEIPASS", os.path.dirname(os.path.abspath(__file__)))
return os.path.join(base_path, relative_path)
def get_command(command, env_var_name):
"""Returns a Path to the command; priority goes to the environment variable,
then in the PATH, then in the resource directory (for a pyinstaller binary)."""
if command in cached_commands:
return cached_commands[command]
p = os.getenv(env_var_name)
if p:
p = Path(p)
else:
p = shutil.which(command)
if p:
p = Path(p)
else:
p = Path(resource_path(command))
if not p.exists():
if emit_warns:
print(
f"info: optional external command '{command}' not found in PATH;",
f"consider installing it or setting environment variable {env_var_name}",
)
p = None
cached_commands[command] = p
return p
def run_and_check(command_and_args, input_data):
try:
return subprocess.check_output(
command_and_args,
input=input_data,
stderr=None,
encoding="ascii",
errors="ignore",
)
except subprocess.CalledProcessError as e:
sys.exit(f"error running command: {command_and_args}\n{e}")
# Produces a self-contained binary for 'frama-c-script estimate-difficulty'
# on a machine without Frama-C.
# Works on Linux and macOS. The Windows binary is compiled and tested using
# a Docker image with wine and pyinstaller (usage of Docker avoids issues with
# staging versions in e.g. Fedora, which may cause weird error messages when
# running in Windows). The Linux binary is tested on a bare-bones Alpine Linux,
# to ensure it does not depend on dynamic libraries.
# The macOS version needs to be tested by hand.
help:
@echo "targets:"
@echo "fc-estimate-difficulty : Linux/macOS version (depending on host system)"
@echo "fc-estimate-difficulty.exe : Windows cross-compiled version (from Linux)"
@echo "clean : Erase working directory"
@echo "test-fc-estimate-difficulty : Test Linux/macOS version"
@echo "test-fc-estimate-difficulty.exe : Test Windows version"
os := $(shell uname -s)
workdir = fced-dist-prepare
distdir = fced-dist
libc_metrics.json: ../libc/__fc_libc.h ../libc/__fc_runtime.c
ifeq ($(wildcard $(FRAMAC)),)
$(error FRAMAC must be set to the path of the 'frama-c' binary)
endif
FRAMAC_SHARE="$(shell $(FRAMAC) -no-autoload-plugins -print-share-path)"
rm -f $@
$(FRAMAC) \
$^ \
-no-autoload-plugins -load-module metrics \
-metrics -metrics-libc -metrics-output $@
chmod -w $@ # generated file: prevent accidental overwriting
PY_DEPS := \
build_callgraph.py \
estimate_difficulty.py \
external_tool.py \
fclog.py \
function_finder.py \
source_filter.py \
COMPLIANCE := $(wildcard ../compliance/*.json)
TOOLS := $(workdir)/scc $(workdir)/astyle
COMMON_DEPS := $(PY_DEPS) $(COMPLIANCE) libc_metrics.json
fc-estimate-difficulty: EXE=
fc-estimate-difficulty.exe: EXE=".exe"
fc-estimate-difficulty: WINE=
fc-estimate-difficulty.exe: WINE="/home/andr/git/wine/wine"
fc-estimate-difficulty: PSEP=:
fc-estimate-difficulty.exe: PSEP=;
fc-estimate-difficulty: $(COMMON_DEPS) $(TOOLS)
fc-estimate-difficulty.exe: \
$(COMMON_DEPS) $(addsuffix .exe,$(TOOLS)) fced-win.Dockerfile
fc-estimate-difficulty:
pyinstaller estimate_difficulty.py \
-F \
-n $@ \
--distpath $(distdir) \
--noconfirm \
--add-data "libc_metrics.json:share" \
--add-data "../compliance/*.json:share/compliance" \
--add-binary "$(workdir)/scc:." \
--add-binary "$(workdir)/astyle:."
ifeq ($(os),Linux)
@echo "Linux: running staticx"
staticx "$(distdir)/$@" $@
else
@echo "NOT running staticx (macOS?)"
mv "$(distdir)/$@" $@
endif
fc-estimate-difficulty.exe:
mkdir -p $(workdir)/compliance
cp ../compliance/*.json $(workdir)/compliance
docker build . -f fced-win.Dockerfile -t fced-win
docker cp $$(docker create --rm fced-win):/fced/$@ $@
$(workdir)/scc: $(workdir)/scc-snapshots-fc-1.1.0
make -C $< clean
make -C $< scc $(if $(findstring Linux,$(os)),CFLAGS="-static") -j
cp $(workdir)/scc-snapshots-fc-1.1.0/scc $@
$(workdir)/scc.exe: $(workdir)/scc-snapshots-fc-1.1.0
make -C $< clean
make -C $< scc CC=x86_64-w64-mingw32-gcc -j
cp $(workdir)/scc-snapshots-fc-1.1.0/scc.exe $@
$(workdir)/scc-snapshots-fc-1.1.0:
mkdir -p $(workdir)
wget 'https://github.com/Frama-C/scc-snapshots/archive/refs/tags/fc-1.1.0.tar.gz' -O $(workdir)/fc-1.1.0.tar.gz
cd $(workdir) && tar xvf fc-1.1.0.tar.gz
touch $@
$(workdir)/astyle: $(workdir)/astyle_3.1
make -C $(workdir)/astyle_3.1/build/gcc clean
make -C $(workdir)/astyle_3.1/build/gcc \
$(if $(findstring Linux,$(os)),LDFLAGS="-static" CFLAGS="-static -static-libgcc -static-libstdc++") -j
cp $(workdir)/astyle_3.1/build/gcc/bin/astyle $@
$(workdir)/astyle.exe: $(workdir)/astyle_3.1
make -C $(workdir)/astyle_3.1/build/gcc clean
make -C $(workdir)/astyle_3.1/build/gcc LDFLAGS="-static" CFLAGS="-static -static-libgcc -static-libstdc++" CXX=x86_64-w64-mingw32-g++ -j
cp $(workdir)/astyle_3.1/build/gcc/bin/astyle.exe $@
$(workdir)/astyle_3.1:
mkdir -p $(workdir)
wget 'https://downloads.sourceforge.net/project/astyle/astyle/astyle%203.1/astyle_3.1_linux.tar.gz' -O $(workdir)/astyle_3.1_linux.tar.gz
cd $(workdir) && tar xvf astyle_3.1_linux.tar.gz
rm -rf $(workdir)/astyle_3.1
mv $(workdir)/astyle $(workdir)/astyle_3.1
sed -i.bak 's/^CXX = g++/CXX ?= g++/' $(workdir)/astyle_3.1/build/gcc/Makefile
sed -i.bak 's/^CXX = g++/CXX ?= g++/' $(workdir)/astyle_3.1/build/gcc/Makefile
touch $@
clean:
rm -rf $(workdir) $(distdir) fc-estimate-difficulty.spec fc-estimate-difficulty.exe.spec
distclean: clean
rm -f fc-estimate-difficulty fc-estimate-difficulty.exe libc_metrics.json
test-fc-estimate-difficulty: fc-estimate-difficulty
ifeq ($(os),Linux)
docker build . -f fced-lin.Dockerfile -t fced-lin
else
./$< fced-test | \
grep -A9 "Overall difficulty score" | \
grep -v 0 | \
grep -q ': '
endif
@echo "Done testing $^."
test-fc-estimate-difficulty.exe: fc-estimate-difficulty.exe
@file $< | grep -q "MS Windows"
@echo "Done testing $< (actual testing done inside Docker image)"
.PHONY: clean distclean test-fc-estimate-difficulty test-fc-estimate-difficulty.exe
FROM alpine:3.15
COPY fc-estimate-difficulty /
RUN mkdir /fced-test
COPY fced-test fced-test/
RUN ./fc-estimate-difficulty fced-test | \
grep -A9 "Overall difficulty score" | \
grep -v 0 | \
grep -q ': '
#include <stdlib.h>
#include <X>
volatile int v;
int main() {
asm("mov ax, ax");
if (v) return main();
malloc(42);
return 0;
}
#include <a.h>
FROM tobix/pywine:3.10
RUN mkdir /fced
COPY *.py /fced/
RUN mkdir /fced/dist-prepare
COPY fced-dist-prepare /fced/dist-prepare/
COPY fced-test /fced/fced-test/
COPY libc_metrics.json /fced/
WORKDIR /fced
RUN wine pyinstaller estimate_difficulty.py \
-F \
-n fc-estimate-difficulty.exe \
--distpath . \
--noconfirm \
--add-data "libc_metrics.json;share" \
--add-data "dist-prepare/compliance/*.json;share/compliance" \
--add-binary "dist-prepare/scc.exe;." \
--add-binary "dist-prepare/astyle.exe;."
RUN wine fc-estimate-difficulty.exe fced-test | \
grep -A9 "Overall difficulty score" | \
grep -v 0 | \
grep -q ': '
# -*- coding: utf-8 -*-
##########################################################################
# #
# This file is part of Frama-C. #
# #
# Copyright (C) 2007-2022 #
# 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). #
# #
##########################################################################
"""Contains functions to perform logging-related configuration common to
several scripts."""
import logging
import sys
# extra log level used in messages
VERBOSE = 15
def init(debug, verbose):
"""Initializes the logging mechanism. 'debug' is the filename to redirect to
(or special values 'stdout'/'stderr'). If None, disable debug.
If 'verbose' is true, output VERBOSE messages. If both are set, the level
is 'debug'."""
logging.addLevelName(VERBOSE, "")
logging.addLevelName(logging.ERROR, "ERROR: ")
logging.addLevelName(logging.WARN, "WARNING: ")
logging.addLevelName(logging.INFO, "")
log_level = logging.DEBUG if debug else VERBOSE if verbose else logging.INFO
log_format = "%(levelname)s%(message)s"
# special values for debug filename
if debug == "stdout" or not debug:
logging.basicConfig(stream=sys.stdout, level=log_level, format=log_format)
# This very ugly hack seems necessary to avoid BrokenPipeErrors when the
# output of the calling script is truncated (via head, grep -q, etc).
# Note that, on Windows, there is an OSError with "22 Invalid argument"
# instead of a BrokenPipeError.
original_flush = sys.stdout.flush
def new_flush():
try:
original_flush()
except BrokenPipeError:
sys.stdout = None
sys.exit(0)
except OSError as e:
if sys.platform == "win32" and e.errno == 22:
sys.stdout = None
sys.exit(0)
raise e
sys.stdout.flush = new_flush
elif debug == "stderr":
logging.basicConfig(stream=sys.stderr, level=log_level, format=log_format)
else:
logging.basicConfig(
filename=debug,
level=log_level,
filemode="w",
format=log_format,
)
......@@ -37,75 +37,24 @@ the efficiency of regex-based heuristics."""
# of errors when running the filters. Note that an absent tool
# does _not_ lead to an error.
import os
from pathlib import Path
import shutil
import subprocess
import external_tool
import sys
# warnings about missing commands are disabled during testing
emit_warns = os.getenv("PTESTS_TESTING") is None
# Cache for get_command
cached_commands = {}
def resource_path(relative_path):
"""Get absolute path to resource; only used by the pyinstaller standalone distribution"""
base_path = getattr(sys, "_MEIPASS", os.path.dirname(os.path.abspath(__file__)))
return os.path.join(base_path, relative_path)
def get_command(command, env_var_name):
"""Returns a Path to the command; priority goes to the environment variable,
then in the PATH, then in the resource directory (for a pyinstaller binary)."""
if command in cached_commands:
return cached_commands[command]
p = os.getenv(env_var_name)
if p:
p = Path(p)
else:
p = shutil.which(command)
if p:
p = Path(p)
else:
p = Path(resource_path(command))
if not p.exists():
if emit_warns:
print(
f"info: optional external command '{command}' not found in PATH; "
f"consider installing it or setting environment variable {env_var_name}"
)
p = None
cached_commands[command] = p
return p
def run_and_check(command_and_args, input_data):
try:
return subprocess.check_output(
command_and_args,
input=input_data,
stderr=None,
encoding="ascii",
errors="ignore",
)
except subprocess.CalledProcessError as e:
sys.exit(f"error running command: {command_and_args}\n{e}")
def filter_with_scc(input_data):
scc = get_command("scc", "SCC")
scc_bin = "scc" if sys.platform != "win32" else "scc.exe"
scc = external_tool.get_command(scc_bin, "SCC")
if scc:
return run_and_check([scc, "-k"], input_data)
return external_tool.run_and_check([scc, "-k", "-b"], input_data)
else:
return input_data
def filter_with_astyle(input_data):
astyle = get_command("astyle", "ASTYLE")
astyle_bin = "astyle" if sys.platform != "win32" else "astyle.exe"
astyle = external_tool.get_command(astyle_bin, "ASTYLE")
if astyle:
return run_and_check(
return external_tool.run_and_check(
[astyle, "--keep-one-line-blocks", "--keep-one-line-statements"], input_data
)
else:
......
/* run.config
NOFRAMAC: testing frama-c-script, not frama-c itself
EXECNOW: LOG @PTEST_NAME@.res LOG @PTEST_NAME@.err PTESTS_TESTING=1 %{bin:frama-c-script} estimate-difficulty @PTEST_FILE@ > @PTEST_NAME@.res 2> @PTEST_NAME@.err
EXECNOW: LOG @PTEST_NAME@.res LOG @PTEST_NAME@.err PTESTS_TESTING=1 %{bin:frama-c-script} estimate-difficulty --no-cloc @PTEST_FILE@ > @PTEST_NAME@.res 2> @PTEST_NAME@.err
*/
// these includes are not actually used by the compiler
......@@ -25,4 +25,8 @@ int main() {
strlen(); // no warning
ccosl(); // warning: neither code nor spec
dprintf(); // no warning: neither code nor spec, but handled by Variadic
__asm__("xor ax, ax");
malloc(2);
alignof(char*);
_Complex cc;
}
Building callgraph...
Computing data about libc/POSIX functions...
[recursion] found recursive cycle near estimate_difficulty.i:18: f -> f
Estimating difficulty for 7 function calls...
- warning: ccosl (POSIX) has neither code nor spec in Frama-C's libc
- warning: setjmp (POSIX) is known to be problematic for code analysis
Estimating difficulty for 10 function calls...
WARNING: ccosl (POSIX) has neither code nor spec in Frama-C's libc
WARNING: setjmp (POSIX) is known to be problematic for code analysis
Function-related warnings: 2
Estimating difficulty for 3 '#include <header>' directives...
- WARNING: included header <complex.h> is explicitly unsupported by Frama-C
WARNING: included header <complex.h> is explicitly unsupported by Frama-C
Header-related warnings: 1
Calls to dynamic allocation functions: malloc
Checking presence of unsupported C11 features...
WARNING: unsupported keyword(s) in estimate_difficulty.i: _Complex (1 line), alignof (1 line)
WARNING: code seems to contain inline assembly ('asm(...)')
Overall difficulty score:
asm: 1
includes: 1
keywords: 2
libc: 2
malloc: 1
recursion: 1
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment