Merge remote-tracking branch 'tl228638/alias-merce/merge4' into jan/alias

src/plugins/alias/.gitattributes

+################
+# MERGE: union #
+################
+
+Changelog merge=union
+
+##################################################
+# BINARY/CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
+##################################################
+
+# note: "binary" is a built-in macro that also
+#       unsets the "text" and "diff" attributes
+
+# note: set "check-eoleof" and "check-utf8" by default to all files
+* check-eoleof check-utf8
+
+# note: unset "-check-eoleof" and "-check-utf8" for "binary"
+*.jpg binary -check-eoleof -check-utf8
+*.pdf binary -check-eoleof -check-utf8
+
+###########################################
+# CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
+###########################################
+
+*.ml  check-syntax check-indent -check-eoleof
+*.mli check-syntax check-indent -check-eoleof
+
+################################
+# HEADER_SPEC: LICENSE.Alias #
+################################
+
+dune-project header_spec=LICENSE.Alias
+dune header_spec=LICENSE.Alias
+dune-workspace header_spec=LICENSE.Alias
+
+Make* header_spec=LICENSE.Alias
+
+*.ml header_spec=LICENSE.Alias
+*.mli header_spec=LICENSE.Alias
+
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+# CI
+
+/.gitlab-ci.yml header_spec=.ignore
+/nix/ci.sh  header_spec=.ignore
+/nix/*.nix header_spec=.ignore
+
+# Doc
+
+/Changelog header_spec=.ignore
+README* header_spec=.ignore
+
+# Git
+
+.gitattributes header_spec=.ignore
+.gitignore header_spec=.ignore
+.gitkeep header_spec=.ignore
+.git-blame-ignore-revs header_spec=.ignore
+
+# Headers
+
+/LICENSE.Alias header_spec=.ignore
+/headers/open-source/* header_spec=.ignore
+/headers/close-source/* header_spec=.ignore
+
+# OCaml
+
+/*.opam* header_spec=.ignore
+/.ocp-indent header_spec=.ignore
+
+#Tests
+
+/tests/**/* header_spec=.ignore

src/plugins/alias/.gitignore

