


\section{Introduction}
\vspace*{-2mm}

Global static analysis and verification tools can greatly help
developers detect high-level, semantic errors in programs or certify
their absence. This is specially the case for high-level, dynamic
languages such as Prolog, where obtaining information such as modes,
types, determinacy, non-failure, cardinality, variable sharing in
structures, constraints, termination, cost, etc., and checking it
against specifications, in the form of annotations or assertions, can
be invaluable aids to programmers. 

Arguably, such tools are more effective the earlier the
stage in which they are applied within the software development
process. Particularly useful is their application
during
code development, simultaneously with the code writing process,
alongside the compiler, debugger, etc.
The tight integration of global analysis and verification
at such early stages
requires fast response times and
source-level presentation of the results within the code development
environment, in order to provide timely and useful feedback to the
programmer.
However, triggering a full and precise semantic analysis of a software
project every time a change is made can be expensive and may not be
able to meet the requirements of the scenario described. This is
specially the case when complex properties need to be inferred for
large, realistic code bases.

Our approach builds on the {\sf CiaoPP}\xspace program development
framework~\cite{aadebug97-informal-short,prog-glob-an-short,assrt-theoret-framework-lopstr99-short,ciaopp-sas03-journal-scp-short,intermod-incanal-2020-tplp-short},
which performs combined static and dynamic program analysis, assertion
checking, and program transformations, based on computing provably
safe approximations of properties, generally using the technique of
abstract interpretation~\cite{Cousot77}.
This framework supports natively Prolog and several extensions within
the LP and CLP paradigms, and can also be applied to
other high- and low-level languages, using the now 
well-understood technique of semantic translation into intermediate
Horn clause-based representation. 
The framework has many uses, but one of the main ones is precisely as
an aid for the programmer during program development, since it can
capture semantic errors that are significantly higher-level than those
detected by classical compilers, as well as produce certificates that
programs do not violate their assertions, eliminate run-time
assertion tests, etc. 

In our framework, 
the requirements for fast response time and precision
stemming from interactive use pointed out above are
addressed 
through a number of techniques, and in particular by an efficient
fixpoint engine, which 
performs context- and path-sensitive
inter-procedural analysis \emph{incrementally},
i.e.,
reactively to fine-grain
edits, avoiding
reanalyses where possible, both within modules and across the
modular organization of the code into
separate compilation units.
In this tool paper we illustrate how the integration of
the static analysis and verification framework within an integrated
development environment (IDE) 
takes advantage of the incremental and modular features
to achieve a high level of reactivity when reflecting analysis and
verification results back as colorings and tooltips directly on the
program text---the tool's {\sf VeriFly}\xspace mode.
The concrete integration 
described
builds on an existing
Emacs-based development environment for the {\sf Ciao}\xspace language, 
and reuses in part
off-the-shelf ``on-the-fly''
\emph{syntax} checking capabilities offered by the Emacs {\sf flycheck}\xspace
package.
Emacs was chosen because it is a solid platform and preferred by many
experienced users.
However, this low-maintenance approach should be easily reproducible in other
modern extensible editors and mature program development environments.

\vspace*{-2mm}
\section{The {\sf CiaoPP}\xspace Framework}\label{sec:ciaopp-framework}
\vspace*{-2mm}

We start by providing an informal overview of the components and
operation of the 
{\sf CiaoPP}\xspace framework
(Fig.~\ref{fig:ciaopp}).


\begin{figure}[t]
  \vspace*{-3mm}
  \centering
  \resizebox{1\textwidth}{!}{
    \input{ciaopp-incanal-wtrue}
  }
  \vspace*{-3mm}  
  \vspace*{-3mm}  
  \caption{Architecture of the {\sf CiaoPP}\xspace framework.}\label{fig:ciaopp}
  \vspace*{-3mm}
  \vspace*{-1mm}
\end{figure}

\vspace*{-4mm}
\paragraph{\textbf{Front end.}}

