Source file meta_parse.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 Logic_ptree
open Logic_typing
open Cil_types
open Meta_options
open Meta_utils

(* Define builtins *)
type context =
  | Weak_invariant
  | Strong_invariant
  | Calling
  | Writing
  | Reading
  | Postcond
  | Precond
  | Conditional_invariant

type target =
  | TgAll
  | TgSet of StrSet.t
  | TgUnion of target list
  | TgInter of target list
  | TgDiff of target * target
  | TgCallees of target
  | TgCallers of target
  | TgFile of string

(* How is the global status of the property obtained *)
type mp_proof_method =
  | MmLocal
  | MmDeduction
  | MmAxiom

(* How should a property be translated locally *)
type mp_translation =
  | MtCheck
  | MtAssert
  | MtDefault (* translation activated, with unspecified mode *)
  | MtNone

(* Kinds of keywords that can be replaced in a MP instantiation *)
type replaced_kind =
  | RepVariable of term (* replace variable by term *)
  | RepApp of (string * term) list (* replace application with arg by associated term *)

type metaproperty = {
  mp_name : string;
  mp_target : target;
  mp_context : context;
  mp_property : Kernel_function.t -> (string * replaced_kind) list -> predicate;
  mp_proof_method : mp_proof_method;
  mp_translation : mp_translation;
  mp_loc : Cil_types.location
}

let mp_commands = ["\\prop"]
let mp_contexts = [
  "\\weak_invariant";
  "\\strong_invariant";
  "\\writing";
  "\\calling";
  "\\reading";
  "\\postcond";
  "\\precond";
  "\\conditional_invariant"
]
let mp_metavariables = [
  "\\written";
  "\\lhost_written";
  "\\read";
  "\\lhost_read";
  "\\called";
  "\\called_arg";
  "\\func";
]
let mp_utils = [
  "\\diff";
  "\\ALL"
]
let mp_preds = mp_commands @ mp_contexts
let mp_terms = mp_metavariables @ mp_utils

(* Gathered properties *)
let gathered_props = ref []

(* Generic typing for classic ACSL predicates, allowing the
 * presence of custom predicates inside *)
let meta_type_predicate loc orig_ctxt meta_ctxt env expr =
  match expr.lexpr_node with
    | PLapp (pname, _, args) when List.mem pname mp_preds ->
      let terms = List.map (meta_ctxt.type_term meta_ctxt env) args in
      let logic_info = List.hd (Logic_env.find_all_logic_functions pname) in
      Logic_const.papp (logic_info, [], terms)
    | PLapp ("\\fguard", _, [dangerous]) ->
      begin try meta_ctxt.type_predicate meta_ctxt env dangerous
      with _ -> Logic_const.pfalse end
    | PLapp ("\\tguard", _, [dangerous]) ->
      begin try meta_ctxt.type_predicate meta_ctxt env dangerous
      with _ -> Logic_const.ptrue end
    | PLapp ("\\assert_type", _, [{lexpr_node = PLcast (ltyp, lexpr)}]) ->
      let typed_term = meta_ctxt.type_term meta_ctxt env lexpr in
      let desired_type = meta_ctxt.logic_type meta_ctxt loc env ltyp in
      let real_type = typed_term.term_type in
      if Cil_datatype.Logic_type_NoUnroll.equal real_type desired_type then
        Logic_const.ptrue
      else meta_ctxt.error loc "%a has type %a instead of %a"
          Printer.pp_term typed_term Printer.pp_logic_type real_type
          Printer.pp_logic_type desired_type
    | _ -> orig_ctxt.type_predicate meta_ctxt env expr

