Merge branch 'feature/andre/frama-c-script-configure' into 'master'

Feature/andre/frama c script configure

See merge request frama-c/frama-c!2116

Makefile

@@ -262,6 +262,7 @@ DISTRIB_FILES:=\
       share/analysis-scripts/frama_c_results.py                         \
       share/analysis-scripts/git_utils.py                               \
       share/analysis-scripts/list_files.py                              \
+      share/analysis-scripts/make_wrapper.py                            \
       share/analysis-scripts/parse-coverage.sh                          \
       share/analysis-scripts/README.md                                  \
       share/analysis-scripts/results_display.py                         \
@@ -1915,6 +1916,7 @@ install:: install-lib
 	  share/analysis-scripts/frama_c_results.py \
 	  share/analysis-scripts/git_utils.py \
 	  share/analysis-scripts/list_files.py \
+	  share/analysis-scripts/make_wrapper.py \
 	  share/analysis-scripts/parse-coverage.sh \
 	  share/analysis-scripts/README.md \
 	  share/analysis-scripts/results_display.py \

bin/frama-c-script

@@ -59,6 +59,21 @@ if [ $# -lt 1 ]; then
    echo "      Monitors and summarizes multiple analyses dispatched by a Makefile"
    echo "      in the current PWD."
    echo "      Use $0 summary --help for more informations."
+   echo ""
+   echo "  - configure <machdep>"
+   echo "      Runs an existing configure script to only consider files"
+   echo "      in Frama-C's libc; this will hopefully disable non-essential"
+   echo "      and non-POSIX external libraries."
+   echo "      <machdep> is necessary to define a required preprocessor symbol"
+   echo "      (run 'frama-c -machdep' help to get the list of machdeps)."
+   echo ""
+   echo "  - make-wrapper <target> <args>"
+   echo "      Runs 'make <target> <args>', parsing the output to suggest"
+   echo "      useful commands in case of failure."
+   echo ""
+   echo "  - normalize-jcdb [path/to/compile_commands.json]"
+   echo "      Applies some transformations to an existing compile_commands.json"
+   echo "      (such as relativizing paths) to improve portability"
    exit
 fi
 
@@ -105,6 +120,7 @@ make_template() {
         dir="."
     fi
     path="$dir/GNUmakefile"
+    path_tmp="${path}.tmp"
     check_path_exists "$path"
     read -p "Main target name: " main
     if [[ ! ( "$main" =~ ^[a-zA-Z_0-9]+$ ) ]]; then
@@ -115,9 +131,41 @@ make_template() {
     if [ "$sources" = "" ]; then
         sources="*.c"
     fi
-    sed "s/^MAIN_TARGET :=/MAIN_TARGET := ${main}/" "${FRAMAC_SHARE}/analysis-scripts/template.mk" > "${path}.tmp"
-    sed "s|\$(MAIN_TARGET).parse:|\$(MAIN_TARGET).parse: $sources|" "${path}.tmp" | sed "/# Remove these lines after defining the main target/{N;N;N;N;d;}" > "$path"
-    rm "${path}.tmp"
+
+    add_main_stub=0
+    read -p "Add stub for function main (only needed if it uses command-line arguments)? [y/N] " yn
+    case $yn in
+        [Yy])
+            add_main_stub=1
+            sources="fc_stubs.c $sources"
+            ;;
+        *)
+            ;;
+    esac
+
+    sed "s/^MAIN_TARGET :=/MAIN_TARGET := ${main}/" "${FRAMAC_SHARE}/analysis-scripts/template.mk" > "$path"
+    sed "s|\$(MAIN_TARGET).parse:|\$(MAIN_TARGET).parse: $sources|" "$path" | sed "/# Remove these lines after defining the main target/{N;N;N;N;d;}" > "$path_tmp"; mv "$path_tmp" "$path"
+    if [ -e "compile_commands.json" ]; then
+        read -p "compile_commands.json exists, add option -json-compilation-database? [Y/n] " yn
+        case $yn in
+            [Nn])
+                echo "Option not added; you can later add it to FCFLAGS."
+                ;;
+            *)
+                # the command below inserts a line after matching a given
+                # pattern; compatible with macOS sed
+                sed -e '/^FCFLAGS[[:space:]]\++=/a\
+\ \ -json-compilation-database .\\' "$path" > "$path_tmp"; mv "$path_tmp" "$path"
+                ;;
+        esac
+    fi
+    if [ $add_main_stub -eq 1 ]; then
+        check_path_exists "fc_stubs.c"
+        cp "${FRAMAC_SHARE}/analysis-scripts/fc_stubs.c" "./"
+        echo "Created stub for main function: fc_stubs.c"
+        sed -e '/^FCFLAGS[[:space:]]\++=/a\
+\ \ -main eva_main \\' "$path" > "$path_tmp"; mv "$path_tmp" "$path"
+    fi
     echo "Template created: $path"
 }
 
