Source file rpp_parser.ml

(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

open Logic_typing
open Logic_ptree
open Cil_types

let () =
  let callpure =
    {bl_name = "\\callpure";
     bl_labels = []; bl_params = []; bl_type = None;
     bl_profile = []}
  and  callset =
    {bl_name = "\\callset";
     bl_labels = []; bl_params = []; bl_type = None;
     bl_profile = []}
  and  call =
    {bl_name = "\\call";
     bl_labels = []; bl_params = []; bl_type = None;
     bl_profile = []}
  and  callresult =
    {bl_name = "\\callresult";
     bl_labels = []; bl_params = []; bl_type = None;
     bl_profile = []}
  in
  Logic_builtin.add callpure;
  Logic_builtin.add callset;
  Logic_builtin.add call;
  Logic_builtin.add callresult

let id_hash = Hashtbl.create 3

let type_relational typing_context loc l =

  let function_parameter_check ctxt x t pred =
    match x.term_type with
    | Ctype(ty) -> if Cil_datatype.Typ.equal t ty then ()
      else
        let test = new Printer.extensible_printer () in
        ctxt.error loc "Cast are not supported:@. @[%a and %a are not compatible@] \
                        for term @. @[%a@] in call of %s @."
          (test#logic_type None)  x.term_type (Printer.pp_typ) t
          Printer.pp_term x (pred.vname)
    | Linteger ->
      if not (Ast_types.is_integral t) then
        ctxt.error loc "Cast are not supported:@. @[%a and %a are not compatible@] \
                        for term @[%a@] in call of %s @."
          (Printer.pp_logic_type)  x.term_type (Printer.pp_typ) t
          Printer.pp_term x (pred.vname)
    | Lreal ->
      if not (Ast_types.is_float t) then
        ctxt.error loc  "Cast are not supported:@. @[%a and %a are not compatible@] \
                         for term @[%a@] in call of %s @."
          (Printer.pp_logic_type)  x.term_type (Printer.pp_typ) t
          Printer.pp_term x (pred.vname)
    | _ ->  ctxt.error loc
              "@[<v 2>Function %s is called with a parameter with \
               an unsupported type:@;@[%a@]"
              pred.vname Printer.pp_term x
  in

  let is_func var ctxt =
    if Ast_types.is_fun var.vtype then var
    else
      ctxt.error loc "Expected a C function: @ @[%a@] @." Printer.pp_varinfo var
  in

  let test_origin ctxt found =
    match found.lv_origin with
    | Some var -> is_func var ctxt
    | None -> ctxt.error loc "No origin information for: @ @[%a@] @." Printer.pp_logic_var found
  in

  let check_is_function_name ctxt p =
    match p.lexpr_node with
    | PLvar x ->
      let test =
        try ctxt.find_var x  with
        | _ -> ctxt.error loc "Unknown function: @ @[%s@]  @." x
      in
      test_origin ctxt test
    | _ ->
      ctxt.error loc "Expected a function name for call but get:@ @[%a@] @." Logic_print.print_lexpr p
  in

  let check_inline_option p =
    match p.lexpr_node with
    | PLconstant(c) -> (match c with
        | IntConstant(s) ->Some(int_of_string s)
        | _ -> None)
    | _ -> None
  in

  let check_call_param ctxt env p f =
    match p.lexpr_node with
    | PLapp ("\\callpure", [], _) ->  ctxt.type_term ctxt env p
    | PLvar _ -> typing_context.type_term ctxt env p
    | PLarrow _ -> typing_context.type_term ctxt env p
    | PLconstant _ -> ctxt.type_term ctxt env p
    | PLbinop _ -> ctxt.type_term ctxt env p
    | PLdot _ -> ctxt.type_term ctxt env p
    | PLarrget _ -> ctxt.type_term ctxt env p
    | PLunop _ -> ctxt.type_term ctxt env p
    | _ -> ctxt.error loc "Unsupported terme@. @[%a@] @.in parameter for function %s @."
             Logic_print.print_lexpr p f
  in

  let type_term ctxt env p =
    match p.lexpr_node with
    | PLapp("\\callpure", [], param) ->
      let (inline,param) = (match check_inline_option (List.hd param) with
          | None -> (1,param)
          | Some x -> (x, (List.tl param)))
      in
      let pred = check_is_function_name ctxt (List.hd param) in
      let (rt,args,_,_) = Cil.splitFunctionType pred.vtype in
      if Option.is_none args then
        ctxt.error loc "Function %a does not have a prototype" Printer.pp_varinfo pred;
      let args = Option.get args in
      let length_pre = List.length (List.tl param) and length_f = List.length args in
      if length_pre <> length_f then
        ctxt.error loc "Expected %d parameter for the call of the pure function %s @."
          length_f pred.vname;
      let predn = List.map (fun p -> check_call_param ctxt env p (pred.vname)) (List.tl param) in
      List.iter2 (fun x (_,t,_) -> function_parameter_check ctxt x t pred) predn args;
      let li = List.hd (Logic_env.find_all_logic_functions "\\callpure") in
      li.l_type <- Some(Cil_types.Ctype rt);
      let inline = Logic_const.tinteger ~loc:pred.vdecl inline in
      let lv_funct = Cil.cvar_to_lvar pred in
      let funct = {term_node = TLval(TVar(lv_funct),TNoOffset);
                   term_loc = inline.term_loc;
                   term_type=Cil_types.Ctype(pred.vtype);
                   term_name = []}
      in
      Logic_const.term ~loc:p.lexpr_loc (Tapp(li,[],(inline :: [funct]) @ predn))
        (Cil_types.Ctype rt)

    | PLapp ("\\callresult", [], param) ->
      if List.length param <> 1 then
        ctxt.error loc "Expected one parameter for \\callresult built-in (identifier):@. @[%a@] @."
          Logic_print.print_lexpr p
      else begin
        let id = List.hd param in
        let id = match id.lexpr_node with
          | PLvar n -> n
          | _ ->
            ctxt.error loc
              "Expect an identifier as parameter for built-in \\callresult: @. @[%a@] @."
              Logic_print.print_lexpr p
        in
        let f =
          (try (Hashtbl.find id_hash id)
           with
           | Not_found -> ctxt.error loc "Unknown identifier %s for @. @[%a@] @."
                            id Logic_print.print_lexpr p
           | _ -> assert false
          )
        in
        let li = List.hd (Logic_env.find_all_logic_functions "\\callresult") in
        let (rt,_,_,_) = Cil.splitFunctionType f.vtype in
        li.l_type <- Some(Cil_types.Ctype rt);
        let ti = Logic_const.tstring ~loc:p.lexpr_loc id in
        Logic_const.term ~loc:p.lexpr_loc (Tapp(li,[],[ti])) (Cil_types.Ctype rt)
      end

    | PLapp ("\\callpure", _, _) ->
      ctxt.error loc "Expect no label for built-in \\callpure: @. @[%a@] @."
        Logic_print.print_lexpr p
    | PLapp ("\\callresult", _, _) ->
      ctxt.error loc "Expect no label for built-in \\callresult: @. [%a@] @."
        Logic_print.print_lexpr p
    | _ -> typing_context.type_term ctxt env p
  in

  let check_identifier ctxt l pred  =
    let rec aux li acc =
      match li with
      | h1 :: q1 -> aux q1 (h1 :: acc)
      | [] -> acc
    in
    if List.length l == 0 then
      ctxt.error loc "Expect an identifier for the \\call to function %s @." pred.vname
    else(
      let reverse = aux l [] in
      (List.tl reverse,List.hd reverse))
  in

  let check_callset_param ctxt env p =
    match p.lexpr_node with
    | PLapp ("\\call",[], param) ->
      let (inline,param) = (match check_inline_option (List.hd param) with
          | None -> (1,param)
          | Some x -> (x, (List.tl param)))
      in
      let pred = check_is_function_name ctxt (List.hd param) in
      let (rt, args, _, _) = Cil.splitFunctionType pred.vtype in
      if Option.is_none args then
        ctxt.error loc "Function %a does not have a prototype" Printer.pp_varinfo pred;
      let args = Option.get args in
      let (funct_param, id) = check_identifier ctxt (List.tl param) pred in
      let length_pre = (List.length funct_param) and length_f = List.length args in
      if length_pre <> length_f then (
        ctxt.error loc "Expected %d parameter for the \\call of the function %s: @. @[%a@] @."
          length_f pred.vname  Logic_print.print_lexpr p
      )
      else(
        let id = (match id.lexpr_node with
            | PLvar n -> n
            | _ -> ctxt.error loc "Expect an identifier as last parameter \
                                   for function %s: @. [%a@] @."
                     pred.vname Logic_print.print_lexpr p)
        in
        match (Hashtbl.find id_hash id) with
        | exception Not_found ->
          Hashtbl.add id_hash id pred;
          let predn =
            List.map (fun p -> check_call_param ctxt env p (pred.vname)) (List.rev funct_param)
          in
          List.iter2 (fun x (_,t,_) -> function_parameter_check ctxt x t pred) predn args;
          let li = List.hd (Logic_env.find_all_logic_functions "\\call") in
          let inline = Logic_const.tinteger ~loc:pred.vdecl inline in
          let tid = Logic_const.tstring ~loc:pred.vdecl id in
          li.l_type <- Some(Cil_types.Ctype rt);
          let lv_funct = Cil.cvar_to_lvar pred in
          let funct = {term_node = TLval(TVar(lv_funct),TNoOffset);
                       term_loc = inline.term_loc;
                       term_type=Cil_types.Ctype(pred.vtype);
                       term_name = []}
          in
          let res =
            Logic_const.term
              ~loc:p.lexpr_loc (Tapp(li,[],tid::inline::[funct]@predn))
              (Cil_types.Ctype rt)
          in
          let label_pre = "Pre_" ^ id in
          let label_post = "Post_" ^ id in
          let new_env =
            Logic_typing.Lenv.add_logic_label
              label_pre (FormalLabel label_pre) env
          in
          let new_env =
            Logic_typing.Lenv.add_logic_label
              label_post (FormalLabel label_post) new_env
          in
          new_env, res
        | _ -> ctxt.error loc "Multiple use of identifier %s @." id)

    | PLapp ("\\call", _, _) -> ctxt.error loc "Expect no label for built-in \\call: @. @[%a@] @."
                                  Logic_print.print_lexpr p

    | _ -> ctxt.error loc "Unsupported terme type in \\callset built-in: @. @[%a@] @."
             Logic_print.print_lexpr p
  in

  let check_call_set ctxt env p  =
    match p.lexpr_node with
    | PLapp ("\\callset",[], param) ->
      let env, calls =
        List.fold_right
          (fun p (env,calls) ->
             let (env, call) = check_callset_param ctxt env p in
             (env, call :: calls))
          param (env, [])
      in
      let li = List.hd (Logic_env.find_all_logic_functions "\\callset") in
      let named_pred =
        {
          pred_name =[];
          pred_loc = p.lexpr_loc;
          pred_content = (Papp(li,[],calls))
        }
      in
      env, Logic_const.pred_of_id_pred (Logic_const.new_predicate named_pred)

    | PLapp ("\\callset", _, _) -> ctxt.error loc "Expect no label for built-in \\callset @."

    | _ -> ctxt.error loc "Unsupported term type in \\rela built-in @."
  in

  let type_predicate  ctxt env p =
    match p.lexpr_node with
    | PLnamed(name,exp) ->
      let pred = ctxt.type_predicate ctxt env exp in
      {pred_name = [name];
       pred_loc = pred.pred_loc;
       pred_content = pred.pred_content}

    | PLapp ("\\callpure", _, _) ->
      ctxt.error loc "A \\callpure is equivalent to a term"

    | PLapp("\\rela",[], param) ->
      if not(Rpp_options.Is_buildin_rela_first.get()) then
        ctxt.error loc
          "@[<v 2>Expected \\rela built-in to be the first element \
           in predicate or in \\forall:@;%a@]"
          Logic_print.print_lexpr p
      else(
        (if List.length param != 2 then(
            ctxt.error loc "Expected 2 parameter for the \\rela built-in: @. @[%a@] @."
              Logic_print.print_lexpr p)
         else(
           let env, callset = check_call_set ctxt env (List.hd param) in
           let pred = typing_context.type_predicate ctxt env (List.hd(List.tl param)) in
           Logic_const.pimplies ~loc:p.lexpr_loc (callset, pred)
         )))

    | PLimplies(({lexpr_node = PLapp("\\callset",_,_)} as set),pred) ->
      if not(Rpp_options.Is_buildin_rela_first.get()) then
        ctxt.error loc
          "Expected \\callset built-in to be the first element in predicat \
           or in \\forall:@. @[%a@] @."
          Logic_print.print_lexpr p
      else(
        let env, callset = check_call_set ctxt env set in
        let pred = typing_context.type_predicate ctxt env pred in
        Logic_const.pimplies ~loc:p.lexpr_loc (callset, pred)
      )

    | PLapp("\\callset",_,_) ->
      ctxt.error loc "Built-in \\callset must be the first element in an implication: @. @[%a@] @."
        Logic_print.print_lexpr p

    | PLforall(_) -> typing_context.type_predicate ctxt env p

    | PLapp ("\\rela", _, _) -> ctxt.error loc "Expect no label for built-in \\rela: @. @[%a@] @."
                                  Logic_print.print_lexpr p
    | _ -> Rpp_options.Is_buildin_rela_first.set(false); typing_context.type_predicate ctxt env p
  in

  let ctxt = { typing_context with type_term ;type_predicate} in
  match l with
  | p ::[] -> Rpp_options.Is_buildin_rela_first.set(true);
    let acsl_pred = Ext_preds[ctxt.type_predicate ctxt ctxt.pre_state p] in
    Hashtbl.clear id_hash;
    acsl_pred
  | _ -> typing_context.error loc "expecting one predicate in relational clause @."

let () =
  Acsl_extension.register_global ~plugin:"rpp" "relational" type_relational true
  (* Acsl_extension.register_behavior "relational" type_relational true *)