Source file meta_deduce.ml

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

(** Offset types handled on variables *)
type supported_offset = NoOff | Field of (fieldinfo * supported_offset)

let emitter = Emitter.create "Deduction engine"
    ~correctness:[] ~tuning:[] [Emitter.Code_annot]

(** ==== PRINTERS FOR THE GENERATION OF PROLOG MODELS ==== *)

(** Print variables as their name and unique id *)
let pp_vi fmt vi =
  Format.fprintf fmt "%s_%d" (String.lowercase_ascii vi.vname) vi.vid

(** Handle offset when printing variables *)
let rec pp_off fmt base = function
  | NoOff -> base fmt ()
  | Field (fi, next) ->
    let base' fmt () =
      Format.fprintf fmt "field(%a, %a)" base () Printer.pp_field fi
    in pp_off fmt base' next

(** Print variables with their offset handled *)
let pp_vi_off fmt (vi, off) =
  pp_off fmt (fun fmt () -> pp_vi fmt vi) off

(** Print the name of a function *)
let pp_ta fmt target =
  (* Avoid having targets beginning with a _ *)
  Format.fprintf fmt "f_%s" (String.lowercase_ascii target)

(** List global variables of a program *)
let get_globals () =
  let r = ref [] in
  Globals.Vars.iter (fun vi _ -> r := vi :: !r);
  !r

(** Iter on f called on the name of a function, and returns the set *)
let callgraph_set_of f ?(orig = ref StrSet.empty) funame =
  let kf = Globals.Functions.find_by_name funame in
  f (fun ckf ->
      let n = Kernel_function.get_name ckf in
      orig := StrSet.add n !orig
    ) kf ; orig

let set_of_callees = callgraph_set_of Callgraph.Uses.iter_on_callees
let set_of_callers = callgraph_set_of Callgraph.Uses.iter_on_callers

(** Get name of function *)
let get_vi_name func acc =
  try
    let kf = Globals.Functions.find_by_name func in
    let vi = Kernel_function.get_vi kf in
    StrSet.add vi.vname acc
  with Not_found ->
    Self.warning
      ~wkey:Meta_options.unknown_func_wkey
      "%s is not a valid C function, ignoring it during target computation"
      func;
    acc

(** Expand set formula defining the targets of an HILARE.
    In particular, resolve \ALL, \callers, \callees, \in_file
    and perform set operations
*)
let rec compute_target = function
  | TgAll ->
    Globals.Functions.fold (fun kf acc ->
        ((Kernel_function.get_vi kf).vname) :: acc) [] |> StrSet.of_list
  | TgSet s -> StrSet.fold get_vi_name s StrSet.empty
  | TgInter sl ->
    sl |> List.map compute_target |> List.fold_left StrSet.inter StrSet.empty
  | TgUnion sl ->
    sl |> List.map compute_target |> List.fold_left StrSet.union StrSet.empty
  | TgDiff (s1, s2) ->
    StrSet.diff (compute_target s1) (compute_target s2)
  | TgCallees s ->
    let open Callgraph in
    let t = compute_target s in
    if not (Services.is_computed ()) then
      Services.compute ();
    let init = ref t in
    !(StrSet.fold (fun n r -> set_of_callees ~orig:r n) t init)
  | TgCallers s ->
    let open Callgraph in
    let t = compute_target s in
    if not (Services.is_computed ()) then
      Services.compute ();
    let init = ref t in
    !(StrSet.fold (fun n r -> set_of_callers ~orig:r n) t init)
  | TgFile file ->
    Globals.Functions.fold (fun kf acc ->
        if file = (Filepath.to_string
                     (fst (Kernel_function.get_location kf)).pos_path)
        then (Kernel_function.get_vi kf).vname :: acc
        else acc
      ) [] |> StrSet.of_list

(** Given a predicate, make the list of its C free variables *)
let compute_footprint pred globals =
  Cil_datatype.Logic_var.Set.fold (fun lv l ->
      match lv.lv_origin with
        | Some vi ->
          if List.exists (fun x -> x.vid = vi.vid) globals then
            (vi :: l) else l
        | None -> l
    ) (Cil.extract_free_logicvars_from_predicate pred) []

(** Pretty-print the edges of the call graph as Prolog facts *)
let generate_callgraph fmt targets =
  List.iter (fun t ->
      let kf = Globals.Functions.find_by_name t in
      List.iter (fun (caller, _) ->
          let caller_name = Kernel_function.get_name caller in
          let callee_name = Kernel_function.get_name kf in
          Format.fprintf fmt "calls(%a, %a).@." pp_ta caller_name pp_ta callee_name;
        ) (Kernel_function.find_syntactic_callsites kf)
    ) targets

(** Generic printer for lists *)
let print_setlist pp =
  let open Format in
  let pp_sep fmt () = pp_print_string fmt ", " in
  pp_print_list ~pp_sep pp