(* Generic typing for classic ACSL terms, allowing the
 * presence of custom term placeholders (\writing, ...). These will be
 * replaced by an actual term as defined by the termassoc association table
*)
let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
  match expr.lexpr_node with
    | PLat(e, l) when List.mem l ["After";"Before"] ->
      let e_t = meta_ctxt.type_term meta_ctxt env e in
      let label = FormalLabel l in
      Logic_const.tat (e_t, label)
    | PLapp ("\\formal", _, [{lexpr_node = PLvar param}]) ->
      (match Globals.Syntactic_search.find_in_scope param (Formal kf) with
        | Some vi -> vi |> Cil.cvar_to_lvar |> Logic_const.tvar
        | None ->
          meta_ctxt.error loc "%s is not a formal in %a"
            param Kernel_function.pretty kf)
    | PLapp ("\\bound", _, [bound]) ->
      Meta_bindings.parse_bound meta_ctxt loc quantifiers bound
    | PLapp (app_name, _, [{lexpr_node = PLvar arg}])
      when List.mem app_name mp_terms ->
      begin match List.assoc_opt app_name termassoc with
        | Some RepApp l ->
          begin match List.assoc_opt arg l with
            | Some term -> term
            | None -> meta_ctxt.error loc
                        "%s is not a valid argument for %s here" arg app_name
          end
        | None -> meta_ctxt.error loc
                    "Application of %s forbidden in this context" app_name
        | _ -> meta_ctxt.error loc
                 "%s expects no arguments but has been provided with one"
                 app_name
      end
    | PLvar vname when List.mem vname mp_terms ->
      begin match List.assoc_opt vname termassoc with
        | Some RepVariable a -> a
        | None -> meta_ctxt.error loc
                    "Variable %s forbidden in this context" vname
        | _ -> meta_ctxt.error loc
                 "%s expects one argument but has been provided with none" vname
      end
    | _ -> orig_ctxt.type_term meta_ctxt env expr

(* Given an association table, combine the previous functions to type
 * a full custom predicate
*)
let process_meta_termassoc typing_context loc kf termassoc expr =
  let quantifiers = Str_Hashtbl.create 5 in
  let meta_tc =
    {typing_context with
       type_predicate = (meta_type_predicate loc typing_context);
       type_term = (meta_type_term termassoc quantifiers kf loc typing_context)
    }
  in
  let fenv = Logic_typing.append_here_label meta_tc.pre_state in
  let fenv2 = Logic_typing.append_pre_label fenv in
  let fenv3 = Logic_typing.append_old_and_post_labels fenv2 in
  let pred = meta_tc.type_predicate meta_tc fenv3 expr in
  Meta_bindings.after_parse meta_tc pred quantifiers

(* Check that a given lexpr refer to a C function and return its varinfo *)
let process_single_target tc expr =
  match expr.lexpr_node with
    | PLvar func -> func
    | _ -> tc.error expr.lexpr_loc "Target is not a variable"

let process_string tc f e = match e.lexpr_node with
  | PLconstant (StringConstant n) -> n
  | PLvar n -> n
  | _ -> tc.error e.lexpr_loc f


(* Process a set (+\diff) expression to a custom target type
 * (because the computation of \ALL must be delegated)
*)
let rec process_targets tc expr = match expr.lexpr_node with
  | PLempty -> TgSet StrSet.empty
  | PLvar "\\ALL" -> TgAll
  | PLset elems ->
    let s = elems |> List.map (process_single_target tc) |> StrSet.of_list in
    TgSet s
  | PLunion l -> TgUnion (List.map (process_targets tc) l)
  | PLinter l -> TgInter (List.map (process_targets tc) l)
  | PLapp ("\\diff", _, [s1; s2]) ->
    TgDiff (process_targets tc s1, process_targets tc s2)
  | PLapp ("\\callees", _, [t]) -> TgCallees (process_targets tc t)
  | PLapp ("\\callers", _, [t]) -> TgCallers (process_targets tc t)
  | PLapp ("\\in_file", _, [t]) -> TgFile (process_string tc "Expected filename" t)
  (* Try to treat non-set expr as a singleton *)
  | _ -> TgSet (StrSet.singleton @@ process_single_target tc expr)

let pp_aslist fmt l =
  let pp_replaced_kind fmt = function
    | RepVariable v -> Printer.pp_term fmt v
    | RepApp l ->
      let pp_singular fmt (a, b) =
        Format.fprintf fmt "(%s, %a)" a Printer.pp_term b
      in Format.pp_print_list pp_singular fmt l
  in
  let pp_assoc fmt (a, b) =
    Format.fprintf fmt "(%s, %a)" a pp_replaced_kind b
  in Format.pp_print_list pp_assoc fmt l

(* Display a typing error, trying to parse the uncatchable
   Cabs2cil exception to avoid clutter *)