+/_build
+tests/**/result
+tests/*/oracle/dune

src/plugins/alias/.gitlab-ci.yml

+################################################################################
+### STAGES
+
+stages:
+  - tests
+
+################################################################################
+### DEFAULT JOB PARAMETERS
+
+default:
+  tags: [nix-v2]
+
+################################################################################
+### VARIABLES
+
+variables:
+  DEFAULT: "master"
+  OCAML: "4.11"
+
+################################################################################
+### TESTS
+
+build-and-test:
+  stage: tests
+  script:
+    - ./nix/ci.sh
+
+check-headers:
+  stage: tests
+  variables:
+    CI_MODE: "check-headers"
+  script:
+    - ./nix/ci.sh
+
+lint:
+  stage: tests
+  variables:
+    CI_MODE: "lint"
+  script:
+    - ./nix/ci.sh

src/plugins/alias/.ocp-indent

+normal

src/plugins/alias/API.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in 'Alias' (alias).             *)
+(*                                                                        *)
+(*  Copyright (C) 2022-2023                                               *)
+(*    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 LICENSE)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+open Simplified
+
+(** Points-to graphs datastructure. *)
+module G = Abstract_state.G
+
+module LSet = Simplified_lset
+
+module Abstract_state = Abstract_state
+
+let check_computed () =
+  if not (Analysis.is_computed ())
+  then
+    Options.abort "Static analysis must be called before any function of the API can be called"
+
+
+let fold_aliases_stmt (f_fold : 'a -> lval -> 'a) (acc: 'a) (kf: kernel_function)  (s:stmt) (lv: lval) : 'a =
+  check_computed ();
+  match Analysis.get_state_before_stmt kf s with
+    None -> acc
+  | Some state ->
+    let set_aliases = Abstract_state.find_all_aliases lv state in
+    LSet.fold_lval (fun e a -> f_fold a e) set_aliases acc
+
+let fold_new_aliases_stmt (f_fold: 'a -> lval -> 'a) (acc: 'a) (kf:kernel_function) (s:stmt) (lv:lval) : 'a =
+  check_computed ();
+  match Analysis.get_state_before_stmt kf s with
+    None -> acc
+  | Some state ->
+    let new_state = Analysis.do_stmt state s in
+    let set_aliases = Abstract_state.find_all_aliases lv new_state in
+    LSet.fold_lval (fun e a -> f_fold a e) set_aliases acc
+
+let fold_aliases_kf (f_fold: 'a -> lval -> 'a) (acc: 'a) (kf:kernel_function) (lv:lval) : 'a =
+  check_computed ();
+  if Kernel_function.has_definition kf
+  then
+    let s = Kernel_function.find_return kf in
+    fold_new_aliases_stmt f_fold acc kf s lv
+  else
+    Options.abort "fold_aliases_kf: function %a has no definition" Kernel_function.pretty kf
+
+let fold_fundec_stmts (f_fold: 'a -> stmt -> lval -> 'a) (acc: 'a) (kf:kernel_function) (lv:lval) : 'a =
+  check_computed ();
+  if Kernel_function.has_definition kf
+  then
+    let f_dec = Kernel_function.get_definition kf in
+    let list_stmt = f_dec.sallstmts in
+    List.fold_left
+      (fun acc s ->
+         fold_new_aliases_stmt
+           (fun a lv -> f_fold a s lv)
+           acc
+           kf
+           s
+           lv
+      )
+      acc
+      list_stmt
+  else
+    Options.abort "fold_fundec_stmts: function %a has no definition" Kernel_function.pretty kf
+
+let are_aliased (kf: kernel_function) (s:stmt) (lv1: lval) (lv2:lval) : bool =
+  check_computed ();
+  match Analysis.get_state_before_stmt kf s with
+    None -> false
+  | Some state ->
+    let setv1 = Abstract_state.find_all_aliases lv1 state in
+    LSet.mem (BLval lv2) setv1
+
+let fold_vertex   (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (kf: kernel_function)  (s:stmt) (lv: lval) : 'a =
+  check_computed ();
+  match Analysis.get_state_before_stmt kf s with
+    None -> acc
+  | Some state ->
+    let v : G.V.t = Abstract_state.find_vertex lv state in
+    let set_aliases = Abstract_state.find_aliases lv state in
+    LSet.fold_lval (fun lv a-> f_fold a v lv) set_aliases acc
+
+let fold_vertex_closure  (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (kf: kernel_function)  (s:stmt) (lv: lval) : 'a =
+  check_computed ();
+  match Analysis.get_state_before_stmt kf s with
+    None -> acc
+  | Some state ->
+    let list_closure : (G.V.t * LSet.t) list = Abstract_state.find_transitive_closure lv state in
+    List.fold_left
+      (fun acc (i,s) -> LSet.fold_lval (fun lv a -> f_fold a i lv) s acc)
+      acc
+      list_closure
+
+let get_state_before_stmt =
+  Analysis.get_state_before_stmt
+
+let call_function a f res args =
+  match Analysis.get_summary f with
+    None -> None
+  | Some su -> Some(Abstract_state.call a res args su)
+
+
+let simplify_lval (lv:lval) : lval =
+  match Simplified.Simplified_lval.from_lval lv with
+    BLval lv -> lv
+  | _ -> Options.fatal "This should not happen"

src/plugins/alias/API.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in 'Alias' (alias).             *)
+(*                                                                        *)
+(*  Copyright (C) 2022-2023                                               *)
+(*    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 LICENSE)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** External API of the plugin Alias *)
+
+open Cil_types
+
+(** Points-to graphs datastructure. *)
+module G: Graph.Sig.G
+
+(** NB : do the analysis BEFORE using any of those functions *)
+
+(* previously get_class_before_statement *)
+(** [fold_aliases_stmt f acc kf s lv] folds [f acc] over all the aliases of the
+    given lval [lv] right before stmt [s] in function [kf]. *)
+val fold_aliases_stmt:
+  ('a -> lval -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
+
+(* previously get_class_after_statment *)
+(** [fold_new_aliases_stmt f acc kf s lv] folds [f acc] over all the aliases of
+    the given lval [lv] created by stmt [s] in function [kf]. *)
+val fold_new_aliases_stmt:
+  ('a -> lval -> 'a) -> 'a -> kernel_function -> stmt -> lval -> 'a
+
+(* previously get_class_fundec *)
+(** [fold_aliases_kf f acc kf lv] folds [f acc] over all the aliases of lval
+    [lv] at the end of function [kf]. *)
+val fold_aliases_kf:
+  ('a -> lval -> 'a) -> 'a -> kernel_function -> lval -> 'a
+
+(** [fold_fundec_stmts f acc kf v] folds [f acc s e] on the list of
+    pairs [s, e] where [e] is the set of lval aliased to [v] after statement [s]
+    in function [kf]. *)
+val fold_fundec_stmts:
+  ('a -> stmt -> lval -> 'a) -> 'a -> kernel_function -> lval -> 'a
+
+(** [are_aliased kf s lv1 lv2] returns true if and only if the two
+    lvals [lv1] and [lv2] are aliased before stmt [s] in function
+    [kf]. *)
+val are_aliased: kernel_function -> stmt -> lval -> lval -> bool
+
+(** [fold_vertex f acc kf s v] folds [f acc i lv] to all [lv] in [i], where [i] is
+    the vertex that represents the equivalence class of [v] before statement [s] in function [kf]. *)
+val fold_vertex:
+  ('a -> G.V.t -> lval -> 'a) -> 'a  -> kernel_function -> stmt -> lval  -> 'a
+
+(** [fold_vertex_closure f acc kf s v] is the transitive closure of function
+    [fold_vertex]. *)
+val fold_vertex_closure:
+  ('a -> G.V.t -> lval -> 'a) -> 'a  -> kernel_function -> stmt -> lval  -> 'a
+
+
+(** direct access to the abstract state. See Abstract_state.mli *)
+
+module Abstract_state : Abstract_state.S
+
+(** [get_state_before_stmt f s] gets the abstract state computed after
+    statement [s] in function [f]. Returns [None] if
+    the abstract state is bottom or not computed. *)
+val get_state_before_stmt :  kernel_function -> stmt -> Abstract_state.t option
+
+
+(** [call_function a f Some(res) args] computes the abstract state
+    after the instruction res=f(args) where res is a lval. [a] is the
+    abstract state before the call. If function [f] returns no value,
+    use [call_function a f None args] instead. Returns [None] if
+    the abstract state [a] is bottom or not computed. *)
+val call_function: Abstract_state.t -> kernel_function -> lval option -> exp list -> Abstract_state.t option
+
+
+(** [simplify_lval lv] returns a lval where every index of an array is
+    replaced by 0, evey pointer arithmetic is simplified to an access
+    to an array *)
+val simplify_lval: lval -> lval

src/plugins/alias/Alias.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in 'Alias' (alias).             *)
+(*                                                                        *)
+(*  Copyright (C) 2022-2023                                               *)
+(*    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 LICENSE)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+module Analysis = Analysis
+
+module API = API
+
+let main () =
+  if Options.Enabled.get() then
+    begin
+      Analysis.compute ();
+      Options.debug "Analysis complete";
+    end
+
+let () =
+  Db.Main.extend main

src/plugins/alias/Alias.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in 'Alias' (alias).             *)
+(*                                                                        *)
+(*  Copyright (C) 2022-2023                                               *)
+(*    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 LICENSE)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Interface for the Alias plug-in. *)
+
+module Analysis: sig
+  (** see file analysis.mli for documentation *)
+  val compute : unit -> unit
+  val clear : unit -> unit
+end
+
+
+module API = API

src/plugins/alias/LICENSE.Alias

+
+This file is part of the Frama-C plug-in 'Alias' (alias).
+
+Copyright (C) 2022-2023
+  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 LICENSE)
+

src/plugins/alias/Makefile

+##########################################################################
+#                                                                        #
+#  This file is part of the Frama-C plug-in 'Alias' (alias).             #
+#                                                                        #
+#  Copyright (C) 2022-2023                                               #
+#    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 LICENSE)                       #
+#                                                                        #
+##########################################################################
+
+.PHONY: all build-profiling build clean
+
+FRAMAC_SHARE:=$(shell frama-c -print-share-path)
+
+sinclude ${FRAMAC_SHARE}/Makefile.common
+
+##########################################################################
+# Build
+
+all:: build frama-c-alias.opam
+
+frama-c-alias.opam: frama-c-alias.opam.template dune-project
+	rm -f $@
+	dune build $@
+
+build::
+	dune build @install
+
+build-profiling::
+	dune build --instrument-with landmarks @install
+
+clean:: purge-tests
+	dune clean
+	rm -rf _build .merlin
+
+##########################################################################
+# Tests
+
+include ${FRAMAC_SHARE}/Makefile.testing
+
+##########################################################################
+# Install
+
+include ${FRAMAC_SHARE}/Makefile.installation
+
+##########################################################################
+# Headers
+
+HDRCK_EXTRA:=-headache-config-file ${FRAMAC_SHARE}/headache_config.txt
+include ${FRAMAC_SHARE}/Makefile.headers
+
+SHORT_NAME:=alias
+LONG_NAME:=Alias
+PLUGIN_NAME:=Alias
+FROM_YEAR:=2022
+
+include headers/Makefile.generate-headers
+
+##########################################################################
+# Linting
+
+include ${FRAMAC_SHARE}/Makefile.linting
+
+##########################################################################

src/plugins/alias/README.md

+# MERCE
+
+GIT project for our collaboration with MERCE
+
+
+## Project Members
+
+Allan Blanchard
+Loïc Correnson
+Tristan Le Gall
+Jan Rochel
+Julien Signoles
+
+## Building
+
+This plug-in requires the library 'unionFind' that can be installed as follows:
+  opam install unionFind
+
+To build with profiling install the package landmarks-ppx and run:
+  dune build --instrument-with landmarks
+
+Using the plugin will then echo profiling information to stderr.

src/plugins/alias/abstract_state.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in 'Alias' (alias).             *)
+(*                                                                        *)
+(*  Copyright (C) 2022-2023                                               *)
+(*    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 LICENSE)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Module abstract_state *)
+
+open Cil_types
+
+(** Points-to graphs datastructure. *)
+module G: Graph.Sig.G
+
+(** NB : type Lval.t is not the same as type lval !! *)
+module LSet = Simplified.Simplified_lset
+
+
+(** external signature *)
+module type S =
+sig
+
+  (** Type denothing an abstract state of the analysis. It is a graph containing
+      all aliases and points-to information. *)
+  type t
+
+  (** access to the points-to graph *)
+  val get_graph: t -> G.t
+
+  (** set of lvals stored in a vertex *)
+  val get_lval_set : G.V.t -> t -> LSet.t
+
+  (** pretty printer; debug=true prints the graph, debug = false only
+      prints aliased variables *)
+  val pretty : ?debug:bool -> Format.formatter -> t -> unit
+
+  (** dot printer; first argument is a file name *)
+  val print_dot : string -> t -> unit
+
+  (** finds the vertex corresponding to a lval. May raise @Not_found
+  *)
+  val find_vertex : lval -> t -> G.V.t
+
+  (** same as previous function, but return a set of lval. Cannot
+      raise an exception but may return an empty set if the lval is not
+      in the graph *)
+  val find_aliases : lval -> t -> LSet.t
+
+  (** similar to the previous functions, but does not only give the
+      equivalence class of lv, but also all lv that are aliases in
+      other vertex of the graph *)
+  val find_all_aliases : lval -> t -> LSet.t
+
+  (** find_aliases, then recursively finds other sets of lvals. We
+      have the property (if lval [lv] is in abstract state [x]) :
+      List.hd (find_transitive_closure lv x) = (find_vertex lv x,
+      find_aliases lv x) *)
+  val find_transitive_closure : lval -> t -> (G.V.t * LSet.t) list
+
+  (** inclusion test; [is_included a1 a2] tests if, for any lvl
+      present in a1 (associated to a vertex v1), that it is also
+      present in a2 (associated to a vertex v2) and that
+      get_lval_set(succ(v1) is included in get_lval_set(succ(v2)) *)
+  val is_included : t -> t -> bool
+
+end
+
+
+include S
+
+(** check all the invariants that must be true on an abstract value
+      before and after each function call or transformation of the graph)  *)
+val assert_invariants : t -> unit
+
+(** Functions for Steensgaard's algorithm, see the paper *)
+val join : t -> G.V.t -> G.V.t -> t
+
+(** transfert functions for different kinds of assignments *)
+val assignment : t -> lval -> exp -> t
+
+(** transfert function for malloc calls *)
+val assignment_x_allocate_y : t -> lval -> t
+
+
+(** inclusion test; [is_included a1 a2] tests if, for any lvl present
+    in a1 (associated to a vertex v1), that it is also present in a2
+    (associated to a vertex v2) and that set(succ(v1) is included in
+    set(succ(v2)) *)
+val is_included : t -> t -> bool
+
+(** union of two abstract values ; ensures that if 2 lval are
+    aliased in one of the two input graph (or in a points-to
+    relationship), then they will also be aliased/points-to in the
+    result *)
+val union : t -> t -> t
+
+(** empty graph *)
+val empty : t
+
+(** Type denoting summaries of functions *)
+type summary
+
+(** creates a summary from a state and a function *)
+val make_summary : t -> kernel_function -> summary
+
+(** pretty printer *)
+val pretty_summary :  ?debug:bool -> Format.formatter -> summary -> unit
+
+(** [call a res args s] computes the abstract state after the
+    instruction res=f(args), with f summarized by [s]. [a] is the abstract state before the call *)
+val call: t -> lval option -> exp list -> summary -> t

src/plugins/alias/analysis.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in 'Alias' (alias).             *)
+(*                                                                        *)
+(*  Copyright (C) 2022-2023                                               *)
+(*    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 LICENSE)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+module Dataflow = Dataflow2
+
+module type Table = sig
+  type key
+  type value
+  val find: key -> value
+  (** @raise Not_found if the key is not in the table. *)
+end
+
+module type InternalTable = sig
+  include Table
+  val add : key -> value -> unit
+  val iter : (key -> value -> unit) -> unit
+end
+
+module Make_table (H: Hashtbl.S) (V: sig type t val size : int end)
+  : InternalTable with type key = H.key and type value = V.t = struct
+  type key = H.key
+  type value = V.t
+  let tbl = H.create V.size
+  let add = H.replace tbl
+  let find = H.find tbl
+  let iter f = H.iter f tbl
+end
+
+(* In Function_table, value None means the function has no definition *)
+module Function_table = Make_table (Kernel_function.Hashtbl) (struct
+    type t = Abstract_state.summary option
+    let size = 7
+  end)
+
+let function_compute_ref = Extlib.mk_fun "function_compute"
+
+(* In Stmt_table, value None means abstract state = Bottom *)
+module Stmt_table = struct
+  include Dataflow.StartData (struct
+      type t = Abstract_state.t option
+      let size = 7
+    end)
+  type key = stmt
+  type value = data
+end
+
+let warn_unsupported_explicit_pointer pp_obj obj loc =
+  Options.warning ~source:(fst loc) ~wkey:Options.Warn.unsupported_address
+    "unsupported feature: explicit pointer address: %a; analysis may be unsound" pp_obj obj
+
+let do_assignment (lv:lval) (exp:exp) (a:Abstract_state.t) : Abstract_state.t =
+  try Abstract_state.assignment a lv exp
+  with Simplified.Explicit_pointer_address loc ->
+    warn_unsupported_explicit_pointer  Printer.pp_exp exp loc;
+    a
+
+let rec do_init (lv:lval) (init:init) state =
+  match init with
+  | SingleInit e -> Option.map (do_assignment lv e) state
+  | CompoundInit (_, l) ->
+    List.fold_left (fun state (o, init) -> do_init (Cil.addOffsetLval o lv) init state) state l
+
+let doFunction f = !function_compute_ref f
+
+let do_function_call (stmt:stmt) state (res : lval option) (ef : exp) (args: exp list) loc =
+  let is_malloc (s:string) : bool =
+    (s = "malloc") || (s = "calloc") (* todo : add all function names *)
+  in
+  match ef with
+  | {enode=Lval (Var v, _);_}  when is_malloc v.vname ->
+    begin
+      (* special case for malloc *)
+      match (state,res) with
+        (None, _) -> None
+      | (Some a, None) -> (Options.warning "Memory allocation not stored (ignored)"; Some a)
+      | (Some a, Some lv) ->
+        try Some (Abstract_state.assignment_x_allocate_y a lv)
+        with Simplified.Explicit_pointer_address loc ->
+          warn_unsupported_explicit_pointer Printer.pp_stmt stmt loc;
+          Some a
+    end
+  | _ ->
+    begin
+      (* general case *)
+      let summary =
+        match Kernel_function.get_called ef with
+        | Some kf when Kernel_function.is_main kf -> None
+        | Some kf -> begin
+            try Function_table.find kf
+            with Not_found -> doFunction kf
+          end
+        | None ->
+          Options.warning ~wkey:Options.Warn.unsupported_function ~source:(fst loc)
+            "unsupported feature: call to function pointer: %a" Exp.pretty ef;
+          None
+      in
+      match (state, summary) with
+        (None, _) -> None
+      | (Some a, Some summary) ->
+        Some (Abstract_state.call a res args summary)
+      | (Some a, None) ->
+        Options.warning ~wkey:Options.Warn.undefined_function ~once:true ~source:(fst loc)
+          "function %a has no definition" Exp.pretty ef;
+        Some a
+    end
+
+let do_cons_init (s:stmt) (v:varinfo) f arg t loc state =
+  Cil.treat_constructor_as_func (do_function_call s state) v f arg t loc
+
+let analyse_instr (s:stmt)  (i:instr) (a:Abstract_state.t option) : Abstract_state.t option =
+  match i with
+    Set (lv,exp,_) -> Option.map (do_assignment lv exp) a
+  | Local_init (v,AssignInit i,_) -> do_init (Var v, NoOffset) i a
+  | Local_init (v,ConsInit (f,arg,t),loc) -> do_cons_init s v f arg t loc a
+  | Code_annot _ -> a
+  | Skip _ -> a
+  | Call (res,ef,es,loc) -> (* !function_compute_ref ef *)
+    do_function_call s a res ef es loc
+  | Asm (_,_,_,loc) ->
+    Options.warning
+      ~source:(fst loc) ~wkey:Options.Warn.unsupported_asm
+      "unsupported feature: assembler code; skipping";
+    a
+
+let pp_abstract_state_opt ?(debug=false) fmt v =
+  match v with
+  | None -> Format.fprintf fmt "⊥"
+  | Some a -> Abstract_state.pretty ~debug fmt a
+
+let do_instr (s:stmt)  (i:instr) (a:Abstract_state.t option) : Abstract_state.t option =
+  Options.feedback ~level:3 "@[analysing instruction:@ %a@]" Printer.pp_stmt s;
+  let result = analyse_instr s i a in
+  Options.feedback ~level:3 "@[May-aliases after instruction@;<2>@[%a@]@;<2>are@;<2>@[%a@]@]"
+    Printer.pp_stmt s (pp_abstract_state_opt ~debug:false) result;
+  Options.debug ~level:3 "@[May-alias graph after instruction@;<2>@[%a@]@;<2>is@;<4>@[%a@]@]"
+    Printer.pp_stmt s (pp_abstract_state_opt ~debug:true) result;
+  result
+
+module T = struct
+  let name = "alias"
+
+  let debug = true (* TODO see options *)
+
+  type t = Abstract_state.t option
+
+  module StmtStartData = Stmt_table
+
+  let copy x = x (* we only have persistant data *)
+
+  let pretty fmt a =
+    match a with
+      None -> Format.fprintf fmt "<No abstract state>"
+    | Some a -> Abstract_state.pretty fmt a
+
+  let computeFirstPredecessor _ a = a
+
+  let combinePredecessors _stmt ~old state =
+    match old, state with
+    | _, None -> assert false
+    | None, Some _ -> Some state (* [old] already included in [state] *)
+    | Some old, Some new_ ->
+      if Abstract_state.is_included new_ old then
+        None
+      else
+        Some (Some (Abstract_state.union old new_))
+
+  let doInstr = do_instr
+
+  let doGuard _ _ a =
+    Dataflow.GUse a, Dataflow.GUse a
+
+  let doStmt _ _ = Dataflow.SDefault
+
+  let doEdge _ _ a = a
+end
+
+module F = Dataflow.Forwards (T)
+
+let do_stmt (a: Abstract_state.t) (s:stmt) :  Abstract_state.t =
+  match s.skind with
+    Instr i ->
+    begin
+      match do_instr s i (Some a) with
+        None -> Options.fatal "problem here"
+      | Some a -> a
+    end
+  | _ -> a
+
+let analyse_function (kf:kernel_function) =
+  Options.feedback ~level:2 "analysing function: %a" Kernel_function.pretty kf;
+  if Kernel_function.has_definition kf then
+    begin
+      let first_stmt =
+        try Kernel_function.find_first_stmt kf
+        with Kernel_function.No_Statement -> assert false
+      in
+      T.StmtStartData.add first_stmt (Some Abstract_state.empty);
+      F.compute [first_stmt];
+      let return_stmt = Kernel_function.find_return kf in
+      try Stmt_table.find return_stmt
+      with Not_found ->
+        begin
+          let source, _ = Kernel_function.get_location kf in
+          Options.warning ~source ~wkey:Options.Warn.no_return_stmt
+            "function %a does not return; analysis may be unsound"
+            Kernel_function.pretty kf;
+          Some Abstract_state.empty
+        end
+    end
+  else
+    None
+
+let doFunction (kf:kernel_function) =
+  let final_state = analyse_function kf in
+  let level = if Kernel_function.is_main kf then 1 else 2 in
+  Options.feedback ~level "@[May-aliases at the end of function %a:@ @[%a@]"
+    Kernel_function.pretty kf
+    (pp_abstract_state_opt ~debug:false) final_state;
+  Options.debug ~level "May-alias graph at the end of function %a:@;<4>@[%a@]"
+    Kernel_function.pretty kf
+    (pp_abstract_state_opt ~debug:true) final_state;
+  let result =
+    match final_state with
+    (* final state is None if kf has no definition *)
+      None -> None
+    | Some fs ->
+      let summary = Abstract_state.make_summary fs kf in
+      Options.debug ~level:2 "Summary of function %a:@ @[%a@]"
+        Kernel_function.pretty kf
+        (Abstract_state.pretty_summary ~debug:false) summary;
+      Some summary
+  in
+  if Kernel_function.is_main kf then
+    let f_name = Options.Dot_output.get () in
+    begin match f_name, final_state with
+      | "", _ -> ()
+      | _, None -> ()
+      | _, Some final_state -> Abstract_state.print_dot f_name final_state
+    end;
+    None
+  else
+    (Function_table.add kf result; result)
+
+let () = function_compute_ref := doFunction
+
+let make_summary (state:Abstract_state.t) (kf:kernel_function) =
+  try
+    begin
+      match Function_table.find kf with
+        Some s -> (state, s)
+      | None -> Options.fatal "not implemented"
+    end
+  with
+    Not_found ->
+    begin
+      match doFunction kf with
+        Some s -> (state, s)
+      | None -> Options.fatal "not implemented"
+    end
+
+let computed_flag = ref false
+
+let is_computed () = !computed_flag
+
+let print_stmt_table_elt fmt k v :unit =
+  let print_key = Stmt.pretty in
+  let print_value fmt v =
+    match v with
+    | None -> Format.fprintf fmt "<Bot>"
+    | Some a -> Abstract_state.pretty ~debug:(Options.DebugTable.get ()) fmt a
+  in
+  Format.fprintf fmt "Before statement %a :@[<hov 2> %a@]" print_key k print_value v
+
+let print_function_table_elt fmt kf s : unit =
+  let function_name = Kernel_function.get_name kf in
+  match s with
+  | None -> Options.debug "function %s -> None" function_name
+  | Some s ->
+    Format.fprintf fmt "Summary of function %s:@;<5 2>@[%a@]@."
+      function_name
+      (Abstract_state.pretty_summary ~debug:(Options.DebugTable.get ())) s
+
+let compute () =
+  Ast.compute ();
+  Globals.Functions.iter (fun kf -> ignore @@ doFunction kf);
+  computed_flag := true;
+  if Options.ShowStmtTable.get () then
+    Stmt_table.iter (print_stmt_table_elt Format.std_formatter);
+  if Options.ShowFunctionTable.get () then
+    Function_table.iter (print_function_table_elt Format.std_formatter)
+
+let clear () =
+  computed_flag := false;
+  Stmt_table.clear ()
+
+let get_state_before_stmt _kf stmt =
+  if is_computed ()
+  then
+    try Stmt_table.find stmt with
+      Not_found -> None
+  else
+    None
+
+let get_summary kf =
+  if is_computed ()
+  then
+    try Function_table.find kf with
+      Not_found -> None
+  else
+    None

src/plugins/alias/analysis.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in 'Alias' (alias).             *)
+(*                                                                        *)
+(*  Copyright (C) 2022-2023                                               *)
+(*    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 LICENSE)                       *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+open Abstract_state
+
+module type Table = sig
+  type key
+  type value
+  val find: key -> value
+  (** @raise Not_found if the key is not in the table. *)
+end
+
+(** Store the graph at each statement. *)
+module Stmt_table: Table with type key = stmt and type value = Abstract_state.t option
+
+
+(** Store the summary of each function. *)
+module Function_table:
+  Table with type key = kernel_function and type value = Abstract_state.summary option
+
+(** [do_stmt a s] computes the abstract state after statement s. This
+    function does NOT store the result in Stmt_table.  *)
+val do_stmt: t -> stmt -> t
+
+(** [make_summary a f] computes the summary of a function (and the
+    next abstract state if needed) and stores the summary in
+    [Function_table]. *)
+val make_summary: t -> kernel_function -> t * summary
+
+(** main analysis functions *)
+
+(** [compute ()] performs the may-alias analysis. It must be done once
+    before using functions defined in API.ml *)
+val compute : unit -> unit
+
+(** [is_computed ()] returns true iff an analysis was done previously *)
+val is_computed : unit -> bool
+
+(** [clear()] clears caches and imperative structures that are used by
+    the analysis. All accumulated data are lost. *)
+val clear : unit -> unit
+
+(** see API.mli *)
+val get_state_before_stmt :  kernel_function -> stmt -> Abstract_state.t option
+
+(** see API.mli *)
+val get_summary : kernel_function -> Abstract_state.summary option

src/plugins/alias/dune

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  This file is part of the Frama-C plug-in 'Alias' (alias).             ;;
+;;                                                                        ;;
+;;  Copyright (C) 2022-2023                                               ;;
+;;    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 LICENSE)                       ;;
+;;                                                                        ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+( rule
+  (alias frama-c-configure)
+  (deps (universe))
+  (action ( progn
+            (echo "Alias:" %{lib-available:frama-c-alias.core} "\n")
+            (echo " - Frama-C:" %{lib-available:frama-c.kernel} "\n")
+          )
+  )
+)
+
+( env
+  (release (flags -noassert))
+  (_ (flags (:standard -w @a-4)))
+)
+
+( library
+  (name Alias)
+  (public_name frama-c-alias.core)
+  (flags -open Frama_c_kernel :standard)
+  (libraries frama-c.kernel ocamlgraph unionFind)
+  (instrumentation (backend landmarks))
+)
+
+( plugin
+  (optional)
+  (name alias)
+  (libraries frama-c-alias.core)
+  (site (frama-c plugins))
+)

src/plugins/alias/dune-project

+(lang dune 3.2)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  This file is part of the Frama-C plug-in 'Alias' (alias).             ;;
+;;                                                                        ;;
+;;  Copyright (C) 2022-2023                                               ;;
+;;    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 LICENSE)                       ;;
+;;                                                                        ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+(using dune_site 0.1)
+(generate_opam_files true)
+
+(name frama-c-alias)
+
+(package (name frama-c-alias)
+ (depends
+  ("frama-c" (and (>= 25.0) (< 27.0)))
+  ("unionFind" (= 20220122))
+ )
+)

src/plugins/alias/dune-workspace

+(lang dune 3.2)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  This file is part of the Frama-C plug-in 'Alias' (alias).             ;;
+;;                                                                        ;;
+;;  Copyright (C) 2022-2023                                               ;;
+;;    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 LICENSE)                       ;;
+;;                                                                        ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(context
+ (default
+  (env (_ (env-vars ("OCAML_LANDMARKS" "auto")))))
+)

src/plugins/alias/frama-c-alias.opam

+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+depends: [
+  "dune" {>= "3.2"}
+  "frama-c" {>= "25.0" & < "27.0"}
+  "unionFind" {= "20220122"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+name: "frama-c-alias"
+version: "26"
+synopsis: "A Frama-C plug-in for Alias Analysis"
+description: """
+  A Frama-C plug-in for Alias Analysis
+"""
+maintainer: "https://git.frama-c.com/pub/frama-c"
+authors: [
+  "Tristan Le Gall"
+  "Jan Rochel"
+]
+license: "Copyright (C) 2022-2022 CEA LIST, All rights reserved. Contact CEA LIST for licensing."
+homepage: "http://frama-c.com/"
+bug-reports: "https://git.frama-c.com/pub/frama-c"

src/plugins/alias/frama-c-alias.opam.template

+name: "frama-c-alias"
+version: "26"
+synopsis: "A Frama-C plug-in for Alias Analysis"
+description: """
+  A Frama-C plug-in for Alias Analysis
+"""
+maintainer: "https://git.frama-c.com/pub/frama-c"
+authors: [
+  "Tristan Le Gall"
+  "Jan Rochel"
+]
+license: "Copyright (C) 2022-2022 CEA LIST, All rights reserved. Contact CEA LIST for licensing."
+homepage: "http://frama-c.com/"
+bug-reports: "https://git.frama-c.com/pub/frama-c"