infer_clone/infer/src/backend/dotty.ml

(*
 * Copyright (c) 2009 - 2013 Monoidics ltd.
 * Copyright (c) 2013 - present Facebook, Inc.
 * All rights reserved.
 *
 * This source code is licensed under the BSD style license found in the
 * LICENSE file in the root directory of this source tree. An additional grant
 * of patent rights can be found in the PATENTS file in the same directory.
 *)

module L = Logging
module F = Format

(** {1 Dotty} *)

(* When false it prints only the retain cycle part of a prop.
   When true it prints the full property (maybe useful for debug) *)
let print_full_prop = ref false

type kind_of_dotty_prop =
  | Generic_proposition
  | Spec_precondition
  | Spec_postcondition of Prop.normal Prop.t (** the precondition associated with the post *)
  | Lambda_pred of int * int * bool

(* the kind of links between different kinds of nodes*)
type kind_of_links =
  | LinkExpToExp
  | LinkExpToStruct
  | LinkStructToExp
  | LinkStructToStruct
  | LinkToArray
  | LinkArrayToExp
  | LinkArrayToStruct
  | LinkToSSL
  | LinkToDLL
  | LinkRetainCycle

(* coordinate identifies a node using two dimension: id is an numerical identifier of the node,*)
(* lambda identifies in which hpred parameter id lays in*)
type coordinate = {
  id: int;
  lambda: int;
}

(* define a link between two nodes. src_fld/trg_fld define the label of the src/trg field. It is*)
(* useful for having nodes from within a struct and/or to inside a struct *)
type link = {
  kind: kind_of_links;
  src: coordinate;
  src_fld: string;
  trg: coordinate;
  trg_fld: string;
}

(* type of the visualized boxes/nodes in the graph*)
type dotty_node =
  | Dotnil of coordinate (* nil box *)
  (* Dotdangling(coo,e,c): dangling box for expression e at coordinate coo and color c *)
  | Dotdangling of coordinate * Sil.exp * string
  (* Dotpointsto(coo,e,c): basic memory cell box for expression e at coordinate coo and color c *)
  | Dotpointsto of coordinate * Sil.exp * string
  (* Dotstruct(coo,e,l,c): struct box for expression e  with field list l at coordinate coo and color c *)
  | Dotstruct of coordinate * Sil.exp * (Ident.fieldname * Sil.strexp) list * string * Sil.exp
  (* Dotarray(coo,e1,e2,l,t,c): array box for expression e1  with field list l at coordinate coo and color c*)
  (* e2 is the size and t is the type *)
  | Dotarray of coordinate * Sil.exp * Sil.exp * (Sil.exp * Sil.strexp) list * Sil.typ * string
  (* Dotlseg(coo,e1,e2,k,h,c): list box from e1 to e2 at coordinate coo and color c*)
  | Dotlseg of coordinate * Sil.exp * Sil.exp * Sil.lseg_kind * Sil.hpred list * string
  (* Dotlseg(coo,e1,e2,e3,e4,k,h,c): doubly linked-list box from with parameters (e1,e2,e3,e4) at coordinate coo and color c*)
  | Dotdllseg of coordinate * Sil.exp * Sil.exp * Sil.exp * Sil.exp * Sil.lseg_kind * Sil.hpred list * string

let mk_coordinate i l = { id = i; lambda = l }

let mk_link k s sf t tf = { kind = k; src = s; src_fld = sf; trg = t; trg_fld = tf }

(* list of dangling boxes*)
let dangling_dotboxes = ref []

(* list of nil boxes*)
let nil_dotboxes = ref []

let exps_neq_zero = ref []

(* list of fields in the structs *)
let fields_structs = ref []
let struct_exp_nodes = ref []

(* general unique counter to assign a different number to boxex,           *)
(* clusters,subgraphs etc.                                                 *)
let dotty_state_count = ref 0

let spec_counter = ref 0
let post_counter = ref 0
let lambda_counter = ref 0
let proposition_counter = ref 0
let target_invisible_arrow_pre = ref 0
let current_pre = ref 0
let spec_id = ref 0
let invisible_arrows = ref false

let print_stack_info = ref false

let exp_is_neq_zero e =
  IList.exists (fun e' -> Sil.exp_equal e e') !exps_neq_zero

(* replace a dollar sign in a name with a D. We need this because dotty get confused if there is*)
(* a dollar sign i a label*)
let strip_special_chars s =
  let b = Bytes.of_string s in
  let replace st c c' =
    if Bytes.contains st c then begin
      let idx = Bytes.index st c in
      try
        Bytes.set st idx c';
        st
      with Invalid_argument _ -> L.out "@\n@\n Invalid argument!!! @\n @.@.@."; assert false
    end else st in
  let s0 = replace b '(' 'B' in
  let s1 = replace s0 '$' 'D' in
  let s2 = replace s1 '#' 'H' in
  let s3 = replace s2 '&' 'E' in
  let s4 = replace s3 '@' 'A' in
  let s5 = replace s4 ')' 'B' in
  let s6 = replace s5 '+' 'P' in
  let s7 = replace s6 '-' 'M' in
  Bytes.to_string s7

let rec strexp_to_string pe coo f se =
  match se with
  | Sil.Eexp (Sil.Lvar pvar, inst) -> F.fprintf f "%a" (Sil.pp_pvar pe) pvar
  | Sil.Eexp (Sil.Var id, inst) ->
      if !print_full_prop then
        F.fprintf f "%a" (Ident.pp pe) id
      else  ()
  | Sil.Eexp (e, inst) ->
      if !print_full_prop then
        F.fprintf f "%a" (Sil.pp_exp pe) e
      else F.fprintf f "_"
  | Sil.Estruct (ls, _) -> F.fprintf f " STRUCT | { %a } " (struct_to_dotty_str pe coo) ls
  | Sil.Earray(e, idx, _) -> F.fprintf f " ARRAY[%a] | { %a } " (Sil.pp_exp pe) e (get_contents pe coo) idx

and struct_to_dotty_str pe coo f ls : unit =
  match ls with
  | [] -> ()
  | (fn, se)::[]-> F.fprintf f "{ <%s%iL%i> %s: %a } " (Ident.fieldname_to_string fn) coo.id coo.lambda (Ident.fieldname_to_string fn) (strexp_to_string pe coo) se
  | (fn, se):: ls'-> F.fprintf f " { <%s%iL%i> %s: %a } | %a" (Ident.fieldname_to_string fn) coo.id coo.lambda (Ident.fieldname_to_string fn) (strexp_to_string pe coo) se (struct_to_dotty_str pe coo) ls'