let typing_error hloc mp_name kf_name metavars (loc, error_msg) =
  let metav_msg =
    if metavars = [] then "there were no meta-variables."
    else Format.asprintf "meta-variables were: %a" pp_aslist metavars
  in
  Self.abort "Error during the typing of a HILARE!\n\
              What:        the HILARE named '%s' (%a)\n\
              Where:       in function '%s', at %a\n\
              Why:         %s\n\
              Environment: %s"
    mp_name Cil_datatype.Location.pretty hloc
    kf_name Cil_datatype.Location.pretty loc
    error_msg
    metav_msg

let delay_prop tc name lexpr kf aslist =
  let dfind_var ?label:_ var =
    (* Tweak find_var so it can find things after link *)
    try tc.find_var var
    with Not_found -> try
      let vi = Globals.Vars.find_from_astinfo var Global in
      Cil.cvar_to_lvar vi
    with Not_found ->
      let kf = Globals.Functions.find_by_name var in
      let vi = Kernel_function.get_vi kf in
      Cil.cvar_to_lvar vi
  in
  let dfet s =
    try tc.find_enum_tag s
    with _ -> Globals.Types.find_enum_tag s
  in
  let dft a b = Globals.Types.find_type a b
  in
  let delayed_tc = {tc with find_var = dfind_var;
                            find_enum_tag = dfet;
                            find_type = dft} in
  let loc = lexpr.lexpr_loc in
  delayed_tc.on_error
    (process_meta_termassoc delayed_tc loc kf aslist)
    (typing_error loc name (Kernel_function.get_name kf) aslist)
    lexpr

let rec macro_replacer changer lexpr =
  let f = macro_replacer changer in
  let lexpr_node = match changer lexpr.lexpr_node with
    | PLapp (a, b, c) -> PLapp (a, b, List.map f c)
    | PLlambda (a, b) -> PLlambda (a, f b)
    | PLlet (a, b, c) -> PLlet (a, f b, f c)
    | PLunop (a, b) -> PLunop (a, f b)
    | PLbinop (a, b, c) -> PLbinop (f a, b, f c)
    | PLdot (a, b) -> PLdot (f a, b)
    | PLarrow (a, b) -> PLarrow (f a, b)
    | PLarrget (a, b) -> PLarrget (f a, f b)
    | PLold a -> PLold (f a)
    | PLat (a, b) -> PLat (f a, b)
    | PLcast (a, b) -> PLcast (a, f b)
    | PLrange (a, b) -> PLrange (Option.map f a, Option.map f b)
    | PLsizeofE a -> PLsizeofE (f a)
    | PLupdate (a, b, c) -> PLupdate (f a, b, c)
    | PLtypeof a -> PLtypeof (f a)
    | PLrel (a, b, c) -> PLrel (f a, b, f c)
    | PLand (a, b) -> PLand (f a, f b)
    | PLor (a, b) -> PLor (f a, f b)
    | PLxor (a, b) -> PLxor (f a, f b)
    | PLimplies (a, b) -> PLimplies (f a, f b)
    | PLiff (a, b) -> PLiff (f a, f b)
    | PLnot a -> PLnot (f a)
    | PLif (a, b, c) -> PLif (f a, f b, f c)
    | PLforall (a, b) -> PLforall (a, f b)
    | PLexists (a, b) -> PLexists (a, f b)
    | PLbase_addr (a, b) -> PLbase_addr (a, f b)
    | PLoffset (a, b) -> PLoffset (a, f b)
    | PLblock_length (a, b) -> PLblock_length (a, f b)
    | PLvalid (a, b) -> PLvalid (a, f b)
    | PLvalid_read (a, b) -> PLvalid_read (a, f b)
    | PLvalid_function a -> PLvalid_function (f a)
    | PLallocable (a, b) -> PLallocable (a, f b)
    | PLfreeable (a, b) -> PLfreeable (a, f b)
    | PLinitialized (a, b) -> PLinitialized (a, f b)
    | PLdangling (a, b) -> PLdangling (a, f b)
    | PLfresh (a, b, c) -> PLfresh (a, f b, f c)
    | PLseparated a -> PLseparated (List.map f a)
    | PLnamed (a, b) -> PLnamed (a, f b)
    | PLcomprehension (a, b, c) -> PLcomprehension (f a, b, Option.map f c)
    | PLset a -> PLset (List.map f a)
    | PLunion a -> PLunion (List.map f a)
    | PLinter a -> PLset (List.map f a)
    | PLlist a -> PLset (List.map f a)
    | PLrepeat (a, b) -> PLrepeat (f a, f b)
    | l -> l
  in {lexpr with lexpr_node}

