Merge branch 'feature/script/ast-diff' into 'master'

Update analysis scripts for new features

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

doc/userman/user-changes.tex

@@ -6,6 +6,7 @@ release. First we list changes of the last release.
 \section*{Frama-C+dev}
 \begin{itemize}
 \item Removed Journalisation
+\item \textbf{Preparing the Sources:} added option \texttt{-ast-diff}.
 \end{itemize}
 
 \section*{24.0 (Chromium)}

doc/userman/user-sources.tex

@@ -332,6 +332,31 @@ in case of \texttt{UNROLL} pragma.
 supported are typedefs redefinition.
 \end{description}
 
+\section{Incremental parsing} (experimental)\label{sec:incremental-parsing}
+
+Parsing large code bases takes a non-negligible amount of time.
+More importantly, non-modular analyses need to be recomputed in their entirety
+even for minuscule AST changes.
+
+In order to help deal with these issues, and to help support for future
+incremental analyses (which recompute results only for the modified AST parts
+and their dependencies), you can use option \optiondef{-}{ast-diff}.
+It enables computing the difference between a previous AST (loaded via
+option \verb|-load| (Section~\ref{sec:saveload}) and the AST computed from the
+current sources. This difference is stored by the \FramaC kernel and can be
+used by plug-ins which support it. Note however that since \verb|-load| implies that
+files given on the command line are ignored, \verb|-load| and \verb|-ast-diff| with
+the list of C files to consider must be properly sequenced through the use of
+\verb|-then| or one of its variants (Section~\ref{sec:then}), as in:
+\begin{lstlisting}[language=shell]
+frama-c -load previous.sav -then -ast-diff file1.c file2.c [...]
+\end{lstlisting}
+
+{\em Note: currently, parsing and type-checking are systematically performed
+  even with this option, and \verb|-ast-diff| compares the normalized ASTs.
+  In the future, though, these steps should be refactored to allow saving
+  further time.}
+
 \section{Predefined macros}\label{sec:predefined-macros}
 
 \FramaC, like several compilers and code analysis tools, predefines and uses

man/frama-c.1.md

@@ -119,6 +119,11 @@ with non-trivial control flow are never duplicated. Defaults to yes.
 : reads ACSL annotations. This is the default. Annotations are pre-processed
 by default. Use -no-pp-annot if you don't want to expand macros in annotations.
 
+[-no]-ast-diff
+: computes AST differences between a loaded session (loaded with **-load**)
+and the current sources. These can then be used by plug-ins supporting
+incremental analyses.
+
 -autocomplete *p1,...,pn*
 : lists the options of plugins *p1,...,pn* in a format suitable for
 autocompletion scripts.

share/analysis-scripts/analysis.mk

@@ -28,10 +28,12 @@
 #
 # FRAMAC        frama-c binary
 # FRAMAC_GUI    frama-c gui binary
+# IVETTE        ivette binary
 # CPPFLAGS      preprocessing flags
 # MACHDEP       machdep
 # FCFLAGS       general flags to use with frama-c
 # FCGUIFLAGS    flags to use with frama-c-gui
+# IVETTEFLAGS   flags to use with Ivette
 # EVAFLAGS      flags to use with the Eva plugin
 # EVABUILTINS   Eva builtins to be set (via -eva-builtin)
 # EVAUSESPECS   Eva functions to be overridden by specs (-eva-use-spec)
@@ -40,6 +42,8 @@
 # FLAMEGRAPH    If set (to any value), running an analysis will produce an
 #               SVG + HTML flamegraph at the end.
 #
+# AST_DIFF      If set (to any value), enables usage of -ast-diff during parse.
+#
 # There are several ways to define or change these variables.
 #
 # With an environment variable:
@@ -60,6 +64,11 @@
 #
 # target.parse: file1.c file2.c file3.c...
 #
+# NOTE ABOUT AST_DIFF:
+# - If AST_DIFF is set to a non-empty value (e.g. `fcmake AST_DIFF=y`), then
+#   during parsing (rule %.parse), we check if there already exists a framac.sav
+#   file. If so, we rename it framac.reparse and, instead of parsing from zero,
+#   we reload this file and apply -ast-diff before reparsing the sources.
 
 # Test if Makefile is > 4.0
 ifneq (4.0,$(firstword $(sort $(MAKE_VERSION) 4.0)))
@@ -108,6 +117,7 @@ fc_list = $(subst $(space),$(comma),$(strip $1))
 FRAMAC     ?= frama-c
 FRAMAC_SCRIPT = $(FRAMAC)-script
 FRAMAC_GUI ?= frama-c-gui
+IVETTE     ?= ivette
 EVAFLAGS   ?= \
   -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state \
   -eva-print-callstacks -eva-warn-key alarm=inactive \
@@ -119,6 +129,7 @@ EVAFLAGS   ?= \
 WPFLAGS    ?=
 FCFLAGS    ?=
 FCGUIFLAGS ?=
+IVETTEFLAGS ?=
 
 export LIBOVERLAY_SCROLLBAR=0
 
@@ -134,7 +145,6 @@ clean-backups:
 	  -regex '^.*_[0-9]{4}-[0-9]{2}-[0-9]{2}_[0-9]{2}-[0-9]{2}-[0-9]{2}\.eva(\.(log|stats|alarms|warnings|metrics))?' \
 	  -delete
 
-
 # --- Generic rules ---
 
 HR_TIMESTAMP := $(shell date +"%H:%M:%S %d/%m/%Y")# Human readable
@@ -151,10 +161,20 @@ SHELL        := $(shell which bash)
 	@#
 
 %.parse: SOURCES = $(filter-out %/command,$^)
-%.parse: PARSE = $(FRAMAC) $(FCFLAGS) $(if $(value MACHDEP),-machdep $(MACHDEP),) -cpp-extra-args="$(CPPFLAGS)" $(SOURCES)
+%.parse: PARSE = $(FRAMAC) \
+                 $(FCFLAGS) \
+                 $(if $(value MACHDEP),-machdep $(MACHDEP),) \
+                 -cpp-extra-args="$(CPPFLAGS)" $(SOURCES) \
+
 %.parse: $$(if $$^,,.IMPOSSIBLE) $$(shell $(SHELL) $(DIR)cmd-dep.sh $$@/command $$(PARSE))
 	@$(call display_command,$(PARSE))
 	mkdir -p $@
+	$(if $(AST_DIFF),\
+	  $(if $(wildcard $*.eva/framac.sav), \
+               mv $*.eva/framac.sav $@/framac.reparse,\
+               $(if $(wildcard $@/framac.sav), \
+                    mv $@/framac.sav $@/framac.reparse,true)),\
+          true)
 	mv -f $@/{command,running}
 	{
 	  $(call time_with_output,$@/stats.txt) \
@@ -164,7 +184,9 @@ SHELL        := $(shell which bash)
 	      -metrics -metrics-log a:$@/metrics.log \
 	      -save $@/framac.sav \
 	      -print -ocode $@/framac.ast -then -no-print \
-	    || ($(RM) $@/stats.txt && false) # Prevents having error code reporting in stats.txt
+	    || (mv -f $@/{running,command} &&
+	        $(RM) $@/stats.txt &&
+	        false) # Prevents having error code reporting in stats.txt
 	} 2>&1 |
 	  $(SED_UNBUFFERED) '/\[metrics\]/,999999d' |
 	  tee $@/parse.log
@@ -176,7 +198,14 @@ SHELL        := $(shell which bash)
 	mv $@/{running,command}
 	touch $@ # Update timestamp and prevent remake if nothing changes
 
-%.eva: EVA = $(FRAMAC) $(FCFLAGS) -eva $(EVAFLAGS)
+define incremental
+  $(if $(AST_DIFF),\
+    $(if $(wildcard $@/framac.sav),\
+      -eva-load $@/framac.sav,\
+      $(warning Cannot do incremental analysis: no previously saved state)))
+endef
+
+%.eva: EVA = $(FRAMAC) $(FCFLAGS) -eva $(call incremental,$1) $(EVAFLAGS)
 %.eva: PARSE_RESULT = $(word 1,$(subst ., ,$*)).parse
 %.eva: $$(PARSE_RESULT) $$(shell $(SHELL) $(DIR)cmd-dep.sh $$@/command $$(EVA)) $(if $(BENCHMARK),.FORCE,)
 	@$(call display_command,$(EVA))
@@ -185,7 +214,7 @@ SHELL        := $(shell which bash)
 	{
 	  $(call time_with_output,$@/stats.txt) \
 	    $(EVA) \
-	      -load $(PARSE_RESULT)/framac.sav -save $@/framac.sav \
+	      -load $(PARSE_RESULT)/framac.sav \
 	      -eva-flamegraph $@/flamegraph.txt \
 	      -kernel-log w:$@/warnings.log \
 	      -from-log w:$@/warnings.log \
@@ -193,12 +222,16 @@ SHELL        := $(shell which bash)
 	      -scope-log w:$@/warnings.log \
 	      -eva-log w:$@/warnings.log \
 	      -then \
+	      -remove-projects @all_but_current -save $@/framac.sav \
+	      -then \
 	      -report-csv $@/alarms.csv -report-no-proven \
 	      -report-log w:$@/warnings.log \
 	      -metrics-eva-cover \
 	      -metrics-log a:$@/metrics.log \
 	      -nonterm -nonterm-log a:$@/nonterm.log \
-	    || ($(RM) $@/stats.txt && false) # Prevents having error code reporting in stats.txt
+	    || (mv -f $@/{running,command} &&
+	        $(RM) $@/stats.txt &&
+	        false) # Prevents having error code reporting in stats.txt
 	} 2>&1 |
 	  $(SED_UNBUFFERED) '/\[eva\] Values at end of function/,999999d' |
 	  tee $@/eva.log
@@ -231,7 +264,9 @@ SHELL        := $(shell which bash)
 	      -then \
 	      -report-csv $@/alarms.csv -report-no-proven \
 	      -report-log w:$@/warnings.log \
-	    || ($(RM) $@/stats.txt && false) # Prevents having error code reporting in stats.txt
+	    || (mv -f $@/{running,command} &&
+	        $(RM) $@/stats.txt &&
+	        false) # Prevents having error code reporting in stats.txt
 	} 2>&1 |
 	  tee $@/wp.log
 	{
@@ -247,6 +282,9 @@ SHELL        := $(shell which bash)
 %.gui: %
 	$(FRAMAC_GUI) $(FCGUIFLAGS) -load $^/framac.sav &
 
+%.ivette: %
+	$(IVETTE) $(IVETTEFLAGS) -load $^/framac.sav &
+
 # Produce and open an SVG + HTML from raw flamegraph data produced by Eva
 %/flamegraph: %/flamegraph.html
 	@