(** Generic printer for sets of strings *)
let print_set pp fmt s =
  StrSet.fold (fun x l -> x :: l) s []
  |> print_setlist pp fmt


(** In order to get the predicate of an HILARE, we must type it.
    To type it, we must instanciate each of its meta-variables.
    Normally, it should be replaced by actual C locations.
    For the deduction, since we don't have any local term to plug in there, we
    use a dummy generic term that can be easily recognized after typing.

    If for any reason the subsequent HILARE does not type, then the user made
    wrong assumptions on its predicate and should have guarded the predicate,
    hence the error message.
*)
let dummy_term loc = {
  term_node = Tnull;
  term_loc = loc;
  term_type = Ctype Cil_const.charPtrType;
  term_name = ["YOUR META-PROPERTY SHOULD BE GUARDED WITH \\fguard OR \\tguard"]
}

(** Map every possible meta-variable to the dummy term and type the HILARE *)
let dummy_unpack mp =
  let terms = ["\\written"; "\\read"; "\\called"] in
  let assoc = List.map (fun t -> (t, RepVariable (dummy_term mp.mp_loc))) terms in
  mp.mp_property (Kernel_function.dummy ()) assoc

(** Main pattern matcher, trying to identify a pattern of predicate in order to
    translate id in Prolog.
    We check each *pred* pattern passed as a parameter and match against the
    HILARE.
*)
let predicate_counter = ref 1
let identify_pred mp preds globals =
  let unpacked = dummy_unpack mp in
  let rec find = function
    | [] -> None
    | (p, print) :: _ when Logic_utils.is_same_predicate p unpacked -> Some print
    | _ :: t -> find t
  in
  match find preds with
    | Some print -> print, preds (* We found a match *)
    | None ->
      (* No match, just compute the footprint and output a generic property *)
      let pname = "p" ^ (string_of_int !predicate_counter) in
      incr predicate_counter;
      let fp = compute_footprint unpacked globals in
      let print fmt () =
        Format.fprintf fmt "property({%a},%s)"
          (print_setlist pp_vi) fp
          pname
      in
      print, (unpacked, print) :: preds

(** From a given lval, prepare translation to Prolog when supported *)
let get_global_variable globals lval =
  let with_offset o = Option.map (fun a -> a, o) in
  match lval with
    | TVar ({lv_origin=Some({vid})}), off ->
      let v = List.find_opt (fun x -> x.vid = vid) globals in
      let rec get_offset = function
        | TNoOffset -> NoOff
        | TField (fi, next) -> Field (fi, get_offset next)
        | _ -> Self.warning
                 "Deduction patterns do not support offsets other than fields"; NoOff
      in
      with_offset (get_offset off) v
    | _ -> None

(** Match predicates of the (exact) form \separated(\written, &X) *)
let is_not_written_predicate globals mp =
  let unpacked = dummy_unpack mp in
  let dt = dummy_term mp.mp_loc in
  begin match unpacked.pred_content with
    | Pseparated [d; l] when Logic_utils.is_same_term d dt ->
      begin match l.term_node with
        | TAddrOf tlval ->
          get_global_variable globals tlval
        | _ -> None
      end
    | _ -> None
  end