@@ -185,6 +233,48 @@ EOF
     fi
 }
 
+configure_for_frama_c() {
+    if [ "$#" -eq 0 ]; then
+        echo "error: 'configure' command requires a machdep";
+        exit 1
+    fi
+    MACHDEP="$(echo $1 | tr a-z A-Z)"
+    shift
+    CPP="gcc -E -nostdinc -fno-builtin -I${FRAMAC_SHARE}/libc -D__FC_MACHDEP_${MACHDEP}" ./configure "$@"
+}
+
+normalize_jcdb() {
+    path=""
+    if [ "$#" -eq 0 ]; then
+        path="./compile_commands.json"
+    else
+        path="$1"
+    fi
+    if [ ! -e "$path" ]; then
+        echo "error: cannot find file: $path";
+        exit 1
+    fi
+    sed "s|$PWD/||g" "$path" > "${path}.tmp"
+    cmp -s "$path" "${path}.tmp"
+    if [ $? -eq 0 ]; then
+        echo "No changes to be applied to $path"
+        rm "${path}.tmp"
+    else
+        echo "Differences to be applied to $path:"
+        diff -u0 "$path" "${path}.tmp"
+        read -p "Normalize $path? [y/N] " yn
+        case $yn in
+            [Yy])
+                mv "${path}.tmp" "$path"
+                echo "Normalization applied to $path"
+            ;;
+            *)
+                echo "Exiting without overwriting."
+                exit 0;;
+        esac
+    fi
+}
+
 case "$command" in
     "make-template")
         shift;
@@ -210,6 +300,18 @@ case "$command" in
         shift;
         ${FRAMAC_SHARE}/analysis-scripts/summary.py "$@";
         ;;
+    "configure")
+        shift;
+        configure_for_frama_c "$@";
+        ;;
+    "make-wrapper")
+        shift;
+        ${FRAMAC_SHARE}/analysis-scripts/make_wrapper.py "$0" "$@";
+        ;;
+    "normalize-jcdb")
+        shift;
+        normalize_jcdb "$@";
+        ;;
     *)
         echo "error: unrecognized command: $command"
 esac

headers/header_spec.txt

@@ -128,6 +128,7 @@ share/analysis-scripts/find_fun.py: .ignore
 share/analysis-scripts/flamegraph.pl: CDDL
 share/analysis-scripts/git_utils.py: .ignore
 share/analysis-scripts/list_files.py: .ignore
+share/analysis-scripts/make_wrapper.py: .ignore
 share/analysis-scripts/parse-coverage.sh: .ignore
 share/analysis-scripts/README.md: .ignore
 share/analysis-scripts/results_display.py: .ignore

share/analysis-scripts/fc_stubs.c

+// Stub for a main function which reads arguments from the command line, to be
+// used by the Eva plug-in.
+// This stub emulates non-deterministic input of up to 5 arguments, each up
+// to 256 characters long. This is sufficient to ensure arbitrary input in
+// virtually every case.
+// Do not forget to add option '-main eva_main' in order to use this stub.
+
+#ifdef __FRAMAC__
+# include "__fc_builtin.h"
+int main(int, char **);
+static volatile int nondet;
+int eva_main() {
+  int argc = Frama_C_interval(0, 5);
+  char argv0[256], argv1[256], argv2[256], argv3[256], argv4[256];
+  char *argv[5] = {argv0, argv1, argv2, argv3, argv4};
+  //@ loop unroll 5;
+  for (int i = 0; i < 5; i++) {
+    Frama_C_make_unknown(argv[i], 255);
+    argv[i][255] = 0;
+  }
+  return main(argc, argv);
+}
+#endif // __FRAMAC__

share/analysis-scripts/find_fun.py

@@ -101,8 +101,8 @@ else:
    if possible_declarators != []:
       print("Possible declarations for function '%s' in the following file(s):"
             % fname)
-      print("  " + "\n  ".join(possible_declarators))
+      print("  " + "\n  ".join(map(os.path.relpath, possible_declarators)))
    if possible_definers != []:
       print("Possible definitions for function '%s' in the following file(s):"
             % fname)
-      print("  " + "\n  ".join(possible_definers))
+      print("  " + "\n  ".join(map(os.path.relpath, possible_definers)))

share/analysis-scripts/make_wrapper.py

