logic_parser.mly

/**************************************************************************/
/*                                                                        */
/*  This file is part of Frama-C.                                         */
/*                                                                        */
/*  Copyright (C) 2007-2020                                               */
/*    CEA   (Commissariat à l'énergie atomique et aux énergies            */
/*           alternatives)                                                */
/*    INRIA (Institut National de Recherche en Informatique et en         */
/*           Automatique)                                                 */
/*                                                                        */
/*  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).            */
/*                                                                        */
/**************************************************************************/

/* Grammar for C annotations */

%{

  open Cil_types
  open Logic_ptree
  open Logic_utils

  let loc () =
    Cil_datatype.Location.of_lexing_loc
      (symbol_start_pos (), symbol_end_pos ())
  let lexeme_start nb =
    Cil_datatype.Position.of_lexing_pos (Parsing.rhs_start_pos nb)
  let lexeme_end nb =
    Cil_datatype.Position.of_lexing_pos (Parsing.rhs_end_pos nb)
  let lexeme_loc nb = (lexeme_start nb, lexeme_end nb)

  let info x = { lexpr_node = x; lexpr_loc = loc () }
  let loc_info loc x = { lexpr_node = x; lexpr_loc = loc }
  let loc_start x = fst x.lexpr_loc
  let loc_end x = snd x.lexpr_loc

  (* Normalize p1 && (p2 && p3) into (p1 && p2) && p3 *)
  let rec pland p1 p2 =
    match p2.lexpr_node with
      | PLand (p3,p4) ->
        let loc = (loc_start p1, loc_end p3) in
        PLand(loc_info loc (pland p1 p3),p4)
      | _ -> PLand(p1,p2)

  let rec plor p1 p2 =
    match p2.lexpr_node with
      | PLor(p3,p4) ->
        let loc = (loc_start p1, loc_end p3) in
        PLor(loc_info loc (plor p1 p3),p4)
      | _ -> PLor(p1,p2)

  let clause_order i name1 name2 =
    raise
      (Not_well_formed
         (lexeme_loc i,
          "wrong order of clause in contract: "
          ^ name1 ^ " after " ^ name2 ^ "."))

  let missing i token next_token =
    raise
      (Not_well_formed
         (lexeme_loc i,
          Format.asprintf "expecting '%s' before %s" token next_token))

  type sense_of_relation = Unknown | Disequal | Less | Greater

  let check_empty (loc,msg) l =
    match l with
        [] -> ()
      | _ -> raise (Not_well_formed (loc,msg))

  let relation_sense rel sense =
    match rel, sense with
      | Eq, (Unknown|Greater|Less) -> sense, true
      | Neq, Unknown -> Disequal, false (* No chain of disequality for now*)
      | (Gt|Ge), (Unknown|Greater) -> Greater, true
      | (Lt|Le), (Unknown|Less) -> Less, true
      | _ -> sense, false

  let type_variables_stack = Stack.create ()

  let enter_type_variables_scope l =
    List.iter Logic_env.add_typename l;
    Stack.push l type_variables_stack

  let exit_type_variables_scope () =
    let l = Stack.pop type_variables_stack in
    List.iter Logic_env.remove_typename l

  let rt_type = ref false

  let set_rt_type () = rt_type:= true

  let reset_rt_type () = rt_type:=false

  let is_rt_type () = !rt_type

  let loc_decl d = { decl_node = d; decl_loc = loc () }

  let concat_froms a1 a2 =
    let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
    (* NB: the following has an horrible complexity, but the order of
       clauses in the input is preserved. *)
    let concat_one acc (_,f2 as p)  =
      try
        let (_,f1) = List.find (compare_pair p) acc
        in
        match (f1, f2) with
          | _,FromAny ->
            (* the new fundeps does not give more information than the one
               which is already present. Just ignore it.
             *)
           acc
          | FromAny, _ ->
              (* the new fundeps is strictly more precise than the old one.
                 We replace the old dependency by the new one, but keep
                 the location at its old place in the list. This ensures
                 that we get the exact same clause if we try to
                 link the original contract with its pretty-printed version. *)
              Extlib.replace compare_pair p acc
          | From _, From _ ->
            (* we keep the two functional dependencies,
               as they have to be proved separately. *)
            acc @ [p]
      with Not_found -> acc @ [p]
    in List.fold_left concat_one a1 a2

  let concat_allocation fa1 fa2 =
    match fa1,fa2 with
      | FreeAllocAny,_ -> fa2
      | _,FreeAllocAny -> fa1
      | FreeAlloc(f1,a1),FreeAlloc(f2,a2) -> FreeAlloc(f2@f1,a2@a1)

  (* a1 represents the assigns _after_ the current clause a2. *)
  let concat_assigns a1 a2 =
    match a1,a2 with
        WritesAny,a -> Writes (concat_froms [] a)
      | Writes [], [] -> a1
      | Writes [], _  | Writes _, [] ->
        raise (
          Not_well_formed (loc(),"Mixing \\nothing and a real location"))
      | Writes a1, a2 -> Writes (concat_froms a2 a1)

  let concat_loop_assigns_allocation annots bhvs2 a2 fa2=
    (* NB: this is supposed to merge assigns related to named behaviors, in
       case of annotation like
       for a,b: assigns x,y;
       for b,c: assigns z,t;
       DO NOT CALL this function for loop assigns not attached to specific
       behaviors.
     *)
    assert (bhvs2 <> []);
    if fa2 == FreeAllocAny && a2 == WritesAny
    then annots
    else
    let split l1 l2 =
      let treat_one (only1,both,only2) x =
        if List.mem x l1 then
          (Extlib.filter_out (fun y -> x=y) only1,x::both,only2)
        else (only1,both,x::only2)
      in List.fold_left treat_one (l1,[],[]) l2
    in
    let treat_one ca (bhvs2,acc) =
      match ca,a2,fa2 with
          (AAssigns(bhvs1,a1)),(Writes a2),_ ->
            let (only1,both,only2) = split bhvs1 bhvs2 in
            (match both with
              | [] -> bhvs2, ca::acc
              | _ ->
                let common_annot = AAssigns(both,concat_assigns a1 a2) in
                let annots =
                  match only1 with
                    | [] -> common_annot :: acc
                    | _ -> AAssigns(only1,a1) :: common_annot :: acc
                in only2,annots)
        | (AAllocation(bhvs1,fa1)),_,(FreeAlloc _) ->
           let (only1,both,only2) = split bhvs1 bhvs2 in
            (match both with
              | [] -> bhvs2, ca::acc
              | _ ->
                let common_annot =
                  AAllocation(both,concat_allocation fa1 fa2)
                in
                let annots =
                  match only1 with
                    | [] -> common_annot :: acc
                    | _ -> AAllocation(only1,fa1) :: common_annot :: acc
                in only2,annots)
         | _,_,_ -> bhvs2,ca::acc
    in