Source file meta_dispatch.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's MetACSL plug-in.                   *)
(*                                                                        *)
(*  Copyright (C) 2018-2024                                               *)
(*    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 Meta_utils
open Meta_parse
open Meta_options

type unpacked_metaproperty = {
  ump_emitter : Emitter.t;
  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * replaced_kind) list -> predicate;
  ump_ip : Property.t;
  ump_counter : int ref;
  ump_admit : bool;
  ump_assert : bool;
}

let name_of_meta_acsl_term t = match t.term_node with
  | TConst LStr s -> s
  | _ -> failwith "Invalid meta term"

let get_mp_ip mp =
  let vis = object (_)
    inherit Visitor.frama_c_inplace
    val mutable found = None
    method get () = Option.get found
    method! vannotation = function
      | Dextended ({ext_name = "meta"; ext_kind = Ext_terms [t]} as ext, _, _) when
          name_of_meta_acsl_term t = mp.mp_name ->
        found <- Some (Property.ip_of_extended Property.ELGlob ext);
        Cil.SkipChildren
      | _ -> Cil.DoChildren
  end in
  ignore (Visitor.visitFramacFileSameGlobals
            (vis :> Visitor.frama_c_visitor) (Ast.get ()));
  vis # get ()

let name_mp_pred flags pred ump_counter =
  let pred = if flags.prefix_meta then
      {pred with pred_name = "meta" :: pred.pred_name} else pred in
  if flags.number_assertions then (
    (* Number the instantiation *)
    ump_counter := !ump_counter + 1;
    {pred with pred_name = ("_" ^ (string_of_int !ump_counter)) :: pred.pred_name}
  )
  else pred

let unpack_mp flags mp admit =
  let ump_emitter = Emitter.create mp.mp_name
      ~correctness:[] ~tuning:[] [Emitter.Code_annot]
  in
  let ump_ip = get_mp_ip mp in
  let ump_counter = ref 0 in
  (* Wrapped property *)
  let ump_property kf ?stmt al =
    let pred = mp.mp_property kf al in
    let pred = match stmt with
      | None -> pred
      | Some stmt -> Meta_simplify.remove_alpha_conflicts pred kf stmt
    in
    let pred = if flags.simpl then
        Meta_simplify.simplify pred
      else pred
    in pred
  in
  let ump_assert = match mp.mp_translation with
    | MtNone -> assert false
    | MtAssert -> true
    | MtCheck -> false
    | MtDefault -> flags.default_to_assert
  in
  {ump_emitter; ump_property; ump_ip; ump_counter; ump_admit = admit; ump_assert}

(* Returns an assoc list associating each context to a
 * hash table mapping each function to a list of
 * MP names to process for that context and for that function.
 * The order is the same as in the original file
 *
 * Also returns a hash table mapping a MP name to an unpacked MP
*)
let dispatch flags mps =
  let all_mp = Hashtbl.create 10 in
  let ctxts = [Weak_invariant; Strong_invariant; Writing; Reading; Calling;
               Precond; Postcond; Conditional_invariant] in
  let tables = List.map (fun ctx -> ctx, Str_Hashtbl.create 5) ctxts in
  List.iter (fun mp ->
      let table = List.assoc mp.mp_context tables in
      let targets = Meta_deduce.compute_target mp.mp_target in
      if flags.list_targets then
        Self.feedback "Targets of %s: %a" mp.mp_name
          StrSet.pretty targets
      ;
      let admit = match mp.mp_proof_method with
        | MmLocal -> false
        | MmAxiom -> true
        | MmDeduction ->
          let ip = get_mp_ip mp in
          Meta_deduce.deduce flags mp ip mps
      in
      if mp.mp_translation <> MtNone then (
        StrSet.iter (fun target ->
            add_to_hash_list Str_Hashtbl.(find_opt, replace) table target mp.mp_name
          ) targets;
        Hashtbl.add all_mp mp.mp_name (unpack_mp flags mp admit)
      );
    ) mps;
  (* Reverse lists in tables to maintain the correct order *)
  List.iter (fun (_, table) ->
      Str_Hashtbl.iter (fun k v ->
          Str_Hashtbl.replace table k (List.rev v)
        ) table
    ) tables;
  tables, all_mp

module UmpHash = struct
  type t = unpacked_metaproperty
  let equal a b = Emitter.equal a.ump_emitter b.ump_emitter
  let hash p = Emitter.hash p.ump_emitter
end
module UmpHashtbl = Hashtbl.Make(UmpHash)

(* Associates a list of deps (IPs) to an UMP *)
let dependencies = UmpHashtbl.create 10
(* Call each time an instantiation of a prop is done *)
let add_dependency ump ips =
  List.iter (add_to_hash_list UmpHashtbl.(find_opt, replace) dependencies ump) ips

(* Call once at the end to actually register dependencies between props and
 * their instanciations *)
let finalize_dependencies () =
  let keys = UmpHashtbl.to_seq_keys dependencies in
  let add_one prop =
    let deps = find_hash_list UmpHashtbl.find_opt dependencies prop in
    (* If the MP is admitted, every instance *is* true *)
    if prop.ump_admit then
      List.iter (fun inst ->
          Property_status.emit prop.ump_emitter ~hyps:[] inst Property_status.True
        ) deps
    else (
      (* The MP is true if every instance is true *)
      Property_status.emit prop.ump_emitter ~hyps:deps prop.ump_ip Property_status.True
    )
  in
  Seq.iter add_one keys