and get_contents_sexp pe coo f se =
  match se with
  | Sil.Eexp (e', inst') ->
      F.fprintf f "%a" (Sil.pp_exp pe) e'
  | Sil.Estruct (se', _) ->
      F.fprintf f "| { %a }" (struct_to_dotty_str pe coo) se'
  | Sil.Earray(e', [], _) ->
      F.fprintf f "(ARRAY Size: %a) | { }" (Sil.pp_exp pe) e'
  | Sil.Earray(e', ((idx, a):: linner), _) ->
      F.fprintf f "(ARRAY Size: %a) | { %a: %a | %a }" (Sil.pp_exp pe) e' (Sil.pp_exp pe) idx
        (strexp_to_string pe coo) a (get_contents pe coo) linner

and get_contents_single pe coo f (e, se) =
  let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in
  F.fprintf f "{ <%s> %a : %a }"
    e_no_special_char (Sil.pp_exp pe) e (get_contents_sexp pe coo) se

and get_contents pe coo f = function
  | [] -> ()
  | [idx_se] ->
      F.fprintf f "%a" (get_contents_single pe coo) idx_se
  | idx_se:: l ->
      F.fprintf f "%a | %a" (get_contents_single pe coo) idx_se (get_contents pe coo) l

and get_contents_range_single pe coo f range_se =
  let (e1, e2), se = range_se in
  let e1_no_special_char = strip_special_chars (Sil.exp_to_string e1) in
  F.fprintf f "{ <%s> [%a,%a] : %a }"
    e1_no_special_char (Sil.pp_exp pe) e1 (Sil.pp_exp pe) e2 (get_contents_sexp pe coo) se

and get_contents_range pe coo f = function
  | [] -> ()
  | [range_se] ->
      F.fprintf f "%a" (get_contents_range_single pe coo) range_se
  | range_se:: l ->
      F.fprintf f "%a | %a" (get_contents_range_single pe coo) range_se (get_contents_range pe coo) l

(* true if node is the sorce node of the expression e*)
let is_source_node_of_exp e node =
  match node with
  | Dotpointsto (_, e', _) -> Sil.exp_compare e e' = 0
  | _ -> false

(* given a node returns its coordinates and the expression. Return -1 in case the expressio doesn.t*)
(* make sense for that case *)
let get_coordinate_and_exp dotnode =
  match dotnode with
  | Dotnil(coo) -> (coo, Sil.exp_minus_one)
  | Dotarray (coo, _, _, _, _, _) -> (coo, Sil.exp_minus_one)
  | Dotpointsto (coo, b, _)
  | Dotlseg (coo, b, _, _, _, _)
  | Dotdllseg (coo, b, _, _, _, _, _, _)
  | Dotstruct (coo, b, _, _, _)
  | Dotdangling(coo, b, _) -> (coo, b)

(* true if a node is of a Dotstruct *)
let is_not_struct node =
  match node with
  | Dotstruct _ -> false
  | _ -> true

(* returns the id field of the coordinate of node *)
let get_coordinate_id node =
  let coo = fst (get_coordinate_and_exp node) in
  coo.id

let rec look_up_for_back_pointer e dotnodes lambda =
  match dotnodes with
  | [] -> []
  | Dotdllseg(coo, _, _, _, e4, _, _, _):: dotnodes' ->
      if Sil.exp_compare e e4 = 0 && lambda = coo.lambda then [coo.id + 1]
      else look_up_for_back_pointer e dotnodes' lambda
  | _:: dotnodes' -> look_up_for_back_pointer e dotnodes' lambda

(* get the nodes corresponding to an expression and a lambda*)
let rec select_nodes_exp_lambda dotnodes e lambda =
  match dotnodes with
  | [] -> []
  | node:: l' ->
      let (coo, e') = get_coordinate_and_exp node in
      if (Sil.exp_compare e e' = 0) && lambda = coo.lambda then node:: select_nodes_exp_lambda l' e lambda
      else select_nodes_exp_lambda l' e lambda

(* look-up the coordinate id in the list of dotnodes those nodes which correspond to expression e*)
(* this is written in this strange way for legacy reason. It should be changed a bit*)
let look_up dotnodes e lambda =
  let r = select_nodes_exp_lambda dotnodes e lambda in
  let r'= IList.map get_coordinate_id r in
  r' @ look_up_for_back_pointer e dotnodes lambda

let pp_nesting fmt nesting =
  if nesting > 1 then F.fprintf fmt "%d" nesting

let reset_proposition_counter () = proposition_counter:= 0

let reset_dotty_spec_counter () = spec_counter:= 0

let max_map f l =
  let curr_max = ref 0 in
  IList.iter (fun x -> curr_max := max !curr_max (f x)) l;
  ! curr_max

let rec sigma_nesting_level sigma =
  max_map (function
      | Sil.Hpointsto _ -> 0
      | Sil.Hlseg (_, hpara, _, _, _) -> hpara_nesting_level hpara
      | Sil.Hdllseg (_, hpara_dll, _, _, _, _, _) -> hpara_dll_nesting_level hpara_dll) sigma

and hpara_nesting_level hpara =
  1 + sigma_nesting_level hpara.Sil.body

and hpara_dll_nesting_level hpara_dll =
  1 + sigma_nesting_level hpara_dll.Sil.body_dll

let color_to_str c =
  match c with
  | Black -> "black"
  | Blue -> "blue"
  | Green -> "green"
  | Orange -> "orange"
  | Red -> "red"

let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list) =
  let exp_color hpred (exp : Sil.exp) =
    if pe.pe_cmap_norm (Obj.repr hpred) == Red then Red
    else pe.pe_cmap_norm (Obj.repr exp) in
  let get_rhs_predicate (hpred, lambda) =
    let n = !dotty_state_count in
    incr dotty_state_count;
    let coo = mk_coordinate n lambda in
    (match hpred with
     | Sil.Hpointsto (_, Sil.Eexp (e, inst), _)
       when not (Sil.exp_equal e Sil.exp_zero)  && !print_full_prop ->
         let e_color_str = color_to_str (exp_color hpred e) in
         [Dotdangling(coo, e, e_color_str)]
     | Sil.Hlseg (k, hpara, _, e2, _) when not (Sil.exp_equal e2 Sil.exp_zero) ->
         let e2_color_str = color_to_str (exp_color hpred e2) in
         [Dotdangling(coo, e2, e2_color_str)]
     | Sil.Hdllseg (k, hpara_dll, e1, e2, e3, e4, elist) ->
         let e2_color_str = color_to_str (exp_color hpred e2) in
         let e3_color_str = color_to_str (exp_color hpred e3) in
         let ll = if not (Sil.exp_equal e2 Sil.exp_zero) then
             [Dotdangling(coo, e2, e2_color_str)]
           else [] in
         if not (Sil.exp_equal e3 Sil.exp_zero) then Dotdangling(coo, e3, e3_color_str):: ll
         else ll
     | Sil.Hpointsto (_, _, _)
     | _ -> [] (* arrays and struct do not give danglings*)
    ) in
  let is_allocated d =
    match d with
    | Dotdangling(_, e, _) ->
        IList.exists (fun a -> match a with
            | Dotpointsto(_, e', _)
            | Dotarray(_, _, e', _, _, _)
            | Dotlseg(_, e', _, _, _, _)
            | Dotdllseg(_, e', _, _, _, _, _, _) -> Sil.exp_equal e e'
            | _ -> false
          ) allocated_nodes
    | _ -> false (*this should never happen since d must be a dangling node *) in
  let rec filter_duplicate l seen_exp =
    match l with
    | [] -> []
    | Dotdangling(coo, e, color):: l' ->
        if (IList.exists (Sil.exp_equal e) seen_exp) then filter_duplicate l' seen_exp
        else Dotdangling(coo, e, color):: filter_duplicate l' (e:: seen_exp)
    | box:: l' -> box:: filter_duplicate l' seen_exp in (* this case cannot happen*)
  let rec subtract_allocated candidate_dangling =
    match candidate_dangling with
    | [] -> []
    | d:: candidates ->
        if (is_allocated d) then subtract_allocated candidates
        else d:: subtract_allocated candidates in
  let candidate_dangling = IList.flatten (IList.map get_rhs_predicate sigma_lambda) in
  let candidate_dangling = filter_duplicate candidate_dangling [] in
  let dangling = subtract_allocated candidate_dangling in
  dangling_dotboxes:= dangling

let rec dotty_mk_node pe sigma =
  let n = !dotty_state_count in
  incr dotty_state_count;
  let do_hpred_lambda exp_color = function
    | (Sil.Hpointsto (e, Sil.Earray(e', l, _), Sil.Sizeof(Sil.Tarray(t, s), _)), lambda) ->
        incr dotty_state_count;  (* increment once more n+1 is the box for the array *)
        let e_color_str = color_to_str (exp_color e) in
        let e_color_str'= color_to_str (exp_color e') in
        [Dotpointsto((mk_coordinate n lambda), e, e_color_str); Dotarray((mk_coordinate (n + 1) lambda), e, e', l, t, e_color_str')]
    | (Sil.Hpointsto (e, Sil.Estruct (l, _), te), lambda) ->
        incr dotty_state_count;  (* increment once more n+1 is the box for the struct *)
        let e_color_str = color_to_str (exp_color e) in
        (*      [Dotpointsto((mk_coordinate n lambda), e, l, true, e_color_str)] *)
        [Dotpointsto((mk_coordinate n lambda), e, e_color_str);
         Dotstruct((mk_coordinate (n + 1) lambda), e, l, e_color_str, te);]
    | (Sil.Hpointsto (e, _, _), lambda) ->
        let e_color_str = color_to_str (exp_color e) in
        if IList.mem Sil.exp_equal e !struct_exp_nodes then [] else
          [Dotpointsto((mk_coordinate n lambda), e, e_color_str)]
    | (Sil.Hlseg (k, hpara, e1, e2, elist), lambda) ->
        incr dotty_state_count; (* increment once more n+1 is the box for last element of the list *)
        let eq_color_str = color_to_str (exp_color e1) in
        [Dotlseg((mk_coordinate n lambda), e1, e2, k, hpara.Sil.body, eq_color_str)]
    | (Sil.Hdllseg (k, hpara_dll, e1, e2, e3, e4, elist), lambda) ->
        let e1_color_str = color_to_str (exp_color e1) in
        incr dotty_state_count;  (* increment once more n+1 is the box for e4 *)
        [Dotdllseg((mk_coordinate n lambda), e1, e2, e3, e4, k, hpara_dll.Sil.body_dll, e1_color_str)] in
  match sigma with
  | [] -> []
  | (hpred, lambda) :: sigma' ->
      let exp_color (exp : Sil.exp) =
        if pe.pe_cmap_norm (Obj.repr hpred) == Red then Red
        else pe.pe_cmap_norm (Obj.repr exp) in
      do_hpred_lambda exp_color (hpred, lambda) @ dotty_mk_node pe sigma'

let set_exps_neq_zero pi =
  let f = function
    | Sil.Aneq (e, Sil.Const (Sil.Cint i)) when Sil.Int.iszero i -> exps_neq_zero := e :: !exps_neq_zero
    | _ -> () in
  exps_neq_zero := [];
  IList.iter f pi

let box_dangling e =
  let entry_e = IList.filter (fun b -> match b with
      | Dotdangling(_, e', _) -> Sil.exp_equal e e' | _ -> false ) !dangling_dotboxes in
  match entry_e with
  |[] -> None
  | Dotdangling(coo, _, _):: _ -> Some coo.id
  | _ -> None (* NOTE: this cannot be possible since entry_e can be composed only by Dotdangling, see def of entry_e*)

let rec get_color_exp dot_nodes e =
  match dot_nodes with
  | [] ->""
  | Dotnil(_):: l' -> get_color_exp l' e
  | Dotpointsto(_, e', c):: l'
  | Dotdangling(_, e', c):: l'
  | Dotarray(_, _, e', _, _, c):: l'
  | Dotlseg(_, e', _, _, _, c):: l'
  | Dotstruct(_, e', _, c, _):: l'
  | Dotdllseg(_, e', _, _, _, _, _, c):: l' -> if (Sil.exp_equal e e') then c else get_color_exp l' e

(* construct a Dotnil and returns it's id *)
let make_nil_node lambda =
  let n = !dotty_state_count in
  incr dotty_state_count;
  nil_dotboxes:= Dotnil(mk_coordinate n lambda)::!nil_dotboxes;
  n

let compute_fields_struct sigma =
  fields_structs:=[];
  let rec do_strexp se in_struct =
    match se with
    | Sil.Eexp (e, inst) -> if in_struct then fields_structs:= e ::!fields_structs else ()
    | Sil.Estruct (l, _) -> IList.iter (fun e -> do_strexp e true) (snd (IList.split l))
    | Sil.Earray (_, l, _) -> IList.iter (fun e -> do_strexp e false) (snd (IList.split l)) in
  let rec fs s =
    match s with
    | [] -> ()
    | Sil.Hpointsto(_, se, _):: s' -> do_strexp se false; fs s'
    | _:: s' -> fs s' in
  fs sigma

let compute_struct_exp_nodes sigma =
  struct_exp_nodes:=[];
  let rec sen s =
    match s with
    | [] -> ()
    | Sil.Hpointsto(e, Sil.Estruct _, _):: s' -> struct_exp_nodes:= e::!struct_exp_nodes; sen s'
    | _:: s' -> sen s' in
  sen sigma

(* returns the expression of a node*)
let get_node_exp n = snd (get_coordinate_and_exp n)

let is_nil e prop =
  (Sil.exp_equal e Sil.exp_zero) || (Prover.check_equal prop e Sil.exp_zero)

(* an edge is in cycle *)
let in_cycle cycle edge =
  match cycle with
  | Some cycle' ->
      IList.mem (fun (fn, se) (_,fn',se') ->
          Ident.fieldname_equal fn fn' && Sil.strexp_equal se se') edge cycle'
  | _ -> false

let node_in_cycle cycle node =
  match cycle, node with
  | Some cycle', Dotstruct(coo, e1, l, c,te)  -> (* only struct nodes can be in cycle *)
      IList.exists (in_cycle cycle) l
  | _ -> false


(* compute a list of (kind of link, field name, coo.id target, name_target) *)
let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
  let find_target_one_fld (fn, se) =
    match se with
    | Sil.Eexp (e, inst) ->
        if is_nil e p then begin
          let n'= make_nil_node lambda in
          if !print_full_prop then
            [(LinkStructToExp, Ident.fieldname_to_string fn, n',"")]
          else []
        end else
          let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
          (match nodes_e with
           | [] ->
               (match box_dangling e with
                | None -> []
                | Some n' -> [(LinkStructToExp, Ident.fieldname_to_string fn, n',"")]
               )
           | [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] ->
               let n = get_coordinate_id node in
               if IList.mem Sil.exp_equal e !struct_exp_nodes then begin
                 let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in
                 let link_kind = if (in_cycle cycle (fn, se)) && (not !print_full_prop) then
                     LinkRetainCycle
                   else LinkStructToStruct in
                 [(link_kind, Ident.fieldname_to_string fn, n, e_no_special_char)]
               end else
                 [(LinkStructToExp, Ident.fieldname_to_string fn, n,"")]
           | _ -> (* by construction there must be at most 2 nodes for an expression*)
               L.out "@\n Too many nodes! Error! @\n@.@."; assert false)
    | Sil.Estruct (l, _) -> [] (* inner struct are printed by print_struc function *)
    | Sil.Earray _ -> [] in (* inner arrays are printed by print_array function *)
  match list_fld with
  | [] -> []
  | a:: list_fld' ->
      let targets_a = find_target_one_fld a in
      targets_a @ compute_target_struct_fields dotnodes list_fld' p f lambda cycle

(* compute a list of (kind of link, field name, coo.id target, name_target) *)
let rec compute_target_array_elements dotnodes list_elements p f lambda =
  let find_target_one_element (idx, se) =
    match se with
    | Sil.Eexp (e, inst) ->
        if is_nil e p then begin
          let n'= make_nil_node lambda in
          [(LinkArrayToExp, Sil.exp_to_string idx, n',"")]
        end else
          let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
          (match nodes_e with
           | [] ->
               (match box_dangling e with
                | None -> []
                | Some n' -> [(LinkArrayToExp, Sil.exp_to_string idx, n',"")]
               )
           | [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] ->
               let n = get_coordinate_id node in
               if IList.mem Sil.exp_equal e !struct_exp_nodes then begin
                 let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in
                 [(LinkArrayToStruct, Sil.exp_to_string idx, n, e_no_special_char)]
               end else
                 [(LinkArrayToExp, Sil.exp_to_string idx, n,"")]
           | _ -> (* by construction there must be at most 2 nodes for an expression*)
               L.out "@\n Too many nodes! Error! @\n@.@."; assert false
          )
    | Sil.Estruct (l, _) -> [] (* inner struct are printed by print_struc function *)
    | Sil.Earray _ ->[] (* inner arrays are printed by print_array function *)
  in
  match list_elements with
  | [] -> []
  | a:: list_ele' ->
      let targets_a = find_target_one_element a in
      targets_a @ compute_target_array_elements dotnodes list_ele' p f lambda

let compute_target_from_eexp dotnodes e p f lambda =
  if is_nil e p then
    let n'= make_nil_node lambda in
    [(LinkExpToExp, n', "")]
  else
    let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
    let nodes_e_no_struct = IList.filter is_not_struct nodes_e in
    let trg = IList.map get_coordinate_id nodes_e_no_struct in
    (match trg with
     | [] ->
         (match box_dangling e with
          | None -> []
          | Some n -> [(LinkExpToExp, n, "")]
         )
     | _ -> IList.map (fun n -> (LinkExpToExp, n, "")) trg
    )

(* build the set of edges between nodes *)
let rec dotty_mk_set_links dotnodes sigma p f cycle =
  let make_links_for_arrays e lie lambda sigma' = (* used for both Earray and ENarray*)
    let src = look_up dotnodes e lambda in
    match src with
    | [] -> assert false
    | n:: nl ->
        let target_list = compute_target_array_elements dotnodes lie p f lambda in
        (* below it's n+1 because n is the address, n+1 is the actual array node*)
        let ff n = IList.map (fun (k, lab_src, m, lab_trg) -> mk_link k (mk_coordinate (n + 1) lambda) (strip_special_chars lab_src) (mk_coordinate m lambda) (strip_special_chars lab_trg)) target_list in
        let links_from_elements = IList.flatten (IList.map ff (n:: nl)) in

        let trg_label = strip_special_chars (Sil.exp_to_string e) in
        let lnk = mk_link (LinkToArray) (mk_coordinate n lambda) "" (mk_coordinate (n + 1) lambda) trg_label in
        lnk :: links_from_elements @ dotty_mk_set_links dotnodes sigma' p f cycle in
  match sigma with
  | [] -> []
  | (Sil.Hpointsto (e, Sil.Earray(_, lie, _), _), lambda):: sigma' ->
      make_links_for_arrays e lie lambda sigma'
  | (Sil.Hpointsto (e, Sil.Estruct (lfld, _), t), lambda):: sigma' ->
      let src = look_up dotnodes e lambda in
      (match src with
       | [] -> assert false
       | nl ->
           (* L.out "@\n@\n List of nl= "; IList.iter (L.out " %i ") nl; L.out "@.@.@."; *)
           let target_list = compute_target_struct_fields dotnodes lfld p f lambda cycle in
           let ff n = IList.map (fun (k, lab_src, m, lab_trg) ->
               mk_link k (mk_coordinate n lambda) lab_src (mk_coordinate m lambda) lab_trg
             ) target_list in
           let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
           let address_struct_id =
             try get_coordinate_id (IList.hd (IList.filter (is_source_node_of_exp e) nodes_e))
             with exn when exn_not_failure exn -> assert false in
           (* we need to exclude the address node from the sorce of fields. no fields should start from there*)
           let nl'= IList.filter (fun id -> address_struct_id != id) nl in
           let links_from_fields = IList.flatten (IList.map ff nl') in
           let lnk_from_address_struct = if !print_full_prop then
               let trg_label = strip_special_chars (Sil.exp_to_string e) in
               [mk_link (LinkExpToStruct) (mk_coordinate address_struct_id lambda) ""
                  (mk_coordinate (address_struct_id + 1) lambda) trg_label]
             else [] in
           lnk_from_address_struct @ links_from_fields @
           dotty_mk_set_links dotnodes sigma' p f cycle)
  | (Sil.Hpointsto (e, Sil.Eexp (e', inst'), t), lambda):: sigma' ->
      let src = look_up dotnodes e lambda in
      (match src with
       | [] -> assert false
       | nl -> if !print_full_prop then
             let target_list = compute_target_from_eexp dotnodes e' p f lambda in
             let ff n = IList.map (fun (k, m, lab_target) ->
                 mk_link k (mk_coordinate n lambda) ""
                   (mk_coordinate m lambda) (strip_special_chars lab_target)
               ) target_list in
             let ll = IList.flatten (IList.map ff nl) in
             ll @ dotty_mk_set_links dotnodes sigma' p f cycle
           else dotty_mk_set_links dotnodes sigma' p f cycle)

  | (Sil.Hlseg (_, pred, e1, e2, elist), lambda):: sigma' ->
      let src = look_up dotnodes e1 lambda in
      (match src with
       | [] -> assert false
       | n:: _ ->
           let (_, m, lab) = IList.hd (compute_target_from_eexp dotnodes e2 p f lambda) in
           let lnk = mk_link LinkToSSL (mk_coordinate (n + 1) lambda) "" (mk_coordinate m lambda) lab in
           lnk:: dotty_mk_set_links dotnodes sigma' p f cycle
      )
  | (Sil.Hdllseg (_, pred, e1, e2, e3, e4, elist), lambda):: sigma' ->
      let src = look_up dotnodes e1 lambda in
      (match src with
       | [] -> assert false
       | n:: _ -> (* n is e1's box  and n+1 is e4's box *)
           let targetF = look_up dotnodes e3 lambda in
           let target_Flink = (match targetF with
               | [] -> []
               | m:: _ -> [mk_link LinkToDLL (mk_coordinate (n + 1) lambda) "" (mk_coordinate m lambda) ""]
             ) in
           let targetB = look_up dotnodes e2 lambda in
           let target_Blink = (match targetB with
               | [] -> []
               | m:: _ -> [mk_link LinkToDLL (mk_coordinate n lambda) "" (mk_coordinate m lambda) ""]
             ) in
           target_Blink @ target_Flink @ dotty_mk_set_links dotnodes sigma' p f cycle
      )

let print_kind f kind =
  incr dotty_state_count;
  match kind with
  | Spec_precondition ->
      incr dotty_state_count;
      current_pre:=!dotty_state_count;
      F.fprintf f "\n PRE%iL0 [label=\"PRE %i \",  style=filled, color= yellow]\n" !dotty_state_count !spec_counter;
      print_stack_info:= true;
  | Spec_postcondition pre ->
      F.fprintf f "\n POST%iL0 [label=\"POST %i \",  style=filled, color= yellow]\n" !dotty_state_count !post_counter;
      print_stack_info:= true;
  | Generic_proposition ->
      if !print_full_prop then
      F.fprintf f "\n HEAP%iL0 [label=\"HEAP %i \",  style=filled, color= yellow]\n" !dotty_state_count !proposition_counter
  | Lambda_pred (no, lev, array) ->
      match array with
      | false ->
          F.fprintf f "style=dashed; color=blue \n state%iL%i [label=\"INTERNAL STRUCTURE %i \",  style=filled, color= lightblue]\n" !dotty_state_count !lambda_counter !lambda_counter ;
          F.fprintf f "state%iL%i -> state%iL%i [color=\"lightblue \"  arrowhead=none] \n" !dotty_state_count !lambda_counter no lev;
      | true ->
          F.fprintf f "style=dashed; color=blue \n state%iL%i [label=\"INTERNAL STRUCTURE %i \",  style=filled, color= lightblue]\n" !dotty_state_count !lambda_counter !lambda_counter ;
          (* F.fprintf f "state%iL%i -> struct%iL%i:%s [color=\"lightblue \"  arrowhead=none] \n" !dotty_state_count !lambda_counter no lev lab;*)

          incr dotty_state_count

(* print a link between two noeds in the graph *)
let dotty_pp_link f link =
  let n1 = link.src.id in
  let lambda1 = link.src.lambda in
  let n2 = link.trg.id in
  let lambda2 = link.trg.lambda in
  let src_fld = link.src_fld in
  let trg_fld = link.trg_fld in
  match n2, link.kind with
  | 0, _  when !print_full_prop ->
      F.fprintf f "state%iL%i -> state%iL%i[label=\"%s DANG\", color= red];\n" n1 lambda1 n2 lambda2 src_fld
  | _, LinkToArray when !print_full_prop ->
      F.fprintf f "state%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]\n" n1 lambda1 n2 lambda2 trg_fld n2 lambda2
  | _, LinkExpToStruct when !print_full_prop ->
      F.fprintf f "state%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]\n" n1 lambda1 n2 lambda2 trg_fld n2 lambda2
  | _, LinkStructToExp when !print_full_prop ->
      F.fprintf f "struct%iL%i:%s%iL%i -> state%iL%i[label=\"\"]\n"
        n1 lambda1 src_fld n1 lambda1 n2 lambda2
  | _, LinkRetainCycle ->
      F.fprintf f "struct%iL%i:%s%iL%i -> struct%iL%i:%s%iL%i[label=\"\", color= red]\n"
        n1 lambda1 src_fld n1 lambda1 n2 lambda2 trg_fld n2 lambda2
  | _, LinkStructToStruct when !print_full_prop ->
      F.fprintf f "struct%iL%i:%s%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]\n" n1 lambda1 src_fld n1 lambda1 n2 lambda2 trg_fld n2 lambda2
  | _, LinkArrayToExp when !print_full_prop ->
      F.fprintf f "struct%iL%i:%s -> state%iL%i[label=\"\"]\n" n1 lambda1 src_fld n2 lambda2
  | _, LinkArrayToStruct when !print_full_prop ->
      F.fprintf f "struct%iL%i:%s -> struct%iL%i[label=\"\"]\n" n1 lambda1 src_fld n2 lambda2
  | _, _  -> if !print_full_prop then
        F.fprintf f "state%iL%i -> state%iL%i[label=\"%s\"];\n" n1 lambda1 n2 lambda2 src_fld
      else ()

(* given the list of nodes and links get rid of spec nodes that are not pointed to by anybody*)
let filter_useless_spec_dollar_box (nodes: dotty_node list) (links: link list) =
  let tmp_nodes = ref nodes in
  let tmp_links = ref links in
  let remove_links_from ln = IList.filter (fun n' -> not (IList.mem Pervasives.(=) n' ln)) !tmp_links in
  let remove_node n ns =
    IList.filter (fun n' -> match n' with
        | Dotpointsto _ -> (get_coordinate_id n')!= (get_coordinate_id n)
        | _ -> true
      ) ns in
  let rec boxes_pointed_by n lns =
    match lns with
    | [] -> []
    | l:: ln' -> let n_id = get_coordinate_id n in
        if l.src.id = n_id && l.src_fld ="" then (
          (*L.out "@\n Found link (%i,%i)" l.src.id l.trg.id;*)
          l:: boxes_pointed_by n ln'
        )
        else boxes_pointed_by n ln' in
  let rec boxes_pointing_at n lns =
    match lns with
    | [] -> []
    | l:: ln' -> let n_id = get_coordinate_id n in
        if l.trg.id = n_id && l.trg_fld ="" then (
          (*L.out "@\n Found link (%i,%i)" l.src.id l.trg.id;*)
          l:: boxes_pointing_at n ln' )
        else boxes_pointing_at n ln' in
  let is_spec_variable = function
    | Sil.Var id ->
        Ident.is_normal id && Ident.name_equal (Ident.get_name id) Ident.name_spec
    | _ -> false in
  let handle_one_node node =
    match node with
    | Dotpointsto _ ->
        let e = get_node_exp node in
        if is_spec_variable e then begin
          (*L.out "@\n Found a spec expression = %s @.@." (Sil.exp_to_string e); *)
          let links_from_node = boxes_pointed_by node links in
          let links_to_node = boxes_pointing_at node links in
          (* L.out "@\n Size of links_from=%i links_to=%i @.@." (IList.length links_from_node) (IList.length links_to_node); *)
          if links_to_node =[] then begin
            tmp_links:= remove_links_from links_from_node ;
            tmp_nodes:= remove_node node !tmp_nodes;
          end
        end
    | _ -> () in
  IList.iter handle_one_node nodes;
  (!tmp_nodes,!tmp_links)

(* print a struct node *)
let rec print_struct f pe e te l coo c =
  let print_type = match te with
    | Sil.Sizeof (t, _) ->
        let str_t = Sil.typ_to_string t in
        (match Str.split_delim (Str.regexp_string Config.anonymous_block_prefix) str_t with
         | [_; _] -> "BLOCK object"
         | _ -> str_t)
    | _ -> Sil.exp_to_string te in
  let n = coo.id in
  let lambda = coo.lambda in
  let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in
  F.fprintf f "subgraph structs_%iL%i {\n" n lambda ;
  if !print_full_prop then
    F.fprintf f
      " node [shape=record]; \n struct%iL%i \
        [label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s\n"
      n lambda e_no_special_char n lambda (Sil.pp_exp pe) e (struct_to_dotty_str pe coo) l c
  else
    F.fprintf f
      " node [shape=record]; \n struct%iL%i \
        [label=\"{<%s%iL%i> OBJECT: %s } | %a\" ] fontcolor=%s\n"
      n lambda e_no_special_char n lambda print_type (struct_to_dotty_str pe coo) l c;
  F.fprintf f "}\n"

and print_array f pe e1 e2 l ty coo c =
  let n = coo.id in
  let lambda = coo.lambda in
  let e_no_special_char = strip_special_chars (Sil.exp_to_string e1) in
  F.fprintf f "subgraph structs_%iL%i {\n" n lambda ;
  F.fprintf f " node [shape=record]; \n struct%iL%i [label=\"{<%s%iL%i> ARRAY| SIZE: %a } | %a\" ] fontcolor=%s\n" n lambda e_no_special_char n lambda (Sil.pp_exp pe) e2 (get_contents pe coo) l c;
  F.fprintf f "}\n"

and print_sll f pe nesting k e1 e2 coo =
  let n = coo.id in
  let lambda = coo.lambda in
  let n' = !dotty_state_count in
  incr dotty_state_count;
  begin
    match k with
    | Sil.Lseg_NE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white];  label=\"list NE\";" n' lambda  (*pp_nesting nesting*)
    | Sil.Lseg_PE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white];  label=\"list PE\";" n' lambda (*pp_nesting nesting *)
  end;
  F.fprintf f "state%iL%i [label=\"%a\"]\n" n lambda (Sil.pp_exp pe) e1;
  let n' = !dotty_state_count in
  incr dotty_state_count;
  F.fprintf f "state%iL%i [label=\"... \" style=filled color=lightgrey] \n" n' lambda ;
  F.fprintf f "state%iL%i -> state%iL%i [label=\" \"] \n" n lambda n' lambda ;
  F.fprintf f "state%iL%i [label=\" \"] \n" (n + 1) lambda ;
  F.fprintf f "state%iL%i -> state%iL%i [label=\" \"] }" n' lambda (n + 1) lambda ;
  incr lambda_counter;
  pp_dotty f (Lambda_pred(n + 1, lambda, false)) (Prop.normalize (Prop.from_sigma nesting)) None

and print_dll f pe nesting k e1 e2 e3 e4 coo =
  let n = coo.id in
  let lambda = coo.lambda in
  let n' = !dotty_state_count in
  incr dotty_state_count;
  begin
    match k with
    | Sil.Lseg_NE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white];  label=\"doubly-linked list NE\";" n' lambda  (*pp_nesting nesting *)
    | Sil.Lseg_PE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white];  label=\"doubly-linked list PE\";" n' lambda (*pp_nesting nesting *)
  end;
  F.fprintf f "state%iL%i [label=\"%a\"]\n" n lambda (Sil.pp_exp pe) e1;
  let n' = !dotty_state_count in
  incr dotty_state_count;
  F.fprintf f "state%iL%i [label=\"... \" style=filled color=lightgrey] \n" n' lambda;
  F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]\n" n lambda n' lambda;
  F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]\n" n' lambda n lambda;
  F.fprintf f "state%iL%i [label=\"%a\"]\n" (n + 1) lambda (Sil.pp_exp pe) e4;
  F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]\n" (n + 1) lambda n' lambda;
  F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]}\n" n' lambda (n + 1) lambda ;
  incr lambda_counter;
  pp_dotty f (Lambda_pred(n', lambda, false)) (Prop.normalize (Prop.from_sigma nesting)) None

and dotty_pp_state f pe cycle dotnode =
  let dotty_exp coo e c is_dangling =
    let n = coo.id in
    let lambda = coo.lambda in
    if is_dangling then
      F.fprintf f "state%iL%i [label=\"%a \", color=red, style=dashed, fontcolor=%s]\n" n lambda (Sil.pp_exp pe) e c
    else
      F.fprintf f "state%iL%i [label=\"%a\" fontcolor=%s]\n" n lambda (Sil.pp_exp pe) e c in
  match dotnode with
  | Dotnil coo when !print_full_prop ->
      F.fprintf f "state%iL%i [label=\"NIL \", color=green, style=filled]\n" coo.id coo.lambda
  | Dotdangling(coo, e, c) when !print_full_prop -> dotty_exp coo e c true
  | Dotpointsto(coo, e1, c) when !print_full_prop -> dotty_exp coo e1 c false
  | Dotstruct(coo, e1, l, c,te) ->
      let l' = if !print_full_prop then l
        else IList.filter (fun edge -> in_cycle cycle edge) l in
      print_struct f pe e1 te l' coo c
  | Dotarray(coo, e1, e2, l, ty, c) when !print_full_prop -> print_array f pe e1 e2 l ty coo c
  | Dotlseg(coo, e1, e2, Sil.Lseg_NE, nesting, c) when !print_full_prop ->
      print_sll f pe nesting Sil.Lseg_NE e1 e2 coo
  | Dotlseg(coo, e1, e2, Sil.Lseg_PE, nesting, c) when !print_full_prop ->
      print_sll f pe nesting Sil.Lseg_PE e1 e2 coo
  | Dotdllseg(coo, e1, e2, e3, e4, Sil.Lseg_NE, nesting, c) when !print_full_prop ->
      print_dll f pe nesting Sil.Lseg_NE e1 e2 e3 e4 coo
  | Dotdllseg(coo, e1, e2, e3, e4, Sil.Lseg_PE, nesting, c) when !print_full_prop ->
      print_dll f pe nesting Sil.Lseg_PE e1 e2 e3 e4 coo
  | _ -> ()

(* Build the graph data structure to be printed *)
and build_visual_graph f pe p cycle =
  let sigma = Prop.get_sigma p in
  compute_fields_struct sigma;
  compute_struct_exp_nodes sigma;
  (* L.out "@\n@\n Computed fields structs: ";
     IList.iter (fun e -> L.out " %a " (Sil.pp_exp pe) e) !fields_structs;
     L.out "@\n@.";
     L.out "@\n@\n Computed exp structs nodes: ";
     IList.iter (fun e -> L.out " %a " (Sil.pp_exp pe) e) !struct_exp_nodes;
     L.out "@\n@."; *)
  let sigma_lambda = IList.map (fun hp -> (hp,!lambda_counter)) sigma in
  let nodes = (dotty_mk_node pe) sigma_lambda in
  if !print_full_prop then make_dangling_boxes pe nodes sigma_lambda;
  let links = dotty_mk_set_links nodes sigma_lambda p f cycle in
  filter_useless_spec_dollar_box nodes links

and display_pure_info f pe prop =
  let print_invisible_objects () =
    for j = 1 to 4 do
      F.fprintf f "  inv_%i%i [style=invis]\n" !spec_counter j;
      F.fprintf f "  inv_%i%i%i [style=invis]\n" !spec_counter j j;
      F.fprintf f "  inv_%i%i%i%i [style=invis]\n" !spec_counter j j j;
    done;
    for j = 1 to 4 do
      F.fprintf f "  state_pi_%i -> inv_%i%i [style=invis]\n" !proposition_counter !spec_counter j;
      F.fprintf f "  inv_%i%i -> inv_%i%i%i [style=invis]\n" !spec_counter j !spec_counter j j;
      F.fprintf f "  inv_%i%i%i -> inv_%i%i%i%i [style=invis]\n" !spec_counter j j !spec_counter j j j;
    done in
  let pure = Prop.get_pure prop in
  F.fprintf f "subgraph {\n";
  F.fprintf f " node [shape=box]; \n state_pi_%i [label=\"STACK \\n\\n %a\" color=orange style=filled]\n" !proposition_counter (Prop.pp_pi pe) pure;
  if !invisible_arrows then print_invisible_objects ();
  F.fprintf f "}\n"

(** Pretty print a proposition in dotty format. *)
and pp_dotty f kind (_prop: Prop.normal Prop.t) cycle =
  incr proposition_counter;
  let pe, prop = match kind with
    | Spec_postcondition pre ->
        target_invisible_arrow_pre:=!proposition_counter;
        let diff = Propgraph.compute_diff Black (Propgraph.from_prop pre) (Propgraph.from_prop _prop) in
        let cmap_norm = Propgraph.diff_get_colormap false diff in
        let cmap_foot = Propgraph.diff_get_colormap true diff in
        let pe = { (Prop.prop_update_obj_sub pe_text pre) with pe_cmap_norm = cmap_norm; pe_cmap_foot = cmap_foot } in
        let pre_stack = fst (Prop.sigma_get_stack_nonstack true (Prop.get_sigma pre)) in (* add stack vars from pre *)
        let prop = Prop.replace_sigma (pre_stack @ Prop.get_sigma _prop) _prop in
        pe, Prop.normalize prop
    | _ ->
        let pe = Prop.prop_update_obj_sub pe_text _prop in
        pe, _prop in
  dangling_dotboxes := [];
  nil_dotboxes :=[];
  set_exps_neq_zero (Prop.get_pi prop);
  incr dotty_state_count;
  F.fprintf f "\n subgraph cluster_prop_%i { color=black \n" !proposition_counter;
  print_kind f kind;
  if !print_stack_info then begin
    display_pure_info f pe prop;
    print_stack_info:= false
  end;
  (* F.fprintf f "\n subgraph cluster_%i { color=black \n" !dotty_state_count; *)
  let (nodes, links) = build_visual_graph f pe prop cycle in
  let all_nodes = (nodes @ !dangling_dotboxes @ !nil_dotboxes) in
  if !print_full_prop then
    IList.iter ((dotty_pp_state f pe) cycle) all_nodes
  else
    IList.iter (fun node ->
        if node_in_cycle cycle node then (dotty_pp_state f pe) cycle node) all_nodes;
  IList.iter (dotty_pp_link f) links;
  (* F.fprintf f "\n } \n"; *)
  F.fprintf f "\n } \n"

let pp_dotty_one_spec f pre posts =
  post_counter := 0;
  incr spec_counter;
  incr proposition_counter;
  incr dotty_state_count;
  F.fprintf f "\n subgraph cluster_%i { color=blue \n" !dotty_state_count;
  incr dotty_state_count;
  F.fprintf f "\n state%iL0 [label=\"SPEC %i \",  style=filled, color= lightblue]\n" !dotty_state_count !spec_counter;
  spec_id:=!dotty_state_count;
  invisible_arrows:= true;
  pp_dotty f (Spec_precondition) pre None;
  invisible_arrows:= false;
  IList.iter (fun (po, path) -> incr post_counter ; pp_dotty f (Spec_postcondition pre) po None;
              for j = 1 to 4 do
                F.fprintf f "  inv_%i%i%i%i -> state_pi_%i [style=invis]\n" !spec_counter j j j !target_invisible_arrow_pre;
              done
            ) posts;
  F.fprintf f "\n } \n"

(* this is used to print a list of proposition when considered in a path of nodes *)
let pp_dotty_prop_list_in_path f plist prev_n curr_n =
  try
    incr proposition_counter;
    incr dotty_state_count;
    F.fprintf f "\n subgraph cluster_%i { color=blue \n" !dotty_state_count;
    incr dotty_state_count;
    F.fprintf f "\n state%iN [label=\"NODE %i \",  style=filled, color= lightblue]\n" curr_n curr_n;
    IList.iter (fun po -> incr proposition_counter ;
                 pp_dotty f (Generic_proposition) po None) plist;
    if prev_n <> - 1 then F.fprintf f "\n state%iN ->state%iN\n" prev_n curr_n;
    F.fprintf f "\n } \n"
  with exn when exn_not_failure exn ->
    ()

let pp_dotty_prop fmt (prop, cycle) =
  reset_proposition_counter ();
  Format.fprintf fmt "@\n@\n@\ndigraph main { \nnode [shape=box]; @\n";
  Format.fprintf fmt "@\n compound = true; rankdir =LR; @\n";
  pp_dotty fmt Generic_proposition prop (Some cycle);
  Format.fprintf fmt "@\n}"

let dotty_prop_to_str prop cycle =
  try
    Some (pp_to_string pp_dotty_prop (prop, cycle))
  with exn when exn_not_failure exn -> None

(* create a dotty file with a single proposition *)
let dotty_prop_to_dotty_file fname prop cycle =
  try
    let out_dot = open_out fname in
    let fmt_dot = Format.formatter_of_out_channel out_dot in
    pp_dotty_prop fmt_dot (prop, cycle);
    close_out out_dot
  with exn when exn_not_failure exn ->
    ()

(* this is used only to print a list of prop parsed with the external parser. Basically deprecated.*)
let pp_proplist_parsed2dotty_file filename plist =
  try
    let pp_list f plist =
      reset_proposition_counter ();
      F.fprintf f "\n\n\ndigraph main { \nnode [shape=box];\n";
      F.fprintf f "\n compound = true; \n";
      F.fprintf f "\n /* size=\"12,7\"; ratio=fill;*/ \n";
      ignore (IList.map (pp_dotty f Generic_proposition) plist);
      F.fprintf f "\n}" in
    let outc = open_out filename in
    let fmt = F.formatter_of_out_channel outc in
    F.fprintf fmt "#### Dotty version:  ####@.%a@.@." pp_list plist;
    close_out outc
  with exn when exn_not_failure exn ->
    ()

(********** START of Print interprocedural cfgs in dotty format  *)
(********** Print control flow graph (in dot form) for fundec to *)
(* channel. You have to compute an interprocedural cfg first               *)

let pp_cfgnodename fmt (n : Cfg.Node.t) =
  F.fprintf fmt "%d" (Cfg.Node.get_id n)

let pp_etlist fmt etl =
  IList.iter (fun (id, ty) ->
      Format.fprintf fmt " %a:%a" Mangled.pp id (Sil.pp_typ_full pe_text) ty) etl

let pp_local_list fmt etl =
  IList.iter (fun (id, ty) ->
      Format.fprintf fmt " %a:%a" Mangled.pp id (Sil.pp_typ_full pe_text) ty) etl

let pp_cfgnodelabel fmt (n : Cfg.Node.t) =
  let pp_label fmt n =
    match Cfg.Node.get_kind n with
    | Cfg.Node.Start_node (pdesc) ->
        (* let def = if Cfg.Procdesc.is_defined pdesc then "defined" else "declared" in *)
        (* Format.fprintf fmt "Start %a (%s)" pp_id (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc)) def *)
        Format.fprintf fmt "Start %s\\nFormals: %a\\nLocals: %a"
          (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc))
          pp_etlist (Cfg.Procdesc.get_formals pdesc)
          pp_local_list (Cfg.Procdesc.get_locals pdesc);
        if IList.length (Cfg.Procdesc.get_captured pdesc) <> 0 then
          Format.fprintf fmt "\\nCaptured: %a"
            pp_local_list (Cfg.Procdesc.get_captured pdesc)
    | Cfg.Node.Exit_node (pdesc) ->
        Format.fprintf fmt "Exit %s" (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc))
    | Cfg.Node.Join_node ->
        Format.fprintf fmt "+"
    | Cfg.Node.Prune_node (is_true_branch, ik, s) -> Format.fprintf fmt "Prune (%b branch)" is_true_branch
    | Cfg.Node.Stmt_node s -> Format.fprintf fmt " %s" s
    | Cfg.Node.Skip_node s -> Format.fprintf fmt "Skip %s" s in
  let instr_string i =
    let pp f () = Sil.pp_instr pe_text f i in
    let str = pp_to_string pp () in
    Escape.escape_dotty str in
  let pp_instrs fmt instrs =
    IList.iter (fun i -> F.fprintf fmt " %s\\n " (instr_string i)) instrs in
  let instrs = Cfg.Node.get_instrs n in
  F.fprintf fmt "%d: %a \\n  %a" (Cfg.Node.get_id n) pp_label n pp_instrs instrs

let pp_cfgnodeshape fmt (n: Cfg.Node.t) =
  match Cfg.Node.get_kind n with
  | Cfg.Node.Start_node _ | Cfg.Node.Exit_node _ -> F.fprintf fmt "color=yellow style=filled"
  | Cfg.Node.Prune_node _ -> F.fprintf fmt "shape=\"invhouse\""
  | Cfg.Node.Skip_node _ -> F.fprintf fmt "color=\"gray\""
  | Cfg.Node.Stmt_node _ -> F.fprintf fmt "shape=\"box\""
  | _ -> F.fprintf fmt ""

(*
let pp_cfgedge fmt src dest =
F.fprintf fmt "%a -> %a"
pp_cfgnodename src
pp_cfgnodename dest
*)

let pp_cfgnode fmt (n: Cfg.Node.t) =
  F.fprintf fmt "%a [label=\"%a\" %a]\n\t\n" pp_cfgnodename n pp_cfgnodelabel n pp_cfgnodeshape n;
  let print_edge n1 n2 is_exn =
    let color = if is_exn then "[color=\"red\" ]" else "" in
    match Cfg.Node.get_kind n2 with
    | Cfg.Node.Exit_node _ when is_exn = true -> (* don't print exception edges to the exit node *)
        ()
    | _ ->
        F.fprintf fmt "\n\t %d -> %d %s;" (Cfg.Node.get_id n1) (Cfg.Node.get_id n2) color in
  IList.iter (fun n' -> print_edge n n' false) (Cfg.Node.get_succs n);
  IList.iter (fun n' -> print_edge n n' true) (Cfg.Node.get_exn n)

(* * print control flow graph (in dot form) for fundec to channel let      *)
(* print_cfg_channel (chan : out_channel) (fd : fundec) = let pnode (s:    *)
(* stmt) = fprintf chan "%a@\n" d_cfgnode s in forallStmts pnode fd *      *)
(* Print control flow graph (in dot form) for fundec to file let           *)
(* print_cfg_filename (filename : string) (fd : fundec) = let chan =       *)
(* open_out filename in begin print_cfg_channel chan fd; close_out chan;   *)
(* end                                                                     *)

(* Print the extra information related to the inteprocedural aspect, ie.,  *)
(* special node, and call / return edges                                   *)
let print_icfg fmt cfg =
  let print_node node =
    let loc = Cfg.Node.get_loc node in
    if (!Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file !DB.current_source) then
      F.fprintf fmt "%a\n" pp_cfgnode node in
  IList.iter print_node (Cfg.Node.get_all_nodes cfg)

let print_edges fmt edges =
  let count = ref 0 in
  let print_edge (n1, n2) =
    incr count;
    F.fprintf fmt "%a -> %a [color=\"red\" label=\"%d\" fontcolor=\"green\"];" pp_cfgnodename n1 pp_cfgnodename n2 !count in
  IList.iter print_edge edges

let print_icfg_dotty cfg (extra_edges : (Cfg.Node.t * Cfg.Node.t) list) =
  let chan = open_out (DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [!Config.dotty_output])) in
  let fmt = Format.formatter_of_out_channel chan in
  F.fprintf fmt "digraph iCFG {\n";
  print_icfg fmt cfg;
  print_edges fmt extra_edges;
  F.fprintf fmt "}\n";
  close_out chan

let store_icfg_to_file filename cfg =
  let chan = open_out ((Filename.chop_extension filename)^".dot") in
  let fmt = Format.formatter_of_out_channel chan in
  F.fprintf fmt "digraph iCFG {\n";
  print_icfg fmt cfg;
  F.fprintf fmt "}\n";
  close_out chan

(********** END of Printing dotty files ***********)

(** Dotty printing for specs *)
let pp_speclist_dotty f (splist: Prop.normal Specs.spec list) =
  let pp_simple_saved = !Config.pp_simple in
  Config.pp_simple := true;
  reset_proposition_counter ();
  reset_dotty_spec_counter ();
  F.fprintf f "@\n@\n\ndigraph main { \nnode [shape=box]; @\n";
  F.fprintf f "@\n compound = true; @\n";
  (*  F.fprintf f "\n size=\"12,7\"; ratio=fill; \n"; *)
  IList.iter (fun s -> pp_dotty_one_spec f (Specs.Jprop.to_prop s.Specs.pre) s.Specs.posts) splist;
  F.fprintf f "@\n}";
  Config.pp_simple := pp_simple_saved

let pp_speclist_to_file (filename : DB.filename) spec_list =
  let pp_simple_saved = !Config.pp_simple in
  Config.pp_simple := true;
  let outc = open_out (DB.filename_to_string (DB.filename_add_suffix filename ".dot")) in
  let fmt = F.formatter_of_out_channel outc in
  let () = F.fprintf fmt "#### Dotty version:  ####@\n%a@\n@\n" pp_speclist_dotty spec_list in
  close_out outc;
  Config.pp_simple := pp_simple_saved

let pp_speclist_dotty_file (filename : DB.filename) spec_list =
  try pp_speclist_to_file filename spec_list
  with exn when exn_not_failure exn ->
    ()

(**********************************************************************)
(* Code prodicing a xml version of a graph                            *)
(**********************************************************************)

(* each node has an unique integer identifier *)
type visual_heap_node =
  | VH_dangling of int * Sil.exp
  | VH_pointsto of int * Sil.exp * Sil.strexp * Sil.exp (* VH_pointsto(id,address,content,type) *)
  | VH_lseg of int * Sil.exp * Sil.exp * Sil.lseg_kind (*VH_lseg(id,address,content last cell, kind) *)
  (*VH_dllseg(id, address, content first cell, content last cell, address last cell, kind) *)
  | VH_dllseg of int * Sil.exp * Sil.exp * Sil.exp * Sil.exp * Sil.lseg_kind

(* an edge is a pair of node identifiers*)
type visual_heap_edge = {
  src: int;
  trg: int;
  lab: string
}

let mk_visual_heap_edge s t l = { src = s; trg = t; lab = l }

(* used to generate unique identifier for all the nodes in the set of visual graphs used to *)
(* represent a proposition*)
let global_node_counter = ref 0

let working_list = ref []

let set_dangling_nodes = ref []

(* convert an exp into a string which is xml friendly, ie. special character are replaced by*)
(* the proper xml way to visualize them*)
let exp_to_xml_string e =
  pp_to_string (Sil.pp_exp (pe_html Black)) e

(* convert an atom into an xml-friendly string without special characters *)
let atom_to_xml_string a =
  pp_to_string (Sil.pp_atom (pe_html Black)) a

(* return the dangling node corresponding to an expression it exists or None *)
let exp_dangling_node e =
  let entry_e = IList.filter (fun b -> match b with
      | VH_dangling(_, e') -> Sil.exp_equal e e' | _ -> false ) !set_dangling_nodes in
  match entry_e with
  |[] -> None
  | VH_dangling(n, e') :: _ -> Some (VH_dangling(n, e'))
  | _ -> None (* NOTE: this cannot be possible since entry_e can be composed only by VH_dangling, see def of entry_e*)

(* make nodes and when it finds a list records in the working list         *)
(* to do (n, prop) where n is the integer identifier of the list node.     *)
(* This allow to keep the connection between the list node and the graph   *)
(* that displays its contents.                                             *)
let rec make_visual_heap_nodes sigma =
  let n = !global_node_counter in
  incr global_node_counter;
  match sigma with
  | [] -> []
  | Sil.Hpointsto (e, se, t):: sigma' ->
      VH_pointsto(n, e, se, t):: make_visual_heap_nodes sigma'
  | Sil.Hlseg (k, hpara, e1, e2, elist):: sigma' ->
      working_list:= (n, hpara.Sil.body)::!working_list;
      VH_lseg(n, e1, e2, k):: make_visual_heap_nodes sigma'
  | Sil.Hdllseg (k, hpara_dll, e1, e2, e3, e4, elist):: sigma'->
      working_list:= (n, hpara_dll.Sil.body_dll)::!working_list;
      VH_dllseg(n, e1, e2, e3, e4, k):: make_visual_heap_nodes sigma'

(* given a node returns its id and address*)
let get_node_id_and_addr node =
  match node with
  | VH_dangling(n, e)
  | VH_pointsto(n, e, _, _)
  | VH_lseg(n, e, _ , _)
  | VH_dllseg(n, e, _, _, _, _) -> (n, e)

(* return node's id*)
let get_node_id node = fst (get_node_id_and_addr node)

(* return node's address*)
let get_node_addr node = snd (get_node_id_and_addr node)

(* return the nodes corresponding to an address given by an expression *)
let rec select_node_at_address nodes e =
  match nodes with
  | [] -> None
  | n:: l' ->
      let e' = get_node_addr n in
      if (Sil.exp_compare e e' = 0) then Some n
      else select_node_at_address l' e

(* look-up the ids in the list of nodes corresponding to expression e*)
(* let look_up_nodes_ids nodes e =
   IList.map get_node_id (select_nodes_exp nodes e) *)

(* create a list of dangling nodes *)
let make_set_dangling_nodes allocated_nodes (sigma: Sil.hpred list) =
  let make_new_dangling e =
    let n = !global_node_counter in
    incr global_node_counter;
    VH_dangling(n, e) in
  let get_rhs_predicate hpred =
    (match hpred with
     | Sil.Hpointsto (_, Sil.Eexp (e, inst), _) when not (Sil.exp_equal e Sil.exp_zero) -> [e]
     | Sil.Hlseg (_, _, _, e2, _) when not (Sil.exp_equal e2 Sil.exp_zero) -> [e2]
     | Sil.Hdllseg (_, _, e1, e2, e3, _, _) ->
         if (Sil.exp_equal e2 Sil.exp_zero) then
           if (Sil.exp_equal e3 Sil.exp_zero) then []
           else [e3]
         else [e2; e3]
     | Sil.Hpointsto (_, _, _)
     | _ -> [] (* arrays and struct do not give danglings. CHECK THIS!*)
    ) in
  let is_not_allocated e =
    let allocated = IList.exists (fun a -> match a with
        | VH_pointsto(_, e', _, _)
        | VH_lseg(_, e', _ , _)
        | VH_dllseg(_, e', _, _, _, _) -> Sil.exp_equal e e'
        | _ -> false ) allocated_nodes in
    not allocated in
  let rec filter_duplicate l seen_exp =
    match l with
    | [] -> []
    | e:: l' ->
        if (IList.exists (Sil.exp_equal e) seen_exp) then filter_duplicate l' seen_exp
        else e:: filter_duplicate l' (e:: seen_exp) in
  let rhs_exp_list = IList.flatten (IList.map get_rhs_predicate sigma) in
  let candidate_dangling_exps = filter_duplicate rhs_exp_list [] in
  let dangling_exps = IList.filter is_not_allocated candidate_dangling_exps in  (* get rid of allocated ones*)
  IList.map make_new_dangling dangling_exps

(* return a list of pairs (n,field_lab) where n is a target node*)
(* corresponding to se and is going to be used a target for and edge*)
(* field_lab is the name of the field which points to n (if any)*)
let rec compute_target_nodes_from_sexp nodes se prop field_lab =
  match se with
  | Sil.Eexp (e, inst) when is_nil e prop -> [] (* Nil is not represented by a node, it's just a value which should be printed*)
  | Sil.Eexp (e, inst) ->
      let e_node = select_node_at_address nodes e in
      (match e_node with
       | None ->
           (match exp_dangling_node e with
            | None -> []
            | Some dang_node -> [(dang_node, field_lab)]
           )
       | Some n -> [(n, field_lab)]
      )
  | Sil.Estruct (lfld, inst) ->
      (match lfld with
       | [] -> []
       | (fn, se2):: l' ->
           compute_target_nodes_from_sexp nodes se2 prop (Ident.fieldname_to_string fn) @
           compute_target_nodes_from_sexp nodes (Sil.Estruct (l', inst)) prop ""
      )
  | Sil.Earray(size, lie, inst) ->
      (match lie with
       | [] -> []
       | (idx, se2):: l' ->
           let lab ="["^exp_to_xml_string idx^"]" in
           compute_target_nodes_from_sexp nodes se2 prop lab @
           compute_target_nodes_from_sexp nodes (Sil.Earray(size, l', inst)) prop ""
      )


(* build the set of edges between nodes *)
let rec make_visual_heap_edges nodes sigma prop =
  let combine_source_target_label n (m, lab) =
    mk_visual_heap_edge (get_node_id n) (get_node_id m) lab in
  match sigma with
  | [] -> []
  | Sil.Hpointsto (e, se, t):: sigma' ->
      let e_node = select_node_at_address nodes e in
      (match e_node with
       | None -> assert false
       | Some n ->
           let target_nodes = compute_target_nodes_from_sexp nodes se prop "" in
           let ll = IList.map (combine_source_target_label n) target_nodes in
           ll @ make_visual_heap_edges nodes sigma' prop
      )
  | Sil.Hlseg (_, pred, e1, e2, elist):: sigma' ->
      let e1_node = select_node_at_address nodes e1 in
      (match e1_node with
       | None -> assert false
       | Some n ->
           let target_nodes = compute_target_nodes_from_sexp nodes (Sil.Eexp (e2, Sil.inst_none)) prop "" in
           let ll = IList.map (combine_source_target_label n) target_nodes in
           ll @ make_visual_heap_edges nodes sigma' prop
      )

  | Sil.Hdllseg (_, pred, e1, e2, e3, e4, elist):: sigma' ->
      let e1_node = select_node_at_address nodes e1 in
      (match e1_node with
       | None -> assert false
       | Some n ->
           let target_nodesF = compute_target_nodes_from_sexp nodes (Sil.Eexp (e3, Sil.inst_none)) prop "" in
           let target_nodesB = compute_target_nodes_from_sexp nodes (Sil.Eexp (e2, Sil.inst_none)) prop "" in
           let llF = IList.map (combine_source_target_label n) target_nodesF in
           let llB = IList.map (combine_source_target_label n) target_nodesB in
           llF @ llB @ make_visual_heap_edges nodes sigma' prop
      )

(* from a prop generate and return visual proposition *)
let prop_to_set_of_visual_heaps prop =
  let result = ref [] in
  working_list:=[(!global_node_counter, Prop.get_sigma prop)];
  incr global_node_counter;
  while (!working_list!=[]) do
    set_dangling_nodes:=[];
    let (n, h) = IList.hd !working_list in
    working_list:= IList.tl !working_list;
    let nodes = make_visual_heap_nodes h in
    set_dangling_nodes:= make_set_dangling_nodes nodes h;
    let edges = make_visual_heap_edges nodes h prop in
    result:= !result @ [(n, nodes @ !set_dangling_nodes, edges)];
  done;
  !result

let rec pointsto_contents_to_xml (co: Sil.strexp) : Io_infer.Xml.node =
  match co with
  | Sil.Eexp (e, inst) ->
      Io_infer.Xml.create_tree "cell" [("content-value", exp_to_xml_string e)] []
  | Sil.Estruct (fel, _) ->
      let f (fld, exp) = Io_infer.Xml.create_tree "struct-field" [("id", Ident.fieldname_to_string fld)] [(pointsto_contents_to_xml exp)] in
      Io_infer.Xml.create_tree "struct" [] (IList.map f fel)
  | Sil.Earray (size, nel, _) ->
      let f (e, se) = Io_infer.Xml.create_tree "array-element" [("index", exp_to_xml_string e)] [pointsto_contents_to_xml se] in
      Io_infer.Xml.create_tree "array" [("size", exp_to_xml_string size)] (IList.map f nel)

(* Convert an atom to xml in a light version. Namely, the expressions are not fully blown-up into *)
(* xml tree but visualized as strings *)
let atom_to_xml_light (a: Sil.atom) : Io_infer.Xml.node =
  let kind_info = match a with
    | Sil.Aeq _ when Prop.atom_is_inequality a ->
        "inequality"
    | Sil.Aeq _ ->
        "equality"
    | Sil.Aneq _ ->
        "disequality" in
  Io_infer.Xml.create_tree "stack-variable" [("type", kind_info); ("instance", atom_to_xml_string a)] []

let xml_pure_info prop =
  let pure = Prop.get_pure prop in
  let xml_atom_list = IList.map atom_to_xml_light pure in
  Io_infer.Xml.create_tree "stack" [] xml_atom_list

(** Return a string describing the kind of a pointsto address *)
let pointsto_addr_kind = function
  | Sil.Lvar pv ->
      if Sil.pvar_is_global pv
      then "global"
      else if Sil.pvar_is_local pv && Mangled.equal (Sil.pvar_get_name pv) Ident.name_return
      then "return"
      else if Sil.pvar_is_local pv
      then "parameter"
      else "other"
  | _ -> "other"

let heap_node_to_xml node =
  match node with
  | VH_dangling(id, addr) ->
      let atts =[("id", string_of_int id); ("address", exp_to_xml_string addr); ("node-type","dangling"); ("memory-type", pointsto_addr_kind addr)] in
      Io_infer.Xml.create_tree "node" atts []
  | VH_pointsto(id, addr, cont, t) ->
      let atts =[("id", string_of_int id); ("address", exp_to_xml_string addr); ("node-type","allocated"); ("memory-type", pointsto_addr_kind addr)] in
      let contents = pointsto_contents_to_xml cont in
      Io_infer.Xml.create_tree "node" atts [contents]
  | VH_lseg(id, addr, cont, Sil.Lseg_NE) ->
      let atts =[("id", string_of_int id); ("address", exp_to_xml_string addr); ("node-type","single linked list"); ("list-type","non-empty"); ("memory-type", "other")] in
      Io_infer.Xml.create_tree "node" atts []
  | VH_lseg(id, addr, cont, Sil.Lseg_PE) ->
      let atts =[("id", string_of_int id); ("address", exp_to_xml_string addr); ("node-type","single linked list"); ("list-type","possibly empty"); ("memory-type", "other")] in
      Io_infer.Xml.create_tree "node" atts []
  | VH_dllseg(id, addr1, cont1, cont2, addr2, k) ->
      let contents1 = pointsto_contents_to_xml (Sil.Eexp (cont1, Sil.inst_none)) in
      let contents2 = pointsto_contents_to_xml (Sil.Eexp (cont2, Sil.inst_none)) in
      let atts =[("id", string_of_int id); ("addr-first", exp_to_xml_string addr1); ("addr-last", exp_to_xml_string addr2); ("node-type","double linked list"); ("memory-type", "other") ] in
      Io_infer.Xml.create_tree "node" atts [contents1 ; contents2]

let heap_edge_to_xml edge =
  let atts =[("source", string_of_int edge.src); ("target", string_of_int edge.trg); ("label", edge.lab) ] in
  Io_infer.Xml.create_tree "edge" atts []

let visual_heap_to_xml heap =
  let (n, nodes, edges) = heap in
  let xml_heap_nodes = IList.map heap_node_to_xml nodes in
  let xml_heap_edges = IList.map heap_edge_to_xml edges in
  Io_infer.Xml.create_tree "heap" [("id", string_of_int n)] (xml_heap_nodes @ xml_heap_edges)

(** convert a proposition to xml with the given tag and id *)
let prop_to_xml prop tag_name id =
  let visual_heaps = prop_to_set_of_visual_heaps prop in
  let xml_visual_heaps = IList.map visual_heap_to_xml visual_heaps in
  let xml_pure_part = xml_pure_info prop in
  let xml_graph = Io_infer.Xml.create_tree tag_name [("id", string_of_int id)] (xml_visual_heaps @ [xml_pure_part]) in
  xml_graph

(** reset the counter used for node and heap identifiers *)
let reset_node_counter () =
  global_node_counter := 0

let print_specs_xml signature specs loc fmt =
  reset_node_counter ();
  let do_one_spec pre posts n =
    let add_stack_to_prop _prop =
      let pre_stack = fst (Prop.sigma_get_stack_nonstack true (Prop.get_sigma pre)) in (* add stack vars from pre *)
      let _prop' = Prop.replace_sigma (pre_stack @ Prop.get_sigma _prop) _prop in
      Prop.normalize _prop' in
    let jj = ref 0 in
    let xml_pre = prop_to_xml pre "precondition" !jj in
    let xml_spec = xml_pre:: (IList.map (fun (po, path) -> jj:=!jj + 1; prop_to_xml (add_stack_to_prop po) "postcondition" !jj) posts) in
    Io_infer.Xml.create_tree "specification" [("id", string_of_int n)] xml_spec in
  let j = ref 0 in
  let list_of_specs_xml =
    IList.map
      (fun s ->
         j:=!j + 1;
         do_one_spec (Specs.Jprop.to_prop s.Specs.pre) s.Specs.posts !j)
      specs in
  let xml_specifications = Io_infer.Xml.create_tree "specifications" [] list_of_specs_xml in
  let xml_signature = Io_infer.Xml.create_tree "signature" [("name", signature)] [] in
  let proc_summary = Io_infer.Xml.create_tree "procedure"
      [("file", DB.source_file_to_string loc.Location.file);
       ("line", string_of_int loc.Location.line)]
      [xml_signature; xml_specifications] in
  Io_infer.Xml.pp_document true fmt proc_summary