diff --git a/Makefile b/Makefile index af9f1b7bef88ce2ef2c4eff555bbd034677060af..4141be89ffdb77e1a58512f4ac273dd5f031556e 100644 --- a/Makefile +++ b/Makefile @@ -563,6 +563,7 @@ KERNEL_CMO=\ src/kernel_services/ast_data/annotations.cmo \ src/kernel_services/ast_printing/printer.cmo \ src/kernel_internals/typing/logic_builtin.cmo \ + src/kernel_services/ast_queries/ast_diff.cmo \ src/kernel_services/ast_printing/cabs_debug.cmo \ src/kernel_internals/parsing/lexerhack.cmo \ src/kernel_internals/parsing/clexer.cmo \ diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 85a742841df0fe295e65d22132756dd7788da302..e34347acdd061e025cfff74a0507b0f5dfac4d46 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -594,6 +594,8 @@ src/kernel_services/ast_printing/printer_tag.mli: CEA_LGPL src/kernel_services/ast_queries/README.md: .ignore src/kernel_services/ast_queries/acsl_extension.ml: CEA_LGPL src/kernel_services/ast_queries/acsl_extension.mli: CEA_LGPL +src/kernel_services/ast_queries/ast_diff.ml: CEA_LGPL +src/kernel_services/ast_queries/ast_diff.mli: CEA_LGPL src/kernel_services/ast_queries/ast_info.ml: CEA_LGPL src/kernel_services/ast_queries/ast_info.mli: CEA_LGPL src/kernel_services/ast_queries/cil.ml: CIL diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml new file mode 100644 index 0000000000000000000000000000000000000000..24757a156e653bb93fe74b912f6883e267902512 --- /dev/null +++ b/src/kernel_services/ast_queries/ast_diff.ml @@ -0,0 +1,156 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2021 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +open Cil_types + +module Orig_project = + State_builder.Option_ref(Project.Datatype)( + struct + let name = "Ast_diff.OrigProject" + let dependencies = [] + end) + +type 'a correspondance = + [ `Same of 'a (** symbol with identical definition has been found. *) + | `Not_present (** no correspondance *) + ] + +module Correspondance = + Datatype.Polymorphic( + struct + type 'a t = 'a correspondance + let name a = Type.name a ^ " correspondance" + let module_name = "Correspondance" + let structural_descr _ = Structural_descr.t_abstract + let reprs x = [ `Not_present; `Same x] + let mk_equal eq x y = + match x,y with + | `Same x, `Same y -> eq x y + | `Not_present, `Not_present -> true + | `Same _, `Not_present + | `Not_present, `Same _ -> false + let mk_compare cmp x y = + match x,y with + | `Not_present, `Not_present -> 0 + | `Not_present, `Same _ -> -1 + | `Same x, `Same y -> cmp x y + | `Same _, `Not_present -> 1 + let mk_hash h = function + | `Same x -> 117 * h x + | `Not_present -> 43 + let map f = function + | `Same x -> `Same (f x) + | `Not_present -> `Not_present + let mk_internal_pretty_code pp prec fmt = function + | `Not_present -> Format.pp_print_string fmt "`Not_present" + | `Same x -> + let pp fmt = Format.fprintf fmt "`Same %a" (pp Type.Call) x in + Type.par prec Call fmt pp + let mk_pretty pp fmt = function + | `Not_present -> Format.pp_print_string fmt "N/A" + | `Same x -> Format.fprintf fmt " => %a" pp x + let mk_varname v = function + | `Not_present -> "x" + | `Same x -> v x ^ "_c" + let mk_mem_project mem query = function + | `Not_present -> false + | `Same x -> mem query x + end + ) + +type kf_correspondance = + [ kernel_function correspondance + | `Same_spec of kernel_function (** body has changed, but spec is identical *) + ] + +module Kf_correspondance = + Datatype.Make( + struct + let name = "Kf_correspondance" + module C = Correspondance.Make(Kernel_function) + include Datatype.Serializable_undefined + type t = kf_correspondance + let reprs = + let kf = List.hd Kernel_function.reprs in + `Same_spec kf :: (C.reprs :> t list) + let compare x y = + match x,y with + | `Same_spec f1, `Same_spec f2 -> Kernel_function.compare f1 f2 + | `Same_spec _, _ -> 1 + | _, `Same_spec _ -> -1 + | (#correspondance as x), (#correspondance as y) -> C.compare x y + let equal = Datatype.from_compare + let hash = function + | `Same_spec f -> 57 * (Kernel_function.hash f) + | #correspondance as x -> C.hash x + let internal_pretty_code p fmt = function + | `Same_spec f -> + let pp fmt = + Format.fprintf fmt "`Same %a" + (Kernel_function.internal_pretty_code Type.Call) f + in + Type.par p Call fmt pp + | #correspondance as x -> C.internal_pretty_code p fmt x + let pretty fmt = function + | `Same_spec f -> + Format.fprintf fmt "-> (contract) %a" Kernel_function.pretty f + | #correspondance as x -> C.pretty fmt x + end) + +module Info(I: sig val name: string end) = + (struct + let name = "Ast_diff." ^ I.name + let dependencies = [Ast.self; Orig_project.self ] + let size = 43 + end) + +module Build(D:Datatype.S_with_collections) = + State_builder.Hashtbl(D.Hashtbl)(Correspondance.Make(D)) + (Info(struct let name = "Ast_diff." ^ D.name end)) + +module Varinfo = Build(Cil_datatype.Varinfo) + +module Compinfo = Build(Cil_datatype.Compinfo) + +module Enuminfo = Build(Cil_datatype.Enuminfo) + +module Enumitem = Build(Cil_datatype.Enumitem) + +module Typeinfo = Build(Cil_datatype.Typeinfo) + +module Stmt = Build(Cil_datatype.Stmt) + +module Logic_info = Build(Cil_datatype.Logic_info) + +module Logic_type_info = Build(Cil_datatype.Logic_type_info) + +module Fieldinfo = Build(Cil_datatype.Fieldinfo) + +module Model_info = Build(Cil_datatype.Model_info) + +module Logic_var = Build(Cil_datatype.Logic_var) + +module Kernel_function = + State_builder.Hashtbl(Kernel_function.Hashtbl)(Kf_correspondance) + (Info(struct let name = "Ast_diff.Kernel_function" end)) + +module Fundec = Build(Cil_datatype.Fundec) diff --git a/src/kernel_services/ast_queries/ast_diff.mli b/src/kernel_services/ast_queries/ast_diff.mli new file mode 100644 index 0000000000000000000000000000000000000000..fe83242b179ab102af7a404f8418c0e4ee57a0c2 --- /dev/null +++ b/src/kernel_services/ast_queries/ast_diff.mli @@ -0,0 +1,96 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2021 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +(** Compute diff information from an existing project. + + @since Frama-C+dev +*) + +open Cil_types + +(** the original project from which a diff is computed. *) +module Orig_project: State_builder.Option_ref with type data = Project.t + +(** possible correspondances between new items and original ones. *) +type 'a correspondance = + [ `Same of 'a (** symbol with identical definition has been found. *) + | `Not_present (** no correspondance *) + ] + +(** specific correspondance for kernel functions *) +type kf_correspondance = + [ kernel_function correspondance + | `Same_spec of kernel_function (** body has changed, but spec is identical *) + ] + +(** varinfos correspondances *) +module Varinfo: + State_builder.Hashtbl + with type key = varinfo and type data = varinfo correspondance + +module Compinfo: + State_builder.Hashtbl + with type key = compinfo and type data = compinfo correspondance + +module Enuminfo: + State_builder.Hashtbl + with type key = enuminfo and type data = enuminfo correspondance + +module Enumitem: + State_builder.Hashtbl + with type key = enumitem and type data = enumitem correspondance + +module Typeinfo: + State_builder.Hashtbl + with type key = typeinfo and type data = typeinfo correspondance + +module Stmt: + State_builder.Hashtbl + with type key = stmt and type data = stmt correspondance + +module Logic_info: + State_builder.Hashtbl + with type key = logic_info and type data = logic_info correspondance + +module Logic_type_info: + State_builder.Hashtbl + with type key = logic_type_info and type data = logic_type_info correspondance + +module Fieldinfo: + State_builder.Hashtbl + with type key = fieldinfo and type data = fieldinfo correspondance + +module Model_info: + State_builder.Hashtbl + with type key = model_info and type data = model_info correspondance + +module Logic_var: + State_builder.Hashtbl + with type key = logic_var and type data = logic_var correspondance + +module Kernel_function: + State_builder.Hashtbl + with type key = kernel_function and type data = kf_correspondance + +module Fundec: + State_builder.Hashtbl + with type key = fundec and type data = fundec correspondance