+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2018                                               #
+#    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 script serves as wrapper to 'make' (when using the analysis-scripts
+# GNUmakefile template): it parses the output and suggests useful commands
+# whenever it can, by calling frama-c-script itself.
+
+import subprocess
+import sys
+import os
+import re
+from functools import partial
+
+if len(sys.argv) < 3:
+   print("usage: %s path-to-frama-c-script target" % sys.argv[0])
+   print("       Builds the specified target, parsing the output to")
+   print("       identify and recommend actions in case of failure.")
+   print("       The first argument must be the path to the frama-c-script")
+   print("       binary.")
+   sys.exit(1)
+
+framac_script = sys.argv[1]
+target = sys.argv[2]
+args = sys.argv[3:]
+
+out = subprocess.Popen(['make', target] + args,
+                       stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+
+output = out.communicate()[0].decode('utf-8')
+
+re_missing_spec = re.compile("Neither code nor specification for function ([^,]+),")
+re_recursive_call_start = re.compile("detected recursive call")
+re_recursive_call_end = re.compile("Use -eva-ignore-recursive-calls to ignore")
+
+tips = []
+
+lines = iter(output.splitlines())
+for line in lines:
+    print(line)
+    match = re_missing_spec.search(line)
+    if match:
+       fname = match.group(1)
+       def action(fname):
+           out = subprocess.Popen([framac_script, "find-fun", fname],
+                                  stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+           output = out.communicate()[0].decode('utf-8')
+           re_possible_definers = re.compile("Possible definitions for function")
+           find_fun_lines = iter(output.splitlines())
+           for find_fun_line in find_fun_lines:
+              if re_possible_definers.match(find_fun_line):
+                 found_files = [next(find_fun_lines)]
+                 while True:
+                    try:
+                       found_files.append(next(find_fun_lines))
+                    except StopIteration:
+                       if len(found_files) > 1:
+                          print("Found several files defining function '"
+                                + fname + "', cannot recommend automatically.")
+                          print("Check which one is appropriate and add it " +
+                                "to the list of sources to be parsed:")
+                          print("\n".join(found_files))
+                       else:
+                          print("Add the following file to the list of "
+                                + "sources to be parsed:\n" + found_files[0])
+                       return
+           print("Could not find any files defining " + fname + ".")
+           print("Find the sources defining it and add them, " +
+                 "or provide a stub.")
+       tip = {"message": "Found function with missing spec: " + fname + "\n" +
+              "   Looking for files defining it...",
+              "action":partial(action, fname)
+       }
+       tips.append(tip)
+    else:
+       match = re_recursive_call_start.search(line)
+       if match:
+          def action():
+             print("Consider patching or stubbing the recursive call, " +
+                   "then re-run the analysis.")
+          msg_lines = []
+          line = next(lines)
+          while True:
+             match = re_recursive_call_end.search(line)
+             if match:
+                tip = {"message": "Found recursive call at:\n" +
+                       "\n".join(msg_lines),
+                       "action":action
+                       }
+                tips.append(tip)
+                break
+             else:
+                msg_lines.append(line)
+                try:
+                   line = next(lines)
+                except StopIteration:
+                   print("** Error: EOF without ending recursive call stack?")
+                   assert False
+
+if tips != []:
+   print("")
+   print("***** make-wrapper recommendations *****")
+   print("")
+   counter = 1
+   print("*** recommendation #" + str(counter) + " ***")
+   print("")
+   for tip in tips:
+      if counter > 1:
+         print("")
+         print("*** recommendation #" + str(counter) + " ***")
+      print(str(counter) + ". " + tip["message"])
+      counter += 1
+      tip["action"]()

src/kernel_services/ast_queries/json_compilation_database.ok.ml

@@ -81,6 +81,10 @@ let split_command_args s =
       let c = String.get s i in
       let new_state, new_acc =
         match state, prev_c, c with
+        | Outside_quote, '\\', c when c = '\"' || c = '\'' ->
+          (* escaped quote, continue with previous arg *)
+          Buffer.add_char buf c;
+          state, acc
         | Outside_quote, _, q when q = '\'' || q = '\"' ->
           (* continue previous arg with q *)
           Buffer.add_char buf q;

tests/jcdb/jcdb.c

 /* run.config
 EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
 OPT: -json-compilation-database @PTEST_DIR@ -print
-OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -print
+OPT: @PTEST_DIR@/jcdb2.c -json-compilation-database @PTEST_DIR@/with_arguments.json -print
 OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
 EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
 */

tests/jcdb/oracle/jcdb.1.res.oracle

 [kernel] Parsing tests/jcdb/jcdb.c (with preprocessing)
+[kernel] Parsing tests/jcdb/jcdb2.c (with preprocessing)
 /* Generated by Frama-C */
 #include "errno.h"
 #include "stdarg.h"

tests/jcdb/with_arguments.json

@@ -16,5 +16,9 @@
           "-UTOUNDEF"
       ],
       "file": "jcdb.c"
+    },
+    { "directory": "tests/jcdb",
+      "command": "/usr/bin/cc -DONION_VERSION=\\\"0.1.tr\\\" -Ibla -o jcdb2.o -c jcdb2.c jcdb.c",
+      "file": "jcdb2.c"
     }
 ]