Before getting into the analysis and verification phases, the tool's
front end 
transforms any syntactic or semantic extensions used in the input
program (such as, e.g, functional notation, or, more specifically for
our discussion, the syntactic sugar related to assertions) in order to
reduce each module to the intermediate representation that the
framework works with.  This representation, which we refer to as the
HC IR\xspace, is fundamentally plain Horn clauses (plain Prolog) extended
with the (canonical part) of the assertion language, reviewed in the
next section.
Although beyond the scope of this paper, as mentioned in the
introduction, the framework can also be applied to other input
languages, outside (C)LP, which is done by translating such input
programs to the same
HC IR\xspace~\cite{decomp-oo-prolog-lopstr07-short}.\footnote{
  This approach is used nowadays in many analysis and
  verification tools
~\cite{
  Peralta-Gallagher-Saglam-SAS98,
  HGScam06-short,decomp-oo-prolog-lopstr07-short,
  mod-decomp-jist09-short,DBLP:conf/tacas/GrebenshchikovGLPR12-short,
  DBLP:conf/cav/GurfinkelKKN15-shorter,
  AngelisFPP17,
  resource-verification-tplp18-shortest,
  resources-blockchain-sas20-short,
  big-small-step-vpt2020-shorter}.
The front end is also in charge of these translations, as well as of
translating the analysis and verification results back to the source
language.
Techniques such as partial evaluation and program specialization offer
powerful methods to obtain such translations with provable
correctness---see~\cite{anal-peval-horn-verif-2021-tplp} for a recent survey.}
However, herein we concentrate on the native use of the tool for (C)LP
programs.  The examples will be written in
{\sf Ciao}\xspace~Prolog~\cite{hermenegildo11:ciao-design-tplp,ciao-reference-manual-1.20-short}\footnote{\url{https://github.com/ciao-lang/devenv}}
using its assertions library and some additional syntactic sugar such
as functional notation, but the tool can easily be adapted to process
source files for other Prolog flavors and systems.
The framework itself is also written in {\sf Ciao}\xspace.

\vspace*{-4mm}
\paragraph{\textbf{The assertion language.}}

A fundamental element of the framework 
is its \emph{assertion
  language}~\cite{full-prolog-esop96-short,prog-glob-an-short,assert-lang-disciplbook-short}.
Such assertions can express a wide range of properties, including
functional (state) properties, such as modes, types,
sharing/aliasing, constraints, etc.,
as well as non-functional (i.e., global, computational)
properties, such as determinacy, non-failure, cardinality, or
resource usage (energy, time, memory, \ldots). The set of properties is
extensible and new abstract domains (see the later discussion of the
analysis) can be defined as ``plug-ins'' to support them.  Assertions
associate these properties to different program points, and
are used 
for multiple purposes,
including writing specifications, 
reporting static analysis and verification results (to the programmer, other
parts of the framework, or other tools), providing assumptions, describing
unknown code, generating test cases automatically, or producing documentation.

\noindent
{\sc Predicate-level assertions}
allow describing \emph{sets} of \emph{preconditions} and \emph{conditional
  postconditions} on the state for a given 
predicate (as well as global properties).
In particular, \texttt{pred}\xspace assertions are of the form:\\ [-2em]
\begin{center}
  \hltexttt{:- [ \mbox{\ensuremath{\mathit{Status}}\xspace} ] pred \mbox{\ensuremath{\mathit{Head}}\xspace} [: \mbox{\ensuremath{\mathit{Pre}}\xspace} ] [=>
    \mbox{\ensuremath{\mathit{Post}}\xspace} ] [+ \mbox{\ensuremath{\mathit{Comp}}\xspace} ].}
\end{center}
\vspace*{-1mm}
\noindent
where \ensuremath{\mathit{Head}}\xspace is a predicate descriptor
that denotes the predicate that the assertion applies to, and \ensuremath{\mathit{Pre}}\xspace and
\ensuremath{\mathit{Post}}\xspace are conjunctions of \emph{state property} literals (the modes,
types, constraints, etc.), which can include arguments, and these can
also be variables from \ensuremath{\mathit{Head}}\xspace.
Such properties are predicates, typically written in
(subsets of) 
the source
language, and thus runnable, so that
they can be used as run-time checks, and which (see ``Assertion
verification'' later in this section) may be
abstracted and inferred by some domain in {\sf CiaoPP}\xspace.
They can be imported from system libraries or user-defined.
\ensuremath{\mathit{Pre}}\xspace expresses properties that hold when \ensuremath{\mathit{Head}}\xspace is called.  \ensuremath{\mathit{Post}}\xspace
states properties that hold if \ensuremath{\mathit{Head}}\xspace is called in a state compatible
with \ensuremath{\mathit{Pre}}\xspace and the call succeeds. Both \ensuremath{\mathit{Pre}}\xspace and \ensuremath{\mathit{Post}}\xspace can be empty
conjunctions (meaning true), and in that case they can be omitted.
\ensuremath{\mathit{Comp}}\xspace describes properties of the whole computation such as
determinism, non-failure, resource usage,
termination, etc., and they also apply
to calls to the predicate 
that meet \ensuremath{\mathit{Pre}}\xspace.
Assertions are optional, and there can be multiple \texttt{pred}
assertions for a predicate.
This allows describing different behaviors for the same predicate for
different call substitutions, i.e., different \emph{modes}.
If multiple \texttt{pred} assertions are present for a given
predicate, 
their \ensuremath{\mathit{Pre}}\xspace fields then describe the set of all admissible calls to the
predicate, i.e., at least one \ensuremath{\mathit{Pre}}\xspace must hold for each call to \ensuremath{\mathit{Head}}\xspace.

$\ensuremath{\mathit{Status}}\xspace$
is a qualifier of the meaning of the assertion. Here we consider (in
the context of static assertion
checking)
the following $\ensuremath{\mathit{Status}}\xspace$es (cf.\ Fig.~\ref{fig:ciaopp}):

\vspace*{-2mm}
\begin{itemize}
  \itemsep=0pt
\item {\tt \textcolor{ciaocheck}{check}}: the assertion expresses properties that must hold at
  run-time, i.e., that the analyzer should prove (or else generate run-time
  checks for). {\tt check} is the \emph{default} status, 
  and can be omitted.
\item {\tt \textcolor{ciaochecked}{checked}}: the analyzer proved that the property holds in all executions.
\item {\tt \textcolor{ciaofalse}{false}}: the analyzer proved that the property does not hold in some execution.
\end{itemize}

Additionally, assertions with \texttt{trust} status can be used to
provide the analyzer with information that it should \emph{assume}. This
can be useful for, e.g., describing external or unknown code or 
improving analysis precision.

Fig.~\ref{fig:nrevf} 
provides some examples of assertions. 
The syntax that allows including the \texttt{pred}\xspace assertions is made
available through the \texttt{assertions} package (packages are
similar to modules but oriented towards providing syntactic and semantic
extensions).
Predicates \texttt{nrev/2} and \texttt{conc/2} define naive reverse
and are written using the \texttt{functional} notation package.
The first assertion (line~\ref{asrtone})
expresses that calls to \texttt{nrev/2} with the first argument bound
to a list are admissible, and that if such calls succeed, then the
second argument should also be bound to a list (as well as being
non-failing, deterministic, terminating, and quadratic). 
Thus, such an assertion
provides information on (a generalization of) types and modes, as well
as determinism, failure, cost, etc.

\begin{figure}[t]
\vspace*{-3mm}
  \prettylstciao
\begin{lstlisting}[belowskip=0mm,escapechar=@]
:- module(_, [nrev/2], [assertions, nativeprops, functional]).
:- entry nrev/2 : {list, ground} * var.                 @\label{entry}@
:- use_module(someprops).

:- pred nrev(A, B) : list(A) => list(B) 
   + (not_fails,is_det,terminates,steps_o(exp(length(A),2)). @\label{asrtone}@
nrev([])    := [].
nrev([H|L]) := ~conc(nrev(L),[H]).

:- pred conc(A,B,C) : list(A) => size_ub(C,length(A)+length(B)) + steps_o(length(A)).
conc([],    L) := L.
conc([H|L], K) := [ H | conc(L,K) ]. 
\end{lstlisting}
\vspace*{-3mm}
\caption{Naive reverse with some assertions.}\label{fig:nrevf}
\vspace*{-3mm}
\end{figure}

\begin{figure}[t]
\vspace*{-3mm}
  \prettylstciao
\begin{lstlisting}[belowskip=0mm,escapechar=]
:- module(someprops, _, [functional, hiord, assertions]).

:- prop color/1.    
color := red | blue | green.

:- prop list/1.     
list := [] | [_ | list].    

:- prop list/2.  
list(T) := [] | [~T | list(T)].

:- prop sorted/1.   
sorted := [] | [_].
sorted([X,Y|Z]) :- X @< Y, sorted([Y|Z]).
\end{lstlisting}
\vspace*{-3mm}
\caption{Examples of state \texttt{prop}erty definitions.}\label{fig:fmoreprops}
\vspace*{-3mm}
\end{figure}


Fig.~\ref{fig:fmoreprops} provides some examples of state properties
(\texttt{prop}s, for short), which, as mentioned before, 
are defined and exported/imported as normal
predicates: e.g., in Fig.~\ref{fig:nrevf} \texttt{list/1},
\texttt{list/2}, or \texttt{color/1} are imported from the 
\texttt{someprops} user module 
while others (e.g., \texttt{size\_ub/2}) from the system's
\texttt{nativeprops} library.
Properties need to be marked explicitly as such
with a \texttt{:- prop} declaration, 
and this flags that they need to meet some
restrictions~\cite{assert-lang-disciplbook-short,ciao-reference-manual-1.20-short}.
E.g., their execution should terminate 
for any possible call since, as 
discussed later, 
\texttt{prop}s will not only be checked at compile time, 
but may also be involved in run-time checks. 
Types are just a particular case (further restriction) of state
properties.  Different type systems
are provided as libraries.
Properties like \texttt{list/1} 
that are in addition regular
types can be flagged as such: \verb|:- prop list/1 + regtype.|
or, more compactly, 
\verb|:- regtype list/2.|

The combination of multiple assertions for a given predicate is
defined more precisely as follows: 
given a
set of assertions $\{a_1, \ldots, a_n\}$, with $a_i = ``\texttt{:- pred }$ $\ensuremath{\mathit{Head}}\xspace
  \texttt{ : } \ensuremath{\mathit{Pre}}\xspace_i \texttt{ => } \ensuremath{\mathit{Post}}\xspace_i \texttt{.}$'' the set of
  \emph{assertion conditions} for \ensuremath{\mathit{Head}}\xspace is $\{ C_0, C_1, \ldots , C_n\}$,
  with:
  \[
  \begin{array}{c}
  \ C_0 = \callsAsr{\ensuremath{\mathit{Head}}\xspace}{\vee_{j = 1}^{n} \ensuremath{\mathit{Pre}}\xspace_j}, \ and \\
  C_i = \successAsr{\ensuremath{\mathit{Head}}\xspace}{\ensuremath{\mathit{Pre}}\xspace_i}{\ensuremath{\mathit{Post}}\xspace_i}, i = 1\ldots n
  \end{array}
  \]
where $\callsAsr{\ensuremath{\mathit{Head}}\xspace}{\ensuremath{\mathit{Pre}}\xspace}$
states conditions on all concrete calls to the predicate described by
\ensuremath{\mathit{Head}}\xspace, and $\successAsr{\ensuremath{\mathit{Head}}\xspace}{\ensuremath{\mathit{Pre}}\xspace_i}{\ensuremath{\mathit{Post}}\xspace_i}$ the conditions
on the success constraints produced by calls to \ensuremath{\mathit{Head}}\xspace if $\ensuremath{\mathit{Pre}}\xspace_i$ is
satisfied.
If the assertions $a_i$ above, $i=1, \ldots, n$, include a
\hltexttt{\mbox{+ \ensuremath{\mathit{Comp}}\xspace}} field, then the set of \emph{assertion
  conditions} also includes conditions of the form:
$\compAsr{\ensuremath{\mathit{Head}}\xspace}{\ensuremath{\mathit{Pre}}\xspace_i}{\ensuremath{\mathit{Comp}}\xspace_i}$, for $i=1, \ldots, n$, that express
properties of the whole computation for calls to \ensuremath{\mathit{Head}}\xspace if $\ensuremath{\mathit{Pre}}\xspace_i$ is
satisfied.

\medskip
\noindent
In addition to predicate-level assertions, {\sc program-point
  assertions} are of the form:
\vspace*{-1mm}
  \prettylstciao
\begin{lstlisting}[belowskip=0mm,escapechar=@,frame=,numbers=none]
      @\emph{Status}@(@\emph{StateFormula}@),
\end{lstlisting}
  and they can be placed at program locations where a new literal may
  be added.  E.g., for status {\tt \textcolor{ciaocheck}{check}} they should be interpreted
  as ``whenever computation reaches a state corresponding to this
  program point,
\emph{StateFormula} should hold.'' For example,
\noindent
  \prettylstciao
\begin{lstlisting}[belowskip=0mm,escapechar=@,frame=,numbers=none]
      check((list(color, A), var(B))), 
\end{lstlisting}
  \noindent is a program-point assertion 
that checks whether \texttt{A} is instantiated to a list of colors and
\texttt{B} is a variable, where \texttt{A} and
\texttt{B} are variables of the clause where the assertion appears.

\vspace*{-4mm}
\paragraph{\textbf{Assertion-related syntactic sugar.}}

In order to facilitate writing assertions, as well as compatibility
with different systems, the assertion language also provides syntactic
sugar such as \emph{modes}, Cartesian product notation, markdown
syntax, etc.
For example, 
the following set of \texttt{pred}\xspace assertions use Cartesian product
notation to provide information on a reversible sorting predicate:
\noindent \prettylstciao
\vspace*{-1mm}
\begin{lstlisting}[belowskip=0mm,escapechar=@,frame=,numbers=none]
:- pred sort/2 : list(num) * var => list(num) * list(num) + is_det. 
:- pred sort/2 : var * list(num) => list(num) * list(num) + non_det. 
\end{lstlisting}
\noindent (in addition, curly brackets can be used to group
properties---see Fig.~\ref{fig:nrevf}). 
The assertion language also allows defining \emph{modes}, which are
macros that can be placed in argument positions of \ensuremath{\mathit{Head}}\xspace and expand to
properties in different assertion fields.  For example, using
the \texttt{isomodes} library 
the assertions above can also be expressed as:
\vspace*{-1mm}
\begin{lstlisting}[escapechar=@,frame=,numbers=none]
:- pred sort(+list(num), -list(num)) + is_det.
:- pred sort(-list(num), +list(num)) + non_det.
\end{lstlisting}
\vspace*{-1mm}
Or, if no types and only modes are used:
\vspace*{-1mm}
\begin{lstlisting}[escapechar=@,frame=,numbers=none]
:- pred sort(+, -).
:- pred sort(-, +).
\end{lstlisting}
\vspace*{-1mm}
There is also an alternative encoding via ``markdown-style'' comments
(provided by libraries \texttt{doccomments} and \texttt{markdown})
that allows writing, e.g.:
\vspace*{-1mm}
\begin{lstlisting}[basicstyle=\ttfamily\small,escapechar=@,frame=,numbers=none]
\end{lstlisting}
\vspace*{-1mm}
Thanks to these libraries and the underlying syntactic expansion
mechanisms, and their modular nature, it is easy to adapt the tool to
other syntactic forms, on a per-module basis, such as for example
supporting ``Quintus-style'' modes:
\noindent
\vspace*{-1mm}
\begin{lstlisting}[escapechar=@,frame=,numbers=none]
:- mode sort(+, -).
:- mode sort(-, +).
\end{lstlisting}
\vspace*{-1mm}
or the SWI-Prolog \texttt{pldoc}-style annotations for documentation,
making all of them machine checkable.

\vspace*{-4mm}
\paragraph{\textbf{Static Program Analysis:}}
The {\sf CiaoPP}\xspace~verification framework uses analyses based on
abstract interpretation (the ``Static Analyzer'' in
Fig.~\ref{fig:ciaopp})
to compute safe over-approximations of the program
semantics. 
Given a program $P$ and a set of queries $\mbox{$\cal Q$}$, an analysis graph is inferred
that abstracts the (possibly infinite) set of (possibly infinite) execution trees.
The analysis result is denoted by $\sem{\prog}_{\Q}^\alpha$, where $\alpha$ is the abstraction(s)
performed. By default, the abstract domains to be used are
automatically selected, depending the properties that appear in the
assertions, but manual selection is also possible. 
Nodes in this
graph abstract how predicates are called (i.e., how they are used in
the program). A predicate may have several nodes if there are
different calling situations (also known as context-sensitivity). For
each calling situation, properties that hold if the predicate succeeds
are also inferred,
and can be
represented by ({\tt \textcolor{ciaotrue}{true}}) assertions.
For our purposes, and without loss of generality, we treat $\ensuremath{\psem^\alpha}$ as a set
of tuples (one per node): 
$\{\tuple{L_1,\lambda_{1}^c,\lambda_{1}^s}, \ldots,
\tuple{L_n,\lambda_{n}^c,\lambda_{n}^s}\}$. In each
$\tuple{L_i,\lambda_{i}^c,\lambda_{i}^s}$ triple, $L_i$ is
a predicate descriptor, and $\lambda_{i}^c$ and $\lambda_{i}^s$ are,
respectively, the abstract call and success substitutions, elements of
abstract domain $D_\alpha$.
\footnote{As mentioned
  before, abstract domains are defined as plug-ins which provide the
  basic abstract domain lattice operations and transfer functions, and
  are made accessible to the generic fixpoint computation component.}
The edges in the graph capture how predicates call each other. Hence this
analysis graph also provides an abstraction of the paths explored by the
concrete executions through the program (also known as path-sensitivity).
The analysis graph thus embodies two different abstractions (two
different abstract domains): the graph itself is a \emph{regular
  approximation} of the paths through the program, using a domain of
regular structures. Separately, the abstract values (call and success
patterns) contained in the graph nodes are finite representations of
the states occurring at each point in these program paths, by means of
one or more data-related abstract domains. 

\vspace*{-4mm}
\paragraph{\textbf{Assertion verification:}}
To verify a program, the behaviors abstracted in $\sem{\prog}_{\Q}^\alpha$ are
compared 
with
program assertions (the ``Static Checker'' in Fig.~\ref{fig:ciaopp}).
The verification results are reported as changes in the status and
transformations of the assertions: {\tt \textcolor{ciaochecked}{checked}}, if the properties
are satisfied; {\tt \textcolor{ciaofalse}{false}} if some property was proved not to hold;
or {\tt \textcolor{ciaocheck}{check}} if it was not possible to determine any the first
two, in which case run-time checks will be included in the program to
make it run-time safe (Fig.~\ref{fig:ciaopp}).
Since in our framework the intended semantics is also specified
by using predicates, some of the properties may be
undecidable and also not exactly representable in the abstract
domains.
However, it is possible to under- and over-approximate them, denoted by
$\underapp{I}$ and $\overapp{I}$.
Such approximations are always computable by choosing the closest
element in the abstract domain. At the limit $\bot$ and $\top$ are,
respectively, an under-approximation and an over-approximation of any
specification.
Let $\renanalysis{\pv}$, where $\pv$ is a predicate descriptor, denote
the set of tuples resulting from the static analysis for predicate
$p\ in \ P$ w.r.t.\ $\mbox{$\cal Q$}$ renamed to variables $\vv$, i.e.:
$\renanalysis{\pv} = \{\tuple{\pv,
  \lambda^{c}\sigma,\lambda^{s}\sigma} \mid \exists
\tuple{\pvp,\lambda^c,\lambda^s} \in \ensuremath{\psem^\alpha}
\text{ and } \sigma
\text{ is a renaming }$ \\ $\text{substitution s.t. }
\pv= \pvp\sigma\}$.

\noindent
The following are some sufficient conditions, adapted
from~\citeauthor{assrt-theoret-framework-lopstr99-short}~(\citeyear{assrt-theoret-framework-lopstr99-short}),
and~\citeauthor{mod-ctchecks-lpar06-short}~(\citeyear{mod-ctchecks-lpar06-short}),
which allow deciding whether assertions are \texttt{\textcolor{ciaochecked}{checked}} or
\texttt{\textcolor{ciaofalse}{false}} with respect to the concrete semantics, based on the
abstract semantics:

\begin{itemize}

\item $\callsAsr{\pv}{\ensuremath{\mathit{Pre}}\xspace}$ is \emph{checked} (resp. \emph{false})
  for predicate $p \in P$ w.r.t.\ $\mbox{$\cal Q$}$ if \\ $\forall
  \tuple{\pv,\lambda^c,\lambda^s} \in \renanalysis{\pv}:
  \ \lambda^c \sqsubseteq \underapp{\ensuremath{\mathit{Pre}}\xspace}$
  (resp. $\lambda^c \sqcap \overapp{\ensuremath{\mathit{Pre}}\xspace} = \bot$).
  
\item $\successAsr{\pv}{\ensuremath{\mathit{Pre}}\xspace}{\ensuremath{\mathit{Post}}\xspace}$ is \emph{checked}
  (resp. \emph{false}) for predicate $p \in P$ w.r.t.\ $\mbox{$\cal Q$}$ if
  $\forall \tuple{\pv, \lambda^c,\lambda^s} \in \renanalysis{\pv}:
\ ( (\lambda^c
\sqcap \overapp{\ensuremath{\mathit{Pre}}\xspace} = \bot) \lor (\lambda^s \sqsubseteq
\underapp{\ensuremath{\mathit{Post}}\xspace}))$ \\
(resp. $\lambda^c \sqsubseteq \underapp{\ensuremath{\mathit{Pre}}\xspace} \land (\lambda^s \sqcap
\overapp{\ensuremath{\mathit{Post}}\xspace} = \bot)$ and there is at least one actual call to
predicate $p$ that succeeds).

\end{itemize}




\vspace*{-4mm}
\paragraph{\textbf{Supporting incrementality.}}
In order to support incrementality, the analysis graph produced by the
static analyzer is made persistent (``Analysis DB'' in
Fig.~\ref{fig:ciaopp}), storing
an abstraction of the behavior of each predicate and predicate (abstract) call
dependencies. In turn, the ``Front-end'' (Fig.~\ref{fig:ciaopp})
keeps track of and translates source code changes into, e.g., clause
and assertion additions, deletions, and changes in the intermediate
representation ($\mathsf{\Delta}$~{\sf CHC} in the figure).
These changes are transmitted to the static analyzer, which performs
incremental fixpoint computation. This process consists in finding
the parts of the graph that need to be deleted or recomputed,
following their dependencies, and updating the fixpoint
~\cite{intermod-incanal-2020-tplp-short,incanal-assrts-openpreds-lopstr19-post-short,inc-fixp-sas-short,incanal-toplas-short}.
The key point here is that a tight relation between the analysis results and the
predicates in the program is kept, allowing reducing the re-computation to the
part of the analysis that corresponds to the affected predicates, and only
propagating it to the rest of the analysis graph if necessary.

\vspace*{-2mm}
\section{{\sf VeriFly}\xspace: The On-the-fly IDE Integration}\label{sec:verifly}
\vspace*{-2mm}

Fig.~\ref{fig:ciaopp+ide} shows the overall architecture of {\sf VeriFly}\xspace,
the integration of the {\sf CiaoPP}\xspace framework with the new IDE components,
represented by the new box to the left, and the communication to and
from {\sf CiaoPP}\xspace.
As mentioned before, the tool interface is implemented within Emacs
and the on-the-fly support is provided by the Emacs ``{\sf flycheck}\xspace''
package.\footnote{\url{https://github.com/flycheck/flycheck}}
\textsf{Flycheck} is an extension developed for GNU Emacs originally
designed for on-the-fly \emph{syntax} checking, but we use it here in
a semantic context.
However, as also mentioned before, a similar integration is possible
with any reasonably extensible IDE.

\begin{figure}
  \hspace*{-2cm}
 \resizebox{1.15\textwidth}{!}{
    \input{ciaopp-flycheck-incanal-wtrue}
  }
  \vspace*{-3mm}  
  \vspace*{-3mm}  
  \caption{Integration of the {\sf CiaoPP}\xspace framework in the Emacs-based
    IDE.}\label{fig:ciaopp+ide}
  \vspace*{-3mm}  
\end{figure}

The overall architecture consists of a {\sf flycheck}\xspace adaptor (implementing
different {\sf Ciao}\xspace-based checkers, from syntactic to full analysis), a
{\sf CiaoPP}\xspace process that runs in the background in daemon mode, and a
lightweight client to {\sf CiaoPP}\xspace.
When a file is opened, modified, or saved, as well as after some small
period of inactivity, an editor checking event is triggered. Edit
events notify {\sf CiaoPP}\xspace (via the lightweight client) about program
changes, which can be both in code and assertions.
The {\sf CiaoPP}\xspace daemon receives these changes, and, behind the scenes,
transforms them
into changes at the HC IR\xspace level (also checking for syntactic errors),
and then incrementally (re-)analyzes the code and (re-)checks any 
reachable assertions.
The latter can be in libraries, other modules, language built-in
specifications, or of course (but not necessarily) in user code.
The results (errors, verifications, and warnings), from static (and
possibly also dynamic checks) are returned to the IDE and presented as
colorings and tooltips directly on the program text.
This overall behavior is what we have called in our tool the
``{\sf VeriFly}\xspace'' mode of operation.

\vspace*{-4mm}
\paragraph{\textbf{Details on the architecture.}} Currently, {\sf flycheck}\xspace requires
saving the contents of the source being edited (Emacs \emph{buffer})
into a temporary file and then invoking an external command.
In our case the external command is a lightweight client that
communicates with a running {\sf CiaoPP}\xspace process, executing as a an
\emph{active module}, a daemon process that executes in the background
and reacts to simple JSON-encoded queries via a
socket.\footnote{JSON-encoded interaction capabilities have been added
  recently to support tool interoperability and browser-based
  interactions, and to simplify future extensions.}
This {\sf CiaoPP}\xspace process is started once and kept alive for future
analyses, ensuring that no time is unnecessarily wasted in startup and
cleanups, as well as allowing caching some common analysis data, etc.\
for libraries. The approach similar to other like LSP (Language
Server Protocol).
Finally, {\sf Ciao}\xspace implements a ``shadow module'' mechanism that allows the
compiler to read alternative versions for some given modules. We use
this mechanism to make {\sf CiaoPP}\xspace (and other {\sf Ciao}\xspace-based checkers) read the
contents of temporary Emacs buffers during edition (saved as temporary
files with \emph{shadowed} names). This is specially useful to work in
(inter-)modular analysis where the analysis root is not necessarily
the active buffer.

\begin{figure}[t]
  \centering
  \vspace*{-3mm}
  \fbox{\includegraphics[width=0.60\textwidth,clip,trim=0 40 0 5]{option-browser}}
  \vspace*{-3mm}
  \caption{The {\sf CiaoPP}\xspace option browser.}\label{fig:browser}
  \vspace*{-3mm}
\end{figure}

\vspace*{-4mm}
\paragraph{\textbf{Customizing the analysis.}} In general, {\sf CiaoPP}\xspace can be run
fully automatically and does not \emph{require} the user to change the
configuration or provide invariants or
assertions, and, for example, selects automatically abstract domains,
as mentioned before. However, the system does have a configuration
interface that allows manual selection of abstract domains, and of
many parameters such as whether passes are incremental or not, the
level of context sensitivity, error and warning levels, the type of
output, etc.
Fig.~\ref{fig:browser} shows the option browsing
interface of the tool, as well as some options (abstract domain
selections) in the menus for the cost analysis, shape and type
analysis, pointer (logic variable) aliasing analysis, and numeric
analysis.

\begin{figure}[t]
  \centering
  \vspace*{-3mm}
  \fbox{\includegraphics[width=0.85\textwidth,clip,trim=0 78 4 3]{ann}}
  \vspace*{-3mm}
  \caption{An assertion within a parallelizer (\texttt{ann}).}\label{fig:ann}
  \vspace*{-3mm}
\end{figure}

\begin{figure}
  \centering
  \vspace*{-3mm}
  \fbox{\includegraphics[width=0.94\textwidth,clip,trim=0 25 0 0]{qsortdl}}
  \vspace*{-3mm}
  \caption{Sorting with incomplete data structures.}\label{fig:qsortdl-verified} 
  \vspace*{-3mm}
\end{figure}

\vspace*{-4mm}
\paragraph{\textbf{{\sf VeriFly}\xspace in action:}}
We now show some simple examples of the system in action.
Fig.~\ref{fig:ann} shows an
assertion being verified within a medium-sized program implementing an
automatic program parallelizer. The \texttt{add\_annotations} loop
traverses recursively a list of blocks and transforms sequential
sections into parallel expressions.  Upon opening the file the
assertion is underlined in green, meaning that it has been verified
({\tt \textcolor{ciaochecked}{checked}} status).  This ensures that upon entering the
procedure there is no variable (pointer) sharing between \texttt{Info}
(the input) and \texttt{Phrase}, i.e., \texttt{indep(Info,Phrase)};
that \texttt{Phrase} will arrive always as a free variable; and that
on output from the procedure, \texttt{Ind} and \texttt{Gnd} will be
ground terms (i.e., will contain no null pointers).
Furthermore, this procedure is guaranteed not to fail. The
corresponding information is also highlighted in the tool-tip (in
yellow).

In Fig.~\ref{fig:qsortdl-verified} 
we show
an implementation of quick-sort using open-ended (``difference'') lists to construct the output
lists (i.e., using pointers to append in constant time). 

\begin{figure}[t]
  \centering
  \vspace*{-3mm}
  \fbox{\includegraphics[width=0.75\textwidth,clip,trim=1 25 38 2]{incompatible_type}}
  \vspace*{-3mm}
  \caption{A property incompatibility bug detected statically.}\label{fig:simplebug}
  \vspace*{-3mm}
\end{figure}

\begin{figure}[t]
  \begin{tabular}{cc}
    \begin{subfigure}[a]{0.5\linewidth}
      \includegraphics[width=1\textwidth,clip,trim=1 0 20 2]{builtin_violation}
      \vspace*{-3mm}
      \vspace*{-3mm}
      \vspace*{-3mm}
      \caption{Static detection of illegal call to lib 
        predicate.
        \vspace*{-3mm}
      }\label{fig:builtin}
    \end{subfigure}
    &
      \begin{subfigure}[a]{0.5\linewidth}
        \includegraphics[width=1\textwidth,clip,trim=1 0 25 0]{always_fails}
        \vspace*{-3mm}
        \vspace*{-3mm}
        \caption{Static detection of simple non-termination.}\label{fig:does-not-succeed}
      \end{subfigure}
  \end{tabular}
      \vspace*{-3mm}
  \caption{Detection of errors at program points.}
  \vspace*{-3mm}
\end{figure}

\begin{figure}[t]
  \centering
  \fbox{\includegraphics[width=1.0\textwidth,clip,trim=1 0 0 0]{revf-bug}}
  \vspace*{-3mm}
  \vspace*{-3mm}
  \caption{Static verification of determinacy, termination, and cost (errors detected).}\label{fig:cost-errors}
  \vspace*{-3mm}
\end{figure}

\begin{figure}[b]
  \centering
  \fbox{\includegraphics[width=1.0\textwidth,clip,trim=1 0 25 0]{revf-verified}}
   \vspace*{-3mm}
   \vspace*{-3mm}
  \caption{Static verification of determinacy, termination, and cost (verified).}\label{fig:cost-verified}
   \vspace*{-3mm}
   \vspace*{-3mm}
\end{figure}

Examples~\ref{fig:simplebug},~\ref{fig:builtin},
and~\ref{fig:does-not-succeed} show static detection of, respectively,
a property incompatibility bug (note that the concrete property
\texttt{sorted/1} is approximated by the regtypes domain as
\texttt{list/1} and an incompatibility is found with \texttt{rt0},
i.e., \texttt{red}), an illegal call to a library predicate, and
a simple non-termination.

Fig.~\ref{fig:cost-errors} shows again the naive reverse
example of Fig.~\ref{fig:nrevf}, modified to 
illustrate the detection of an error
regarding unintended behavior w.r.t.\ cost.  The assertion in lines 5
and 6 of Fig.~\ref{fig:cost-errors} (left) states that predicate
\texttt{nrev} should be linear in the length of the (input) argument
\texttt{A}. This is expressed by the property
\texttt{steps\_o(length(A))}, meaning that the cost, in terms of
resolution steps, of any call to \texttt{nrev(A, B)} with \texttt{A}
bound to a list and \texttt{B} a free variable, is in
$O($\texttt{length(A)}$)$.  However, this worst case asymptotic
complexity stated in the user-provided assertion is incompatible with
a safe, quadratic lower bound on the cost of such calls ($ \frac{1}{2}
\ length{(A)}^2 + \frac{3}{2} \ length(A) + 1$) inferred by the static
analyzer. In contrast, assertion in lines 5 and 6 of
Fig.~\ref{fig:cost-verified} (left) states that predicate
\texttt{nrev} should have a quadratic worst case asymptotic complexity
in the length of \texttt{A}, which is proved to hold by means of the
upper-bound cost function inferred by analysis (which coincides with
the lower bound above). Fig.~\ref{fig:cost-verified} also shows the
verification of determinacy, non-failure, and termination properties.


\vspace*{-2mm}
\section{Some Performance Results}\label{sec:results}
\vspace*{-2mm}

\newcommand{\texttt{pairSh}}{\texttt{pairSh}}
\newcommand{\texttt{def}}{\texttt{def}}
\newcommand{\texttt{ShGrC}}{\texttt{ShGrC}}

\begin{table}[t]
  \caption{Average response time (seconds) for the experiments with
    any program edit.}\label{tab:exp-any}
    \vspace*{-3mm}
  \begin{minipage}{\textwidth}
    \begin{tabular}{rrrcrrcrrc}
      \toprule
      & \multicolumn{3}{c}{\texttt{aggreg}} & \multicolumn{3}{c}{\texttt{readin}} & \multicolumn{3}{c}{\texttt{talkr}} \\
      \cmidrule(lr){2-4} \cmidrule(lr){5-7} \cmidrule(lr){8-10}
      domain & \textit{noinc} & \textit{inc} & \textit{speedup} & \textit{noinc} & \textit{inc} & \textit{speedup}  & \textit{noinc} & \textit{inc} & \textit{speedup} \\
      \midrule
      \texttt{pairSh} & 2.8 & 1.6 & $\times 1.8$ & 2.9 & 1.5 & $\times 1.9$ & 2.8 & 1.6 & $\times 1.8$ \\
      \texttt{def} &  3.0 & 1.6 & $\times 1.9$ & 2.7 & 1.5 & $\times 1.8$ & 2.9 & 1.7 & $\times 1.7$ \\ 
      \texttt{ShGrC} & 18.1 & 5.1 & $\mathbf{\times 3.5}$ & 18.3 & 5.1 & $\mathbf{\times 3.6}$ & 18.1 & 4.5 & $\mathbf{\times 4.0}$ \\
      \bottomrule
    \end{tabular}
  \end{minipage}
  \caption{Average response time (seconds) for the experiments only
    changing assertions.}\label{tab:exp-assertions}
  \begin{minipage}{\textwidth}
    \begin{tabular}{rccccccccc}
      \toprule
      & \multicolumn{3}{c}{\texttt{aggreg}} & \multicolumn{3}{c}{\texttt{readin}} & \multicolumn{3}{c}{\texttt{talkr}} \\
      \cmidrule(lr){2-4} \cmidrule(lr){5-7} \cmidrule(lr){8-10}
      domain & \textit{noinc} & \textit{inc} & \textit{speedup} & \textit{noinc} & \textit{inc} & \textit{speedup}  & \textit{noinc} & \textit{inc} & \textit{speedup} \\
      \midrule
      \texttt{pairSh} & 2.8 & 1.7 & $\times 1.6$ &  2.7 & 1.6 & $\times 1.7$ & 2.9 & 1.7 & $\times 1.7$ \\
      \texttt{def}   & 3.1 & 1.5 & $\times 2.0$ &  2.9 & 1.4 & $\times 2.0$ & 3.0 & 1.6 & $\times 1.9$ \\
      \texttt{ShGrC}  & 18.2 & 2.0 & $\mathbf{\times 9.1}$ &  18.1 & 1.9 & $\mathbf{\times 9.6}$ & 18.2 & 1.9 & $\mathbf{\times 9.6}$ \\
      \bottomrule
    \end{tabular}
  \end{minipage}
  \vspace*{-3mm}
\end{table}


We provide some performance results
from our tool using 
the well-known \texttt{chat-80}
program
(\url{https://github.com/ciao-lang/chat80})
which contains $5.2$k
lines of Prolog code across 27 files, and uses a number of system
libraries containing different Prolog built-ins and library predicates. 
The experiments consisted in
opening a specific module in the IDE, and activating the checking of assertions
with global analysis, i.e., analyzing the whole application as well as
the libraries, and then
performing a series of small edits, observing the total response time,
i.e., the time from edit to graphical update of assertion coloring in the IDE. 
Concretely, we performed two kinds of edits, predicate and assertions
(\textbf{E1}), and only assertions (\textbf{E2}). The edits were
performed on 
three selected files: \texttt{aggreg}, \texttt{readin}, and \texttt{talkr}.
To study whether incrementality improves response times significantly, we
included experiments enabling and disabling it. The experiments were performed
using {\sf Ciao}\xspace 1.20 on a MacBook Air with the Apple M1 chip and 16 GB of RAM.\@
We evaluated the tool with three well-known abstract domains: a classic pair
sharing~\cite{MarriottSondergaard93} (\texttt{pairSh}), a dependency tracking
via propositional clauses domain~\cite{free-def-comb-short} (\texttt{def}), and
sharing+groundness with clique-based widening~\cite{shcliques-padl06-shorter} (\texttt{ShGrC}).
The latter is the most precise, and, hence, the most expensive.
We used sharing/groundness domains because they are known to be costly
and at the same time, beyond mode inference, 
necessary to ensure correctness of most other analyses in (C)LP
systems that support logical variables, and furthermore in any
language that has pointers (aliasing).

Tables~\ref{tab:exp-any} and~\ref{tab:exp-assertions} show the response times of
analyzing and checking assertions in experiments \textbf{E1} and \textbf{E2} respectively. For
each of the files that were modified the table shows three columns:
\textit{noinc} is the response time in the non-incremental analysis setting,
\textit{inc} is the response time in the incremental setting, and
\textit{speedup} is the speedup of \textit{inc} vs.\ \textit{noinc}. Each of
the rows in the table correspond to each of the abstract domains. The reported
time is the average of \emph{total} roundtrip assertion checking time,
\emph{measured from the IDE}, that is, what the programmer actually perceives.

In all of the experiments incrementality provides significant
speedups.
In the first experiment, \textbf{E1} (Table~\ref{tab:exp-any}), for the \texttt{pairSh}\ and
\texttt{def}\ domains, it allows keeping the response time, crucial for the
interactive use case of the analyzer that we propose, under 2~s.
For \texttt{ShGrC}, a significant speedup is also achieved (more than $\times
3.5$). The response time is borderline at $5~s$. 
The reason for this is, as mentioned, that the domain is more precise,
an thus more computationally expensive, which in fact allows
(dis)proving more assertions.
For the \textbf{E2} experiment (Table~\ref{tab:exp-assertions}), the tool detects that
no changes are required in the analysis results, and the assertions can be
rechecked w.r.t.\ the available (previous) analysis. The performance analyzing
with \texttt{ShGrC}\ is improved significantly (more than $\times 9$) but, more
importantly, the response times are around $2~s$.
All in all, the incremental features allow using many domains and, at
least in some cases, even the most expensive domains.

Note that the experiments reveal also that an interesting
configuration of this tool is to run different analyses in a
portfolio, where which analyses to run is decided depending on the
kind of change occurred.
If only assertions have changed, it is enough to recheck only with
\texttt{ShGrC}.  However if both the code and the assertions changed,
analysis for all domains can be run in parallel giving fast, less
precise feedback to the programmer as the results are available, and
then refine the results when the more precise results are ready.

Aside from the data in the tables, we observed a constant overhead of
$0.4$~s for loading the code---parsing and prior transformations---in the
tool.
This is currently still not fully incremental and has not been
optimized yet to load only the parts that change.
Verification times are negligible w.r.t.\ analysis times and are
approx.\ $0.1$~s; this is also non incremental, since we found that it
is not currently a bottleneck, although we plan to make it incremental
in the future to push the limits of optimizations forward.

\vspace*{-2mm}
\section{Related Work}\label{sec:related}
\vspace*{-2mm}

The topic of assertion checking in logic programming, and in Prolog in
particular, has received considerable attention. A family of
approaches involves defining static type systems for logic
programs~\cite{mycroft84:type_system_prolog,LakshmanReddy91,Pfenning92TILP} 
and several strongly-typed logic programming systems have been
proposed, notable examples being Mercury~\cite{mercury-jlp-short} and
G{\"o}del~\cite{goedel-short}. Approaches for combining strongly typed
and untyped Prolog modules were proposed
in~\cite{schrijvers08:typed_prolog-short}.
Most of these approaches impose a number of restrictions
that make them less appropriate for dynamic languages like Prolog.
The {\sf Ciao}\xspace model introduced an alternative for writing safe programs
without relying on full static typing, but based instead the notions
of safe approximations and abstract interpretation, providing a more
general and flexible approach than in previous work, since assertions
are optional and can contain any abstract property.  This approach is
specially useful for dynamic languages
---see,
e.g.,~\citeauthor{hermenegildo11:ciao-stop-short}~(\citeyear{hermenegildo11:ciao-stop-short})
for a discussion of this topic.
Some aspects of the {\sf Ciao}\xspace model have been adopted or applied in other
recent Prolog-based approaches, such as,
e.g.,~\citeauthor{schrijvers08:typed_prolog-short}~(\citeyear{schrijvers08:typed_prolog-short}),~\citeauthor{koerner-types-prolog-wflp20-shorter}~(\citeyear{koerner-types-prolog-wflp20-shorter})
or the library for run-time checking of assertions in SWI-Prolog.
It can be considered an antecedent of the now popular
\emph{gradual-} and \emph{hybrid-typing}
approaches~\cite{DBLP:conf/popl/Flanagan06-hybrid-type-checking-shortest,Siek06gradualtyping,DBLP:conf/popl/RastogiSFBV15-short}.
Moreover, recent
work~\cite{optchk-journal-scp-short,termhide-padl2018-short}
illustrates further that these techniques and the exploitation of
local data invariants allows maintaining strong safety guarantees
with zero or very low (and potentially
guaranteed~\cite{rtchecks-cost-2018-ppdp-short}) run-time check
overheads, even in a reusable-library context, without requiring
switching to strong typing. 
This approach is also more natural in Prolog-style languages that
distinguish between erroneous and failed (backtracking) executions.
All these techniques taken together strongly suggest that using the
Ciao approach comparable safety guarantees to those of strong typing
can be achieved without its requirements.
There has been work on incrementality within theorem
proving-based verification approaches, such as,
e.g.,~\citeauthor{leino-caching-verification-2015-short}~\citeyear{leino-caching-verification-2015-short}
and~\citeauthor{tschannen-oop-verification-11-short}~\citeyear{leino-caching-verification-2015-short}.
Additional references can be found in the {\sf CiaoPP}\xspace overview papers and
the other citations provided.

\vspace*{-2mm}
\section{Conclusions}\label{sec:conclude}
\vspace*{-2mm}

We have shown how a combination of the {\sf CiaoPP}\xspace static analysis and
verification framework within an integrated development environment
(IDE), can take advantage of 
incrementality 
to achieve a high level of reactivity
when reflecting analysis and verification results back as colorings
and tooltips directly on the program text. We have termed this mode of
operation ``{\sf VeriFly}\xspace mode.''
Our initial experience with this integrated tool shows quite promising
results, with low latency times that provide early, continuous, and
precise ``on-the-fly'' 
semantic feedback to programmers during the development process.
This allows detecting many types of errors
including swapped variables, property incompatibilities, illegal calls
to library predicates, violated numeric constraints, unintended
behavior w.r.t.\ termination, resource usage, determinism, covering
and failure,
etc.
While 
presented using the Emacs and the {\sf flycheck}\xspace package, we argue that
our 
techniques and results should be applicable to any {\sf VeriFly}\xspace-style
integration into a modern extensible IDE.\@
We plan to continue our work 
to achieve further reactivity and scalability improvements, enhanced
presentations of verification results, and improved diagnosis,
contributing to further improve the programming environments
available to the (C)LP programmer.

\vspace*{-2mm}

\bibliographystyle{acmtrans}
\small 