let macro_table = Hashtbl.create 2
let process_macro tc loc = function
  | [
    {lexpr_node = PLapp ("\\name", _, [ename])};
    {lexpr_node = PLapp ("\\arg_nb", _, [eargnb])};
    etemplate
  ] ->
    let name = match ename.lexpr_node with
      | PLvar n -> n
      | _ -> tc.error ename.lexpr_loc "Name must be a single word"
    in let arg_nb = match eargnb.lexpr_node with
        | PLconstant (IntConstant i) -> int_of_string i
        | _ -> tc.error eargnb.lexpr_loc "arg_nb must be a positive integer"
    in
    Hashtbl.add macro_table name (arg_nb, etemplate);
    Ext_terms [Logic_const.tstring ~loc ("macro_" ^ name)]
  | _ -> tc.error loc "Invalid macro shape"

let expand_macros tc loc prop =
  let prefix = "\\param_" in
  let macro_filter = function
    | PLapp (name, _, params) as a ->
      if Hashtbl.mem macro_table name then
        let argnb, template = Hashtbl.find macro_table name in
        if List.length params = argnb then
          let extract_param p =
            Extlib.string_del_prefix prefix p
            |> Option.map (int_of_string)
            |> fun o -> Option.bind o (fun n ->
                if n <= argnb && n > 0 then Some (n - 1) else None
              )
          in
          let param_replacer = function
            | (PLvar v) as e -> begin match extract_param v with
                | Some n -> (List.nth params n).lexpr_node
                | None -> e
              end
            | (PLlet (s, b, r)) as e -> begin match extract_param s with
                | Some n -> begin match (List.nth params n).lexpr_node with
                    | PLvar na -> PLlet (na, b, r)
                    | _ -> tc.error loc "Param replacement in \\let should be a simple var"
                  end
                | None -> e
              end
            | e -> e
          in (macro_replacer param_replacer template).lexpr_node
        else tc.error loc "%s takes %d args but %d were given" name argnb
            (List.length params)
      else a
    | e -> e
  in macro_replacer macro_filter prop

let process_flags tc loc = function
  | {lexpr_node = PLapp ("\\flags", _, l)} ->
    List.map (fun x -> match x.lexpr_node with
        | PLnamed ("proof", {lexpr_node=PLvar v}) -> begin match v with
            | "axiom" -> `Axiom
            | "deduce" -> `Deduction
            | "local" -> `Local
            | _ -> tc.error loc "Invalid value %s for flag proof" v
          end
        | PLnamed ("translate", {lexpr_node=PLvar v}) -> begin match v with
            | "true" | "yes" -> `Translate
            | "false" | "no" -> `NoTranslate
            | "check" -> `ForceCheck
            | "assert" -> `ForceAssert
            | _ -> tc.error loc "Invalid value %s for flag translate" v
          end
        | PLnamed (k, {lexpr_node=PLvar _}) -> tc.error loc "Unknown flag %s" k
        | _ -> tc.error loc "A flag should has the shape key:value"
      ) l
  | _ -> tc.error loc "Flags should be absent or listed with \\flags"

let get_status tc loc options =
  (* By default, translate locally with asserts *)
  let pm = ref MmLocal in
  let tr = ref MtDefault in
  List.iter (function
      | `Axiom -> pm := MmAxiom
      | `Local -> pm := MmLocal
      | `Deduction -> pm := MmDeduction
      | `ForceAssert -> tr := MtAssert
      | `ForceCheck -> tr := MtCheck
      | `Translate -> tr := MtDefault
      | `NoTranslate -> tr := MtNone
    ) options;
  if !pm = MmLocal && !tr = MtNone then
    tc.error loc "When proof method is local, translation must be enabled"
  ; (!pm, !tr)

