infer_clone/infer/src/clang/cTL.ml

(*
 * Copyright (c) 2016-present, Facebook, Inc.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

open! IStd
open Ctl_parser_types
module L = Logging

(* This module defines a language to define checkers. These checkers
   are intepreted over the AST of the program. A checker is defined by a
   CTL formula which express a condition saying when the checker should
    report a problem *)

(** Transition labels used for example to switch from decl to stmt *)
type transitions =
  | AccessorForProperty of ALVar.alexp  (** decl to decl *)
  | Body  (** decl to stmt *)
  | FieldName of ALVar.alexp  (** stmt to stmt, decl to decl *)
  | Fields  (** stmt to stmt, decl to decl *)
  | InitExpr  (** decl to stmt *)
  | Super  (** decl to decl *)
  | ParameterName of ALVar.alexp  (** stmt to stmt, decl to decl *)
  | ParameterPos of ALVar.alexp  (** stmt to stmt, decl to decl *)
  | Parameters  (** stmt to stmt, decl to decl *)
  | Cond
  | PointerToDecl  (** stmt to decl *)
  | Protocol  (** decl to decl *)
[@@deriving compare]

let is_transition_to_successor trans =
  match trans with
  | Body | InitExpr | FieldName _ | Fields | ParameterName _ | ParameterPos _ | Parameters | Cond ->
      true
  | Super | PointerToDecl | Protocol | AccessorForProperty _ ->
      false


(* In formulas below prefix
   "E" means "exists a path"
   "A" means "for all path" *)

type t =
  (* A ctl formula *)
  | True
  | False
  (* not really necessary but it makes it evaluation faster *)
  | Atomic of CPredicates.t
  | Not of t
  | And of t * t
  | Or of t * t
  | Implies of t * t
  | InNode of ALVar.alexp list * t
  | AX of transitions option * t
  | EX of transitions option * t
  | AF of transitions option * t
  | EF of transitions option * t
  | AG of transitions option * t
  | EG of transitions option * t
  | AU of transitions option * t * t
  | EU of transitions option * t * t
  | EH of ALVar.alexp list * t
  | ET of ALVar.alexp list * transitions option * t
[@@deriving compare]

let equal = [%compare.equal : t]

let has_transition phi =
  match phi with
  | True
  | False
  | Atomic _
  | Not _
  | And (_, _)
  | Or (_, _)
  | Implies (_, _)
  | InNode (_, _)
  | EH (_, _) ->
      false
  | AX (trans_opt, _)
  | AF (trans_opt, _)
  | AG (trans_opt, _)
  | AU (trans_opt, _, _)
  | EX (trans_opt, _)
  | EF (trans_opt, _)
  | EG (trans_opt, _)
  | EU (trans_opt, _, _)
  | ET (_, trans_opt, _) ->
      Option.is_some trans_opt


(* "set" clauses are used for defining mandatory variables that will be used
   by when reporting issues: eg for defining the condition.

   "desc" clauses are used for defining the error message,
   the suggestion, the severity.

   "let" clauses are used to define temporary formulas which are then
   used to abbreviate the another formula. For example

   let f = a And B

   set formula  = f OR f

   set message = "bla"

*)

type clause =
  | CLet of ALVar.formula_id * ALVar.t list * t
  (* Let clause: let id = definifion;  *)
  | CSet of ALVar.keyword * t
  (* Set clause: set id = definition *)
  | CDesc of ALVar.keyword * string
  (* Description clause eg: set message = "..." *)
  | CPath of [`WhitelistPath | `BlacklistPath] * ALVar.t list

type ctl_checker =
  {id: string; (* Checker's id *) definitions: clause list (* A list of let/set definitions *)}

type al_file =
  { import_files: string list
  ; global_macros: clause list
  ; global_paths: (string * ALVar.alexp list) list
  ; checkers: ctl_checker list }

let equal_ast_node = Poly.( = )

module Debug = struct
  let pp_transition fmt trans_opt =
    let pp_aux fmt trans =
      match trans with
      | AccessorForProperty kind ->
          Format.pp_print_string fmt ("AccessorForProperty " ^ ALVar.alexp_to_string kind)
      | Body ->
          Format.pp_print_string fmt "Body"
      | FieldName name ->
          Format.pp_print_string fmt ("FieldName " ^ ALVar.alexp_to_string name)
      | Fields ->
          Format.pp_print_string fmt "Fields"
      | InitExpr ->
          Format.pp_print_string fmt "InitExpr"
      | Super ->
          Format.pp_print_string fmt "Super"
      | ParameterName name ->
          Format.pp_print_string fmt ("ParameterName " ^ ALVar.alexp_to_string name)
      | ParameterPos pos ->
          Format.pp_print_string fmt ("ParameterPos " ^ ALVar.alexp_to_string pos)
      | Parameters ->
          Format.pp_print_string fmt "Parameters"
      | Cond ->
          Format.pp_print_string fmt "Cond"
      | Protocol ->
          Format.pp_print_string fmt "Protocol"
      | PointerToDecl ->
          Format.pp_print_string fmt "PointerToDecl"
    in
    match trans_opt with Some trans -> pp_aux fmt trans | None -> Format.pp_print_char fmt '_'


  (* a flag to print more or less in the dotty graph *)
  let full_print = true

  let rec pp_formula fmt phi =
    let nodes_to_string nl = List.map ~f:ALVar.alexp_to_string nl in
    match phi with
    | True ->
        Format.pp_print_string fmt "True"
    | False ->
        Format.pp_print_string fmt "False"
    | Atomic p ->
        CPredicates.pp_predicate fmt p
    | Not phi ->
        if full_print then Format.fprintf fmt "NOT(%a)" pp_formula phi
        else Format.pp_print_string fmt "NOT(...)"
    | And (phi1, phi2) ->
        if full_print then Format.fprintf fmt "(%a AND %a)" pp_formula phi1 pp_formula phi2
        else Format.pp_print_string fmt "(... AND ...)"
    | Or (phi1, phi2) ->
        if full_print then Format.fprintf fmt "(%a OR %a)" pp_formula phi1 pp_formula phi2
        else Format.pp_print_string fmt "(... OR ...)"
    | Implies (phi1, phi2) ->
        Format.fprintf fmt "(%a ==> %a)" pp_formula phi1 pp_formula phi2
    | InNode (nl, phi) ->
        Format.fprintf fmt "IN-NODE %a: (%a)"
          (Pp.comma_seq Format.pp_print_string)
          (nodes_to_string nl) pp_formula phi
    | AX (trs, phi) ->
        Format.fprintf fmt "AX[->%a](%a)" pp_transition trs pp_formula phi
    | EX (trs, phi) ->
        Format.fprintf fmt "EX[->%a](%a)" pp_transition trs pp_formula phi
    | AF (trs, phi) ->
        Format.fprintf fmt "AF[->%a](%a)" pp_transition trs pp_formula phi
    | EF (trs, phi) ->
        Format.fprintf fmt "EF[->%a](%a)" pp_transition trs pp_formula phi
    | AG (trs, phi) ->
        Format.fprintf fmt "AG[->%a](%a)" pp_transition trs pp_formula phi
    | EG (trs, phi) ->
        Format.fprintf fmt "EG[->%a](%a)" pp_transition trs pp_formula phi
    | AU (trs, phi1, phi2) ->
        Format.fprintf fmt "A[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2
    | EU (trs, phi1, phi2) ->
        Format.fprintf fmt "E[->%a][%a UNTIL %a]" pp_transition trs pp_formula phi1 pp_formula phi2
    | EH (arglist, phi) ->
        Format.fprintf fmt "EH[%a](%a)"
          (Pp.comma_seq Format.pp_print_string)
          (nodes_to_string arglist) pp_formula phi
    | ET (arglist, trans, phi) ->
        Format.fprintf fmt "ET[%a][%a](%a)"
          (Pp.comma_seq Format.pp_print_string)
          (nodes_to_string arglist) pp_transition trans pp_formula phi


  let pp_ast ~ast_node_to_highlight ?(prettifier= Fn.id) fmt root =
    let pp_node_info fmt an =
      let name = Ctl_parser_types.ast_node_name an in
      let typ = Ctl_parser_types.ast_node_type an in
      let cast_kind = Ctl_parser_types.ast_node_cast_kind an in
      Format.fprintf fmt " %s %s %s" name typ cast_kind
    in
    let rec pp_children pp_node wrapper fmt level nodes =
      match nodes with
      | [] ->
          ()
      | node :: nodes ->
          pp_node fmt (wrapper node) level "|-" ;
          pp_children pp_node wrapper fmt level nodes
    in
    let rec pp_ast_aux fmt root level prefix =
      let get_node_name (an: ast_node) =
        match an with
        | Stmt stmt ->
            Clang_ast_proj.get_stmt_kind_string stmt
        | Decl decl ->
            Clang_ast_proj.get_decl_kind_string decl
      in
      let should_highlight =
        match (root, ast_node_to_highlight) with
        | Stmt r, Stmt n ->
            phys_equal r n
        | Decl r, Decl n ->
            phys_equal r n
        | _ ->
            false
      in
      let node_name =
        let node_name = get_node_name root in
        if should_highlight then prettifier node_name else node_name
      in
      let spaces = String.make (level * String.length prefix) ' ' in
      let next_level = level + 1 in
      Format.fprintf fmt "%s%s%s %a@\n" spaces prefix node_name pp_node_info root ;
      match root with
      | Stmt (DeclStmt (_, stmts, ([VarDecl _] as var_decl))) ->
          (* handling special case of DeclStmt with VarDecl: emit the VarDecl node
              then emit the statements in DeclStmt as children of VarDecl. This is
              because despite being equal, the statements inside VarDecl and those
              inside DeclStmt belong to different instances, hence they fail the
              phys_equal check that should colour them *)
          pp_children pp_ast_aux (fun n -> Decl n) fmt next_level var_decl ;
          pp_stmts fmt (next_level + 1) stmts
      | Stmt stmt ->
          let _, stmts = Clang_ast_proj.get_stmt_tuple stmt in
          pp_stmts fmt next_level stmts
      | Decl decl ->
          let decls =
            Clang_ast_proj.get_decl_context_tuple decl |> Option.map ~f:(fun (decls, _) -> decls)
            |> Option.value ~default:[]
          in
          pp_decls fmt next_level decls
    and pp_stmts fmt level stmts = pp_children pp_ast_aux (fun n -> Stmt n) fmt level stmts
    and pp_decls fmt level decls = pp_children pp_ast_aux (fun n -> Decl n) fmt level decls in
    pp_ast_aux fmt root 0 ""


  module EvaluationTracker = struct
    exception Empty_stack of string

    type eval_result = Eval_undefined | Eval_true | Eval_false

    type content =
      { ast_node: ast_node
      ; phi: t
      ; lcxt: CLintersContext.context
      ; eval_result: eval_result
      ; witness: ast_node option }

    type eval_node = {id: int; content: content}

    type tree = Tree of eval_node * tree list

    type ast_node_to_display =
      (* the node can be used to describe further sub calls in the evaluation stack *)
      | Carry_forward of ast_node
      (* the node cannot be further used to describe sub calls in the evaluation stack *)
      | Last_occurrence of ast_node

    type t =
      { next_id: int
      ; eval_stack: (tree * ast_node_to_display) Stack.t
      ; forest: tree list
      ; breakpoint_line: int option
      ; debugger_active: bool }

    let create_content ast_node phi lcxt =
      {ast_node; phi; eval_result= Eval_undefined; lcxt; witness= None}


    let create source_file =
      let breakpoint_token = "INFER_BREAKPOINT" in
      let breakpoint_line =
        In_channel.read_lines (SourceFile.to_abs_path source_file)
        |> List.findi ~f:(fun _ line -> String.is_substring line ~substring:breakpoint_token)
        |> Option.map ~f:(fun (i, _) -> i + 1)
      in
      {next_id= 0; eval_stack= Stack.create (); forest= []; breakpoint_line; debugger_active= false}


    let explain t ~eval_node ~ast_node_to_display =
      let line_number an =
        let line_of_source_range (sr: Clang_ast_t.source_range) =
          let loc_info, _ = sr in
          loc_info.sl_line
        in
        match an with
        | Stmt stmt ->
            let stmt_info, _ = Clang_ast_proj.get_stmt_tuple stmt in
            line_of_source_range stmt_info.si_source_range
        | Decl decl ->
            let decl_info = Clang_ast_proj.get_decl_tuple decl in
            line_of_source_range decl_info.di_source_range
      in
      let stop_and_explain_step () =
        let highlight_style =
          match eval_node.content.eval_result with
          | Eval_undefined ->
              ANSITerminal.[Bold]
          | Eval_true ->
              ANSITerminal.[Bold; green]
          | Eval_false ->
              ANSITerminal.[Bold; red]
        in
        let ast_node_to_highlight = eval_node.content.ast_node in
        let ast_root, is_last_occurrence =
          match ast_node_to_display with
          | Carry_forward n ->
              (n, false)
          | Last_occurrence n ->
              (n, true)
        in
        let witness_str =
          match eval_node.content.witness with
          | Some witness ->
              "\n- witness: " ^ Ctl_parser_types.ast_node_kind witness ^ " "
              ^ Ctl_parser_types.ast_node_name witness
          | None ->
              ""
        in
        let ast_str =
          Format.asprintf "%a %s"
            (pp_ast ~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s"))
            ast_root witness_str
        in
        L.progress "@\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s@\n"
          eval_node.id (Stack.length t.eval_stack)
          (Option.value_map ~default:"Unknown" ~f:string_of_int (line_number ast_node_to_highlight)) ;
        let is_eval_result_undefined =
          match eval_node.content.eval_result with Eval_undefined -> true | _ -> false
        in
        if is_last_occurrence && is_eval_result_undefined then
          L.progress "From this step, a transition to a different part of the AST may follow.@\n" ;
        let phi_str = Format.asprintf "%a" pp_formula eval_node.content.phi in
        L.progress "CTL Formula: %s@\n@\n" phi_str ;
        L.progress "%s@\n" ast_str ;
        let quit_token = "q" in
        L.progress "Press Enter to continue or type %s to quit... @?" quit_token ;
        match In_channel.input_line_exn In_channel.stdin |> String.lowercase with
        | s when String.equal s quit_token ->
            L.exit 0
        | _ ->
            (* Remove the line at the bottom of terminal with the debug instructions *)
            let open ANSITerminal in
            (* move one line up, as current line is the one generated by pressing enter *)
            move_cursor 0 (-1) ;
            move_bol () ;
            (* move to the beginning of the line *)
            erase Below
        (* erase what follows the cursor's position *)
      in
      match (t.debugger_active, t.breakpoint_line, line_number eval_node.content.ast_node) with
      | false, Some break_point_ln, Some ln when ln >= break_point_ln ->
          L.progress "Attaching debugger at line %d" ln ;
          stop_and_explain_step () ;
          {t with debugger_active= true}
      | true, _, _ ->
          stop_and_explain_step () ; t
      | _ ->
          t


    let eval_begin t content =
      let node = {id= t.next_id; content} in
      let create_subtree root = Tree (root, []) in
      let subtree' = create_subtree node in
      let ast_node_from_previous_call =
        match Stack.top t.eval_stack with
        | Some (_, Last_occurrence _) ->
            content.ast_node
        | Some (_, Carry_forward an) ->
            an
        | None ->
            content.ast_node
      in
      let ast_node_to_display =
        if has_transition content.phi then Last_occurrence ast_node_from_previous_call
        else Carry_forward ast_node_from_previous_call
      in
      Stack.push t.eval_stack (subtree', ast_node_to_display) ;
      let t' = explain t ~eval_node:node ~ast_node_to_display in
      {t' with next_id= t.next_id + 1}


    let eval_end t result =
      let result_bool = Option.is_some result in
      let eval_result_of_bool = function true -> Eval_true | false -> Eval_false in
      if Stack.is_empty t.eval_stack then
        raise (Empty_stack "Unbalanced number of eval_begin/eval_end invocations") ;
      let evaluated_tree, eval_node, ast_node_to_display =
        match Stack.pop_exn t.eval_stack
        with Tree (({id= _; content} as eval_node), children), ast_node_to_display ->
          let content' =
            {content with eval_result= eval_result_of_bool result_bool; witness= result}
          in
          let eval_node' = {eval_node with content= content'} in
          (Tree (eval_node', children), eval_node', ast_node_to_display)
      in
      let t' = explain t ~eval_node ~ast_node_to_display in
      let forest' =
        if Stack.is_empty t'.eval_stack then evaluated_tree :: t'.forest
        else
          let parent =
            match Stack.pop_exn t'.eval_stack with Tree (node, children), ntd ->
              (Tree (node, evaluated_tree :: children), ntd)
          in
          Stack.push t'.eval_stack parent ; t'.forest
      in
      {t' with forest= forest'}


    module DottyPrinter = struct
      let dotty_of_ctl_evaluation t =
        let buffer_content buf =
          let result = Buffer.contents buf in
          Buffer.reset buf ; result
        in
        let dotty_of_tree cluster_id tree =
          let get_root tree = match tree with Tree (root, _) -> root in
          let get_children tree = match tree with Tree (_, children) -> List.rev children in
          (* shallow: emit dotty about root node and edges to its children *)
          let shallow_dotty_of_tree tree =
            let root_node = get_root tree in
            let children = get_children tree in
            let edge child_node =
              if equal_ast_node root_node.content.ast_node child_node.content.ast_node then
                Printf.sprintf "%d -> %d [style=dotted]" root_node.id child_node.id
              else Printf.sprintf "%d -> %d [style=bold]" root_node.id child_node.id
            in
            let color =
              match root_node.content.eval_result with
              | Eval_true ->
                  "green"
              | Eval_false ->
                  "red"
              | _ ->
                  L.(die InternalError) "Tree is not fully evaluated"
            in
            let label =
              let string_of_lcxt c =
                match c.CLintersContext.et_evaluation_node with
                | Some s ->
                    "et_evaluation_node = " ^ s
                | _ ->
                    "et_evaluation_node = NONE"
              in
              let string_of_ast_node an =
                match an with
                | Stmt stmt ->
                    Clang_ast_proj.get_stmt_kind_string stmt
                | Decl decl ->
                    Clang_ast_proj.get_decl_kind_string decl
              in
              let smart_string_of_formula phi =
                let num_children = List.length children in
                match phi with
                | And _ when Int.equal num_children 2 ->
                    "(...) AND (...)"
                | Or _ when Int.equal num_children 2 ->
                    "(...) OR (...)"
                | Implies _ when Int.equal num_children 2 ->
                    "(...) ==> (...)"
                | Not _ ->
                    "NOT(...)"
                | _ ->
                    Format.asprintf "%a" pp_formula phi
              in
              Format.sprintf "(%d)\\n%s\\n%s\\n%s" root_node.id
                (Escape.escape_dotty (string_of_ast_node root_node.content.ast_node))
                (Escape.escape_dotty (string_of_lcxt root_node.content.lcxt))
                (Escape.escape_dotty (smart_string_of_formula root_node.content.phi))
            in
            let edges =
              let buf = Buffer.create 16 in
              List.iter
                ~f:(fun subtree -> Buffer.add_string buf (edge (get_root subtree) ^ "\n"))
                children ;
              buffer_content buf
            in
            Printf.sprintf "%d [label=\"%s\" shape=box color=%s]\n%s\n" root_node.id label color
              edges
          in
          let rec traverse buf tree =
            Buffer.add_string buf (shallow_dotty_of_tree tree) ;
            List.iter ~f:(traverse buf) (get_children tree)
          in
          let buf = Buffer.create 16 in
          traverse buf tree ;
          Printf.sprintf "subgraph cluster_%d {\n%s\n}" cluster_id (buffer_content buf)
        in
        let buf = Buffer.create 16 in
        List.iteri
          ~f:(fun cluster_id tree -> Buffer.add_string buf (dotty_of_tree cluster_id tree ^ "\n"))
          (List.rev t.forest) ;
        Printf.sprintf "digraph CTL_Evaluation {\n%s\n}\n" (buffer_content buf)
    end
  end
end

let print_checker c =
  L.(debug Linters Medium) "@\n-------------------- @\n" ;
  L.(debug Linters Medium) "@\nChecker name: %s@\n" c.id ;
  List.iter
    ~f:(fun d ->
      match d with
      | CSet (keyword, phi) ->
          let cn_str = ALVar.keyword_to_string keyword in
          L.(debug Linters Medium) "    %s=  @\n    %a@\n@\n" cn_str Debug.pp_formula phi
      | CLet (exp, _, phi) ->
          let cn_str = ALVar.formula_id_to_string exp in
          L.(debug Linters Medium) "    %s=  @\n    %a@\n@\n" cn_str Debug.pp_formula phi
      | CDesc (keyword, s) ->
          let cn_str = ALVar.keyword_to_string keyword in
          L.(debug Linters Medium) "    %s=  @\n    %s@\n@\n" cn_str s
      | CPath (paths_keyword, paths) ->
          let keyword =
            match paths_keyword with `WhitelistPath -> "whitelist_path" | _ -> "blacklist_path"
          in
          let paths_str = String.concat ~sep:"," (List.map ~f:ALVar.alexp_to_string paths) in
          L.(debug Linters Medium) "    %s=  @\n    %s@\n@\n" keyword paths_str )
    c.definitions ;
  L.(debug Linters Medium) "@\n-------------------- @\n"


let ctl_evaluation_tracker = ref None

let create_ctl_evaluation_tracker source_file =
  match (Config.linters_developer_mode, !ctl_evaluation_tracker) with
  | true, None ->
      ctl_evaluation_tracker := Some (Debug.EvaluationTracker.create source_file)
  | true, _ ->
      L.(die InternalError) "A CTL evaluation tracker has already been created"
  | _ ->
      ()


let debug_create_payload ast_node phi lcxt =
  match !ctl_evaluation_tracker with
  | Some _ ->
      Some (Debug.EvaluationTracker.create_content ast_node phi lcxt)
  | None ->
      None


let debug_eval_begin payload =
  match (!ctl_evaluation_tracker, payload) with
  | Some tracker, Some payload ->
      ctl_evaluation_tracker := Some (Debug.EvaluationTracker.eval_begin tracker payload)
  | _ ->
      ()


let debug_eval_end result =
  match !ctl_evaluation_tracker with
  | Some tracker ->
      ctl_evaluation_tracker := Some (Debug.EvaluationTracker.eval_end tracker result)
  | None ->
      ()


let save_dotty_when_in_debug_mode source_file =
  match !ctl_evaluation_tracker with
  | Some tracker ->
      let dotty_dir = Config.results_dir ^/ Config.lint_dotty_dir_name in
      Utils.create_dir dotty_dir ;
      let source_file_basename = Filename.basename (SourceFile.to_abs_path source_file) in
      let file = dotty_dir ^/ source_file_basename ^ ".dot" in
      let dotty = Debug.EvaluationTracker.DottyPrinter.dotty_of_ctl_evaluation tracker in
      Utils.with_file_out file ~f:(fun oc -> Out_channel.output_string oc dotty)
  | _ ->
      ()


(* Helper functions *)
(* given a decl returns a stmt such that decl--->stmt via label trs *)
let transition_decl_to_stmt d trs =
  let open Clang_ast_t in
  let temp_res =
    match (trs, d) with
    | Body, ObjCMethodDecl (_, _, omdi) ->
        [omdi.omdi_body]
    | Body, FunctionDecl (_, _, _, fdi)
    | Body, CXXMethodDecl (_, _, _, fdi, _)
    | Body, CXXConstructorDecl (_, _, _, fdi, _)
    | Body, CXXConversionDecl (_, _, _, fdi, _)
    | Body, CXXDestructorDecl (_, _, _, fdi, _) ->
        [fdi.fdi_body]
    | Body, BlockDecl (_, bdi) ->
        [bdi.bdi_body]
    | InitExpr, VarDecl (_, _, _, vdi) ->
        [vdi.vdi_init_expr]
    | InitExpr, ObjCIvarDecl (_, _, _, fldi, _)
    | InitExpr, FieldDecl (_, _, _, fldi)
    | InitExpr, ObjCAtDefsFieldDecl (_, _, _, fldi) ->
        [fldi.fldi_init_expr]
    | InitExpr, CXXMethodDecl (_, _, _, _, mdi)
    | InitExpr, CXXConstructorDecl (_, _, _, _, mdi)
    | InitExpr, CXXConversionDecl (_, _, _, _, mdi)
    | InitExpr, CXXDestructorDecl (_, _, _, _, mdi) ->
        List.map ~f:(fun ci -> ci.xci_init_expr) mdi.xmdi_cxx_ctor_initializers
    | InitExpr, EnumConstantDecl (_, _, _, ecdi) ->
        [ecdi.ecdi_init_expr]
    | _, _ ->
        [None]
  in
  List.fold ~f:(fun l e -> match e with Some st -> Stmt st :: l | _ -> l) temp_res ~init:[]


let transition_decl_to_decl_via_accessor_for_property d desired_kind =
  let open Clang_ast_t in
  let find_property_for_accessor decl_opt predicate =
    let decl_matches decl =
      match decl with ObjCPropertyDecl (_, _, opdi) -> predicate opdi | _ -> false
    in
    match decl_opt with
    | Some (ObjCCategoryImplDecl (_, _, _, _, ocidi)) ->
        let category_decls =
          match CAst_utils.get_decl_opt_with_decl_ref ocidi.ocidi_category_decl with
          | Some (ObjCCategoryDecl (_, _, decls, _, _)) ->
              List.filter ~f:decl_matches decls
          | _ ->
              []
        in
        let class_decls =
          match CAst_utils.get_decl_opt_with_decl_ref ocidi.ocidi_class_interface with
          | Some (ObjCInterfaceDecl (_, _, decls, _, _)) ->
              List.filter ~f:decl_matches decls
          | _ ->
              []
        in
        category_decls @ class_decls
    | Some (ObjCImplementationDecl (_, _, _, _, oidi)) -> (
      match CAst_utils.get_decl_opt_with_decl_ref oidi.oidi_class_interface with
      | Some (ObjCInterfaceDecl (_, _, decls, _, _)) ->
          List.filter ~f:decl_matches decls
      | _ ->
          [] )
    | _ ->
        []
  in
  match d with
  | ObjCMethodDecl (di, method_decl_name, mdi)
    -> (
      (* infer whether this method may be a getter or setter (or
         neither) from its argument list *)
      let num_params = List.length mdi.omdi_parameters in
      let actual_kind, accessor_decl_ref_of_property_decl_info =
        match num_params with
        | 0 ->
            ("getter", fun opdi -> opdi.opdi_getter_method)
        | 1 ->
            ("setter", fun opdi -> opdi.opdi_setter_method)
        | _ ->
            ("", fun _ -> None)
      in
      if not (ALVar.compare_str_with_alexp actual_kind desired_kind) then []
      else
        match CAst_utils.get_decl_opt_with_decl_ref mdi.omdi_property_decl with
        | Some property_decl ->
            (* clang handles most cases: property declarations with
               accessor method declarations in the inferface; property
               declarations in base classes; etc. *)
            [Decl property_decl]
        | None ->
            (* search the interface for a matching property *)
            let name_check opdi =
              match accessor_decl_ref_of_property_decl_info opdi with
              | None ->
                  false
              | Some dr ->
                match dr.dr_name with
                | Some ni ->
                    String.equal method_decl_name.ni_name ni.ni_name
                | _ ->
                    false
            in
            let impl_decl_opt = CAst_utils.get_decl_opt di.di_parent_pointer in
            List.map ~f:(fun x -> Decl x) (find_property_for_accessor impl_decl_opt name_check) )
  | _ ->
      []


let transition_decl_to_decl_via_super d =
  let decl_opt_to_ast_node_opt d_opt = match d_opt with Some d' -> [Decl d'] | None -> [] in
  let do_ObjCImplementationDecl d =
    match CAst_utils.get_impl_decl_info d with
    | Some idi ->
        decl_opt_to_ast_node_opt (CAst_utils.get_super_ObjCImplementationDecl idi)
    | None ->
        []
  in
  match d with
  | Clang_ast_t.ObjCImplementationDecl _ ->
      do_ObjCImplementationDecl d
  | Clang_ast_t.ObjCInterfaceDecl (_, _, _, _, idi) ->
      decl_opt_to_ast_node_opt (CAst_utils.get_decl_opt_with_decl_ref idi.otdi_super)
  | _ ->
      []


let transition_decl_to_decl_via_protocol d =
  let open Clang_ast_t in
  let get_nodes dr =
    match CAst_utils.get_decl dr.dr_decl_pointer with Some d -> Some (Decl d) | None -> None
  in
  match d with
  | Clang_ast_t.ObjCProtocolDecl (_, _, _, _, opdi) ->
      List.filter_map ~f:get_nodes opdi.opcdi_protocols
  | _ ->
      []


let transition_stmt_to_stmt_via_condition st =
  let open Clang_ast_t in
  match st with
  | IfStmt (_, _ :: _ :: cond :: _)
  | ConditionalOperator (_, cond :: _, _)
  | ForStmt (_, [_; _; cond; _; _])
  | WhileStmt (_, [_; cond; _]) ->
      [Stmt cond]
  | _ ->
      []


let transition_stmt_to_decl_via_pointer stmt =
  let open Clang_ast_t in
  match stmt with
  | ObjCMessageExpr (_, _, _, obj_c_message_expr_info) -> (
    match CAst_utils.get_decl_opt obj_c_message_expr_info.Clang_ast_t.omei_decl_pointer with
    | Some decl ->
        [Decl decl]
    | None ->
        [] )
  | DeclRefExpr (_, _, _, decl_ref_expr_info) -> (
    match CAst_utils.get_decl_opt_with_decl_ref decl_ref_expr_info.Clang_ast_t.drti_decl_ref with
    | Some decl ->
        [Decl decl]
    | None ->
        [] )
  | _ ->
      []


let transition_via_parameters an =
  let open Clang_ast_t in
  match an with
  | Decl (ObjCMethodDecl (_, _, omdi)) ->
      List.map ~f:(fun d -> Decl d) omdi.omdi_parameters
  | Stmt (ObjCMessageExpr (_, stmt_list, _, _)) ->
      List.map ~f:(fun stmt -> Stmt stmt) stmt_list
  | _ ->
      []


let parameter_of_corresp_name method_name args name =
  let names =
    List.filter (String.split ~on:':' method_name) ~f:(fun label -> not (String.is_empty label))
  in
  match List.zip names args with
  | Some names_args
    -> (
      let names_arg_opt =
        List.find names_args ~f:(fun (arg_label, _) -> ALVar.compare_str_with_alexp arg_label name)
      in
      match names_arg_opt with Some (_, arg) -> Some arg | None -> None )
  | None ->
      None


let parameter_of_corresp_pos args pos =
  let pos_int =
    match pos with ALVar.Const n -> ( try int_of_string n with Failure _ -> -1 ) | _ -> -1
  in
  List.nth args pos_int


let transition_via_specified_parameter ~pos an key =
  let invalid_param_name_use () =
    Logging.die InternalError "Transition ParameterName is only available for ObjC methods"
  in
  let node_opt_to_ast_node_list f arg_stmt_opt =
    match arg_stmt_opt with Some arg -> [f arg] | None -> []
  in
  let apply_decl arg = Decl arg in
  let apply_stmt arg = Stmt arg in
  match an with
  | Stmt (ObjCMessageExpr (_, stmt_list, _, omei)) ->
      let method_name = omei.omei_selector in
      let parameter_of_corresp_key =
        if pos then parameter_of_corresp_pos else parameter_of_corresp_name method_name
      in
      let arg_stmt_opt = parameter_of_corresp_key stmt_list key in
      node_opt_to_ast_node_list apply_stmt arg_stmt_opt
  | Stmt (CallExpr (_, _ :: args, _)) ->
      let parameter_of_corresp_key =
        if pos then parameter_of_corresp_pos else invalid_param_name_use ()
      in
      let arg_stmt_opt = parameter_of_corresp_key args key in
      node_opt_to_ast_node_list apply_stmt arg_stmt_opt
  | Decl (ObjCMethodDecl (_, named_decl_info, omdi)) ->
      let method_name = named_decl_info.ni_name in
      let parameter_of_corresp_key =
        if pos then parameter_of_corresp_pos else parameter_of_corresp_name method_name
      in
      let arg_decl_opt = parameter_of_corresp_key omdi.omdi_parameters key in
      node_opt_to_ast_node_list apply_decl arg_decl_opt
  | Decl (FunctionDecl (_, _, _, fdi))
  | Decl (CXXMethodDecl (_, _, _, fdi, _))
  | Decl (CXXConstructorDecl (_, _, _, fdi, _)) ->
      let parameter_of_corresp_key =
        if pos then parameter_of_corresp_pos else invalid_param_name_use ()
      in
      let arg_decl_opt = parameter_of_corresp_key fdi.fdi_parameters key in
      node_opt_to_ast_node_list apply_decl arg_decl_opt
  | _ ->
      []


let transition_via_parameter_name an name = transition_via_specified_parameter an name ~pos:false

let transition_via_parameter_pos an pos = transition_via_specified_parameter an pos ~pos:true

let transition_via_fields an =
  let open Clang_ast_t in
  match an with
  | Decl (RecordDecl (_, _, _, decls, _, _, _)) | Decl (CXXRecordDecl (_, _, _, decls, _, _, _, _)) ->
      List.filter_map ~f:(fun d -> match d with FieldDecl _ -> Some (Decl d) | _ -> None) decls
  | Stmt (InitListExpr (_, stmts, _)) ->
      List.map ~f:(fun stmt -> Stmt stmt) stmts
  | _ ->
      []


let field_has_name name node =
  match node with
  | Decl (FieldDecl (_, name_info, _, _)) ->
      ALVar.compare_str_with_alexp name_info.Clang_ast_t.ni_name name
  | _ ->
      false


let field_of_name name nodes = List.filter ~f:(field_has_name name) nodes

let field_of_corresp_name_from_init_list_expr name init_nodes (expr_info: Clang_ast_t.expr_info) =
  match CAst_utils.get_decl_from_typ_ptr expr_info.ei_qual_type.qt_type_ptr with
  | Some decl
    -> (
      let fields = transition_via_fields (Decl decl) in
      match List.zip init_nodes fields with
      | Some init_nodes_fields ->
          List.filter ~f:(fun (_, field) -> field_has_name name field) init_nodes_fields
          |> List.map ~f:(fun (node, _) -> node)
      | None ->
          [] )
  | None ->
      []


let transition_via_field_name node name =
  let open Clang_ast_t in
  match node with
  | Decl (RecordDecl _) | Decl (CXXRecordDecl _) ->
      let fields = transition_via_fields node in
      field_of_name name fields
  | Stmt (InitListExpr (_, stmts, expr_info)) ->
      let nodes = List.map ~f:(fun stmt -> Stmt stmt) stmts in
      field_of_corresp_name_from_init_list_expr name nodes expr_info
  | _ ->
      []


(* given a node an returns a list of nodes an' such that an transition to an' via label trans *)
let next_state_via_transition an trans =
  match (an, trans) with
  | Decl d, Super ->
      transition_decl_to_decl_via_super d
  | _, FieldName name ->
      transition_via_field_name an name
  | _, Fields ->
      transition_via_fields an
  | _, Parameters ->
      transition_via_parameters an
  | Decl d, InitExpr | Decl d, Body ->
      transition_decl_to_stmt d trans
  | Decl d, Protocol ->
      transition_decl_to_decl_via_protocol d
  | Stmt st, Cond ->
      transition_stmt_to_stmt_via_condition st
  | Stmt st, PointerToDecl ->
      transition_stmt_to_decl_via_pointer st
  | an, ParameterName name ->
      transition_via_parameter_name an name
  | an, ParameterPos pos ->
      transition_via_parameter_pos an pos
  | Decl d, AccessorForProperty name ->
      transition_decl_to_decl_via_accessor_for_property d name
  | _, _ ->
      []


let choose_one_witness an1 an2 =
  if Ctl_parser_types.ast_node_equal an1 an2 then an1
  else if Ctl_parser_types.is_node_successor_of an1 ~is_successor:an2 then an2
  else an1


let choose_witness_opt witness_opt1 witness_opt2 =
  match (witness_opt1, witness_opt2) with
  | Some witness1, Some witness2 ->
      Some (choose_one_witness witness1 witness2)
  | Some witness, None | None, Some witness ->
      Some witness
  | None, None ->
      None


(* Evaluation of formulas *)
(* evaluate an atomic formula (i.e. a predicate) on a ast node an and a
   linter context lcxt. That is:  an, lcxt |= pred_name(params) *)
let rec eval_Atomic pred_name_ args an lcxt =
  let pred_name = ALVar.formula_id_to_string pred_name_ in
  match (pred_name, args, an) with
  | "call_class_method", [m], an ->
      CPredicates.call_class_method an m
  | "call_function", [m], an ->
      CPredicates.call_function an m
  | "call_instance_method", [m], an ->
      CPredicates.call_instance_method an m
  | "call_method", [m], an ->
      CPredicates.call_method an m
  | "captures_cxx_references", [], _ ->
      CPredicates.captures_cxx_references an
  | "context_in_synchronized_block", [], _ ->
      CPredicates.context_in_synchronized_block lcxt
  | "declaration_has_name", [decl_name], an ->
      CPredicates.declaration_has_name an decl_name
  | "declaration_ref_name", [decl_name], an ->
      CPredicates.declaration_ref_name an decl_name
  | "decl_unavailable_in_supported_ios_sdk", [], an ->
      CPredicates.decl_unavailable_in_supported_ios_sdk lcxt an
  | "class_unavailable_in_supported_ios_sdk", [], an ->
      CPredicates.class_unavailable_in_supported_ios_sdk lcxt an
  | "has_cast_kind", [name], an ->
      CPredicates.has_cast_kind an name
  | "has_type", [typ], an ->
      CPredicates.has_type an typ
  | "has_value", [typ], an ->
      CPredicates.has_value an typ
  | "isa", [classname], an ->
      CPredicates.isa an classname
  | "is_assign_property", [], an ->
      CPredicates.is_assign_property an
  | "is_binop_with_kind", [kind], an ->
      CPredicates.is_binop_with_kind an kind
  | "is_class", [cname], an ->
      CPredicates.is_class an cname
  | "is_const_var", [], an ->
      CPredicates.is_const_expr_var an
  | "is_decl", [], an ->
      CPredicates.is_decl an
  | "is_enum_constant", [cname], an ->
      CPredicates.is_enum_constant an cname
  | "is_enum_constant_of_enum", [name], an ->
      CPredicates.is_enum_constant_of_enum an name
  | "is_global_var", [], an ->
      CPredicates.is_global_var an
  | "is_static_local_var", [], an ->
      CPredicates.is_static_local_var an
  | "is_in_block", [], _ ->
      CPredicates.is_in_block lcxt
  | "is_in_cxx_constructor", [name], _ ->
      CPredicates.is_in_cxx_constructor lcxt name
  | "is_in_cxx_destructor", [name], _ ->
      CPredicates.is_in_cxx_destructor lcxt name
  | "is_in_cxx_method", [name], _ ->
      CPredicates.is_in_cxx_method lcxt name
  | "is_in_function", [name], _ ->
      CPredicates.is_in_function lcxt name
  | "is_in_objc_class_method", [name], _ ->
      CPredicates.is_in_objc_class_method lcxt name
  | "is_in_objc_instance_method", [name], _ ->
      CPredicates.is_in_objc_instance_method lcxt name
  | "is_in_objc_method", [name], _ ->
      CPredicates.is_in_objc_method lcxt name
  | "is_in_objc_interface_named", [name], _ ->
      CPredicates.is_in_objc_interface_named lcxt name
  | "is_in_objc_implementation_named", [name], _ ->
      CPredicates.is_in_objc_implementation_named lcxt name
  | "is_in_objc_class_named", [name], _ ->
      CPredicates.is_in_objc_class_named lcxt name
  | "is_in_objc_subclass_of", [name], _ ->
      CPredicates.is_in_objc_subclass_of lcxt name
  | "is_in_objc_category_interface_on_class_named", [name], _ ->
      CPredicates.is_in_objc_category_interface_on_class_named lcxt name
  | "is_in_objc_category_implementation_on_class_named", [name], _ ->
      CPredicates.is_in_objc_category_implementation_on_class_named lcxt name
  | "is_in_objc_category_on_class_named", [name], _ ->
      CPredicates.is_in_objc_category_on_class_named lcxt name
  | "is_in_objc_category_interface_on_subclass_of", [name], _ ->
      CPredicates.is_in_objc_category_interface_on_subclass_of lcxt name
  | "is_in_objc_category_implementation_on_subclass_of", [name], _ ->
      CPredicates.is_in_objc_category_implementation_on_subclass_of lcxt name
  | "is_in_objc_category_on_subclass_of", [name], _ ->
      CPredicates.is_in_objc_category_on_subclass_of lcxt name
  | "is_in_objc_category_interface_named", [name], _ ->
      CPredicates.is_in_objc_category_interface_named lcxt name
  | "is_in_objc_category_implementation_named", [name], _ ->
      CPredicates.is_in_objc_category_implementation_named lcxt name
  | "is_in_objc_category_named", [name], _ ->
      CPredicates.is_in_objc_category_named lcxt name
  | "is_in_objc_protocol_named", [name], _ ->
      CPredicates.is_in_objc_protocol_named lcxt name
  | "is_ivar_atomic", [], an ->
      CPredicates.is_ivar_atomic an
  | "is_method_property_accessor_of_ivar", [], an ->
      CPredicates.is_method_property_accessor_of_ivar an lcxt
  | "is_node", [nodename], an ->
      CPredicates.is_node an nodename
  | "is_objc_constructor", [], _ ->
      CPredicates.is_objc_constructor lcxt
  | "is_objc_dealloc", [], _ ->
      CPredicates.is_objc_dealloc lcxt
  | "is_objc_extension", [], _ ->
      CPredicates.is_objc_extension lcxt
  | "is_objc_interface_named", [name], an ->
      CPredicates.is_objc_interface_named an name
  | "is_objc_implementation_named", [name], an ->
      CPredicates.is_objc_implementation_named an name
  | "is_objc_class_named", [name], an ->
      CPredicates.is_objc_class_named an name
  | "is_objc_category_interface_on_class_named", [name], an ->
      CPredicates.is_objc_category_interface_on_class_named an name
  | "is_objc_category_implementation_on_class_named", [name], an ->
      CPredicates.is_objc_category_implementation_on_class_named an name
  | "is_objc_category_on_class_named", [cname], an ->
      CPredicates.is_objc_category_on_class_named an cname
  | "is_objc_category_interface_named", [name], an ->
      CPredicates.is_objc_category_interface_named an name
  | "is_objc_category_implementation_named", [name], an ->
      CPredicates.is_objc_category_implementation_named an name
  | "is_objc_category_named", [cname], an ->
      CPredicates.is_objc_category_named an cname
  | "is_objc_category_interface_on_subclass_of", [name], an ->
      CPredicates.is_objc_category_interface_on_subclass_of an name
  | "is_objc_category_implementation_on_subclass_of", [name], an ->
      CPredicates.is_objc_category_implementation_on_subclass_of an name
  | "is_objc_category_on_subclass_of", [name], an ->
      CPredicates.is_objc_category_on_subclass_of an name
  | "is_objc_protocol_named", [name], an ->
      CPredicates.is_objc_protocol_named an name
  | "is_objc_class_method_named", [name], an ->
      CPredicates.is_objc_class_method_named an name
  | "is_objc_instance_method_named", [name], an ->
      CPredicates.is_objc_instance_method_named an name
  | "is_objc_method_named", [name], an ->
      CPredicates.is_objc_method_named an name
  | "is_objc_method_overriding", [], an ->
      CPredicates.is_objc_method_overriding an
  | "is_objc_method_exposed", [], an ->
      CPredicates.is_objc_method_exposed lcxt an
  | "is_property_pointer_type", [], an ->
      CPredicates.is_property_pointer_type an
  | "is_strong_property", [], an ->
      CPredicates.is_strong_property an
  | "is_strong_ivar", [], an ->
      CPredicates.is_strong_ivar an
  | "is_unop_with_kind", [kind], an ->
      CPredicates.is_unop_with_kind an kind
  | "is_weak_property", [], an ->
      CPredicates.is_weak_property an
  | "is_receiver_objc_class_type", [], an ->
      CPredicates.is_receiver_objc_class_type an
  | "is_receiver_objc_id_type", [], an ->
      CPredicates.is_receiver_objc_id_type an
  | "is_receiver_subclass_of", [name], an ->
      CPredicates.is_receiver_subclass_of lcxt an name
  | "is_receiver_class_named", [name], an ->
      CPredicates.is_receiver_class_named lcxt an name
  | "is_receiver_super", [], an ->
      CPredicates.is_receiver_super an
  | "iphoneos_target_sdk_version_greater_or_equal", [version], _ ->
      CPredicates.iphoneos_target_sdk_version_greater_or_equal lcxt (ALVar.alexp_to_string version)
  | "method_return_type", [typ], an ->
      CPredicates.method_return_type an typ
  | "within_responds_to_selector_block", [], an ->
      CPredicates.within_responds_to_selector_block lcxt an
  | "using_namespace", [namespace], an ->
      CPredicates.using_namespace an namespace
  | "is_at_selector_with_name", [name], an ->
      CPredicates.is_at_selector_with_name an name
  | "has_type_const_ptr_to_objc_class", [], an ->
      CPredicates.has_type_const_ptr_to_objc_class an
  | "has_type_subprotocol_of", [protname], an ->
      CPredicates.has_type_subprotocol_of an protname
  | "has_visibility_attribute", [vis], an ->
      CPredicates.has_visibility_attribute an vis
  | "has_used_attribute", [], an ->
      CPredicates.has_used_attribute an
  | "within_available_class_block", [], an ->
      CPredicates.within_available_class_block lcxt an
  | "is_method_called_by_superclass", [], an ->
      CPredicates.is_method_called_by_superclass an
  | "is_cxx_copy_constructor", [], an ->
      CPredicates.is_cxx_copy_constructor an
  | "is_init_expr_cxx11_constant", [], an ->
      CPredicates.is_init_expr_cxx11_constant an
  | _ ->
      L.(die ExternalError) "Undefined Predicate or wrong set of arguments: '%s'" pred_name

and eval_AND an lcxt f1 f2 =
  match eval_formula f1 an lcxt with
  | Some witness1 -> (
    match eval_formula f2 an lcxt with
    | Some witness2 ->
        Some (choose_one_witness witness1 witness2)
    | _ ->
        None )
  | None (* we short-circuit the AND evaluation *) ->
      None

and eval_OR an lcxt f1 f2 = choose_witness_opt (eval_formula f1 an lcxt) (eval_formula f2 an lcxt)

and eval_Implies an lcxt f1 f2 =
  let witness1 = if Option.is_some (eval_formula f1 an lcxt) then None else Some an in
  let witness2 = eval_formula f2 an lcxt in
  choose_witness_opt witness1 witness2

(* an, lcxt |= EF phi  <=>
   an, lcxt |= phi or exists an' in Successors(st): an', lcxt |= EF phi

   That is: a (an, lcxt) satifies EF phi if and only if
   either (an,lcxt) satifies phi or there is a child an' of the node an
   such that (an', lcxt) satifies EF phi
*)
and eval_EF phi an lcxt trans =
  match (trans, an) with
  | Some _, _ ->
      (* Using equivalence EF[->trans] phi = phi OR EX[->trans](EF[->trans] phi)*)
      let phi' = Or (phi, EX (trans, EF (trans, phi))) in
      eval_formula phi' an lcxt
  | None, _ ->
      let witness_opt = eval_formula phi an lcxt in
      if Option.is_some witness_opt then witness_opt
      else
        List.fold_left (Ctl_parser_types.get_direct_successor_nodes an) ~init:witness_opt ~f:
          (fun acc node -> choose_witness_opt (eval_EF phi node lcxt trans) acc )

(* an, lcxt |= EX phi  <=> exists an' in Successors(st): an', lcxt |= phi

   That is: a (an, lcxt) satifies EX phi if and only if
   there exists is a child an' of the node an
   such that (an', lcxt) satifies phi
*)
and eval_EX phi an lcxt trans =
  let succs =
    match trans with
    | Some l ->
        next_state_via_transition an l
    | None ->
        Ctl_parser_types.get_direct_successor_nodes an
  in
  let witness_opt =
    List.fold_left succs ~init:None ~f:(fun acc node ->
        choose_witness_opt (eval_formula phi node lcxt) acc )
  in
  match (witness_opt, trans) with
  | Some _, Some trans when not (is_transition_to_successor trans) ->
      Some an (* We want to limit the witnesses to the successors of the original node. *)
  | _ ->
      witness_opt

(* an, lcxt |= E(phi1 U phi2) evaluated using the equivalence
   an, lcxt |= E(phi1 U phi2) <=> an, lcxt |= phi2 or (phi1 and EX(E(phi1 U phi2)))

   That is: a (an,lcxt) satifies E(phi1 U phi2) if and only if
   an,lcxt satifies the formula phi2 or (phi1 and EX(E(phi1 U phi2)))
*)
and eval_EU phi1 phi2 an lcxt trans =
  let f = Or (phi2, And (phi1, EX (trans, EU (trans, phi1, phi2)))) in
  eval_formula f an lcxt

(* an |= A(phi1 U phi2) evaluated using the equivalence
   an |= A(phi1 U phi2) <=> an |= phi2 or (phi1 and AX(A(phi1 U phi2)))

   Same as EU but for the all path quantifier A
*)
and eval_AU phi1 phi2 an lcxt trans =
  let f = Or (phi2, And (phi1, AX (trans, AU (trans, phi1, phi2)))) in
  eval_formula f an lcxt

(* an, lcxt |= InNode[node_type_list] phi <=>
   an is a node of type in node_type_list and an satifies phi
*)
and in_node node_type_list phi an lctx =
  let holds_for_one_node n =
    match lctx.CLintersContext.et_evaluation_node with
    | Some id ->
        if String.equal id (Ctl_parser_types.ast_node_unique_string_id an) then
          eval_formula phi an lctx
        else None
    | None ->
        if Ctl_parser_types.ast_node_has_kind [n] an then eval_formula phi an lctx else None
  in
  (* This is basically an OR of formula holds in the various nodes in the list *)
  List.fold_left node_type_list ~init:None ~f:(fun acc node ->
      choose_witness_opt (holds_for_one_node node) acc )

(* Intuitive meaning: (an,lcxt) satifies EH[Classes] phi
   if the node an is among the declaration specified by the list Classes and
   there exists a super class in its hierarchy whose declaration satisfy phi.

   an, lcxt |= EH[Classes] phi <=>
   the node an is in Classes and there exists a declaration d in Hierarchy(an)
   such that d,lcxt |= phi *)
and eval_EH classes phi an lcxt =
  (* Define EH[Classes] phi = ET[Classes](EF[->Super] phi) *)
  let f = ET (classes, None, EX (Some Super, EF (Some Super, phi))) in
  eval_formula f an lcxt

(* an, lcxt |= ET[T][->l]phi <=>
   eventually we reach a node an' such that an' is among the types defined in T
   and:

   an'-l->an''
   ("an' transitions" to another node an'' via an edge labelled l)
   and an'',lcxt |= phi

   or l is unspecified and an,lcxt |= phi
*)
and eval_ET tl trs phi an lcxt =
  let f =
    match trs with
    | Some _ ->
        EF (None, InNode (tl, EX (trs, phi)))
    | None ->
        EF (None, InNode (tl, phi))
  in
  eval_formula f an lcxt

(* Formulas are evaluated on a AST node an and a linter context lcxt *)
and eval_formula f an lcxt : Ctl_parser_types.ast_node option =
  debug_eval_begin (debug_create_payload an f lcxt) ;
  let res =
    match f with
    | True ->
        Some an
    | False ->
        None
    | Atomic (name, params) -> (
      try if eval_Atomic name params an lcxt then Some an else None
      with CFrontend_config.IncorrectAssumption e ->
        let trans_unit_ctx = lcxt.CLintersContext.translation_unit_context in
        ClangLogging.log_caught_exception trans_unit_ctx "IncorrectAssumption" e.position
          e.source_range e.ast_node ;
        None )
    | InNode (node_type_list, f1) ->
        in_node node_type_list f1 an lcxt
    | Not f1 -> (
      match eval_formula f1 an lcxt with Some _ -> None | None -> Some an )
    | And (f1, f2) ->
        eval_AND an lcxt f1 f2
    | Or (f1, f2) ->
        eval_OR an lcxt f1 f2
    | Implies (f1, f2) ->
        eval_Implies an lcxt f1 f2
    | AU (trans, f1, f2) ->
        eval_AU f1 f2 an lcxt trans
    | EU (trans, f1, f2) ->
        eval_EU f1 f2 an lcxt trans
    | EF (trans, f1) ->
        eval_EF f1 an lcxt trans
    | AF (trans, f1) ->
        eval_formula (AU (trans, True, f1)) an lcxt
    | AG (trans, f1) ->
        eval_formula (Not (EF (trans, Not f1))) an lcxt
    | EX (trans, f1) ->
        eval_EX f1 an lcxt trans
    | AX (trans, f1) ->
        eval_formula (Not (EX (trans, Not f1))) an lcxt
    | EH (cl, phi) ->
        eval_EH cl phi an lcxt
    | EG (trans, f1) ->
        (* st |= EG f1 <=> st |= f1 /\ EX EG f1 *)
        eval_formula (And (f1, EX (trans, EG (trans, f1)))) an lcxt
    | ET (tl, sw, phi) ->
        eval_ET tl sw phi an lcxt
  in
  debug_eval_end res ; res