(** Match predicates of the form X == \old(X) *)
let is_negative_assigns_predicate globals mp =
  let unpacked = dummy_unpack mp in
  let get_global_tlval t = match t with
    | TLval tlval -> get_global_variable globals tlval
    | _ -> None
  in
  match unpacked.pred_content with
    | Prel (Req, {term_node = t1}, {term_node = t2}) ->
      let l1 = get_global_tlval t1 in
      let l2 = match t2 with
        | Tat ({term_node=t2'}, BuiltinLabel Old) -> get_global_tlval t2'
        | _ -> None
      in
      begin match l1, l2 with
        | Some (a, _), Some (b, _) when a.vid = b.vid -> l1
        | _ -> None
      end
    | _ -> None

(** Export a predicate, trying to match against known patterns *)
let pp_property preds globals mp =
  let default () =
    let print, preds = identify_pred mp preds globals in
    print, preds
  in
  begin match mp.mp_context with
    | Postcond ->
      begin match is_negative_assigns_predicate globals mp with
        | Some vi_off ->
          (fun fmt () ->
             Format.fprintf fmt "negative_assigns(%a)" pp_vi_off vi_off), preds
        | None -> default ()
      end
    | Writing ->
      begin match is_not_written_predicate globals mp with
        | Some vi_off ->
          (fun fmt () -> Format.fprintf fmt "not_written(%a)" pp_vi_off vi_off), preds
        | None -> default ()
      end
    | _ -> default ()
  end

(** Export a whole HILARE: context (as a string), predicate, target set *)
let generate_mp prefix preds globals fmt (mp, tset) =
  let print, preds = pp_property preds globals mp in
  Format.fprintf fmt "%% Export of HILARE %s@.meta_%s(\"%s\", %a, {%a}).@."
    mp.mp_name prefix
    (match mp.mp_context with
      | Weak_invariant -> "Weak invariant"
      | Strong_invariant -> "Strong invariant"
      | Conditional_invariant -> "Conditional invariant"
      | Postcond -> "Postcond"
      | Precond -> "Precond"
      | Writing -> "Writing"
      | Reading -> "Reading"
      | Calling -> "Calling"
    )
    print ()
    (print_set pp_ta) tset;
  preds

(** Export all previous HILARE *)
let all_preds = ref None
let generate_mps fmt (mps, globals, tsets) =
  let rec aux preds = function
    | [] -> all_preds := Some preds
    | mp :: t ->
      let preds = generate_mp "ground" preds globals fmt (mp,
                                                          (List.assoc mp.mp_name tsets))
      in aux preds t
  in aux [] mps

(** Generic function to run a system command with a timeout and retries *)
let rec run_with_timeout_retry ?(timeout=30) ?(max_attempts=8) command =
  if max_attempts = 0 then None
  else
    let tcommand = Format.asprintf "timeout %d %s" timeout command in
    let result = Sys.command tcommand in
    if result = 124 then
      let max_attempts = max_attempts - 1 in
      run_with_timeout_retry ~timeout ~max_attempts command
    else Some result

(** Main deduction function *)
let deduce flags mp ip mps =
  (* Retrieve the preceding HILARE in the correct order *)
  let rec takeFirstMps acc = function
    | h :: _ when h.mp_name = mp.mp_name -> List.rev acc
    | h :: t -> takeFirstMps (h :: acc) t
    | [] -> assert false
  in
  let all_mps = takeFirstMps [] mps in
  predicate_counter := 1;
  let globals = get_globals () in
  let mp_targets = List.map (fun m -> (m.mp_name, compute_target m.mp_target)) all_mps in
  (* Prepare to print *)
  let buffer = Buffer.create 5000 in
  let fmt = Format.formatter_of_buffer buffer in
  let targets =
    Globals.Functions.fold (fun kf acc ->
        ((Kernel_function.get_vi kf).vname) :: acc) []
  in

  let print_goal fmt () =
    match !all_preds with
      | Some p ->
        ignore (generate_mp "valid" p globals fmt
                  (mp, compute_target mp.mp_target))
      | None -> failwith "Oh no"
  in

  Format.fprintf fmt {|
%% This file is automatically generated by MetAcsl.
%% It is provided as an input to run.pl in order to attempt HILARE deduction.

%% == Export of the list of functions ==
targets({%a}).

%% == Export of the call graph's edges ==
%a

%% == Export already established HILAREs ==
%a

%% This is the HILARE we want to prove
go :- %a
|}
    (print_setlist pp_ta) targets
    generate_callgraph targets
    generate_mps (all_mps, globals, mp_targets)
    print_goal ()
  ;

  (* Stop printing and flush everything into a temporary file *)
  Format.pp_print_flush fmt ();
  let current_dir = Sys.getcwd () in
  let filename = Format.asprintf "%s/%s_goal.slog" current_dir mp.mp_name in
  let oc = open_out filename in
  output_string oc (Buffer.contents buffer);
  close_out oc;
  (* Locate where the Prolog model is and go to it *)
  let dir =
    try Findlib.package_directory "frama-c-metacsl"
    with Findlib.No_such_package(_,err) ->
      Self.fatal "Could not locate my own directory: %s" err
  in
  Sys.chdir (dir ^ "/deduce");
  (* Run the Prolog model on our file, with a 30s timeout *)
  let command = Format.asprintf "./run.pl prove %s 30 > /dev/null" filename in
  let max_attempts = 8 in
  let result = match run_with_timeout_retry ~max_attempts command with
    | None ->
      (* This happens if Prolog get stuck and is not interruptible, for an obuscure reaons *)
      Self.warning "%s : PROLOG FAILURE, (%d ATTEMPTS)" mp.mp_name max_attempts;
      Property_status.emit emitter ~hyps:[] ip Property_status.False_and_reachable;
      false
    | Some 0 -> (* Property could be deduced, propagate status *)
      Self.feedback "%s : OK" mp.mp_name;
      Property_status.emit emitter ~hyps:[] ip Property_status.True; true
    | Some _ -> (* Property could not be deduced, propagate FALSE to be safe *)
      Self.warning "%s : FAILURE" mp.mp_name;
      Property_status.emit emitter ~hyps:[] ip Property_status.False_and_reachable;
      false
  in
  Sys.chdir current_dir;
  if not flags.keep_proof_files then Sys.remove filename;
  result