(* Take the params of \prop as lexprs, type it and fill the table.
 * The last parameter is not typed, as we don't know yet how the placeholders
 * will be replaced (thus the whole property is untypable yet. Instead its
 * typing is wrapped into a function taking the correct association table, to
 * delegate the task until instanciation
*)
let process_property tc loc = function
  | {lexpr_node = PLapp ("\\name", _, [ename])} ::
    {lexpr_node = PLapp ("\\targets", _, [etargets])} ::
    {lexpr_node = PLapp ("\\context", _, [econtext])} :: tail ->
    let mp_name = process_string tc "Prop name must be a string" ename in
    let mp_target = process_targets tc etargets in
    let mp_context = match econtext.lexpr_node with
      | PLvar "\\weak_invariant" -> Weak_invariant
      | PLvar "\\strong_invariant" -> Strong_invariant
      | PLvar "\\conditional_invariant" -> Conditional_invariant
      | PLvar "\\writing" -> Writing
      | PLvar "\\reading" -> Reading
      | PLvar "\\calling" -> Calling
      | PLvar "\\precond" -> Precond
      | PLvar "\\postcond" -> Postcond
      | _ -> tc.error econtext.lexpr_loc "Invalid context %a"
               Logic_print.print_lexpr econtext
    in
    let eproperty, options = match tail with
      | [] -> tc.error loc "Missing actual property"
      | [x] -> x, []
      | [o; x] -> x, process_flags tc loc o
      | _ -> tc.error loc "Too many trailing arguments in MP"
    in
    let mp_proof_method, mp_translation = get_status tc loc options in
    (* Execute macros in property *)
    let expanded = expand_macros tc loc eproperty in
    (* Delegate typing of property *)
    let mp_property = delay_prop tc mp_name expanded in
    gathered_props := {mp_name; mp_target; mp_context; mp_proof_method;
                       mp_translation; mp_property; mp_loc = loc} :: !gathered_props;
    Ext_terms [Logic_const.tstring ~loc mp_name]
  | _ -> tc.error loc "Invalid property shape"

(* Process each command and fill the table *)
let process_meta tc loc l =
  begin match l with
    | command :: t -> begin match command.lexpr_node with
        | PLvar "\\prop" -> process_property tc loc t
        | PLvar "\\macro" -> process_macro tc loc t
        (* Already processed file *)
        | PLconstant StringConstant str -> Ext_terms [Logic_const.tstring ~loc str]
        | _ -> tc.error loc "Invalid command"
      end
    | _ -> tc.error loc "Missing command"
  end

let process_inline tc loc = function
  | [{lexpr_node = PLvar "lenient"}] ->
    Ext_terms [Logic_const.tstring "lenient"]
  | [{lexpr_node = PLapp("\\bind", _, [{lexpr_node = PLvar cvar_name};
                                       {lexpr_node = PLvar gvar_name}])}] ->
    Meta_bindings.parse_bind tc loc cvar_name gvar_name
  | _ -> Self.warning "%a: invalid inline annotation" Printer.pp_location loc;
    Ext_id (-1)

let register_parsing () =
  (* Add builtins, as predicates and terms *)
  let bl_from_name predicate bl_name = {
    bl_name; bl_labels = []; bl_params = []; bl_profile = [];
    bl_type = if predicate then None else Some (Lvar "dummy")
  } in
  mp_preds |> List.map (bl_from_name true) |> List.iter Logic_builtin.register;
  mp_terms |> List.map (bl_from_name false) |> List.iter Logic_builtin.register;
  (* Register parser for meta global statements *)
  Acsl_extension.register_global ~plugin:"meta" "meta" process_meta true;
  Acsl_extension.register_code_annot_next_stmt ~plugin:"meta" "imeta"
    process_inline ~visitor:Meta_bindings.process_imeta false

(* !! Expects a list of props sorted by name !! *)
let rec check_for_duplicates = function
  | [] -> None
  | [_] -> None
  | h1 :: h2 :: _ when h1.mp_name = h2.mp_name -> Some (h1, h2)
  | _ :: t -> check_for_duplicates t

let metaproperties () =
  (* Check that there are no duplicate MPs *)
  let sorted_props = List.sort (fun a b -> compare a.mp_name b.mp_name)
      !gathered_props in
  begin match check_for_duplicates sorted_props with
    | None -> ()
    | Some (m1, m2) ->
      Self.abort "The meta-property named %s is defined at \
                  least twice :@,Here: %a@,and here: %a"
        m1.mp_name Printer.pp_location m1.mp_loc Printer.pp_location m2.mp_loc
  end ;
  List.rev !gathered_props