<commit_before>(********************************************************
   This file is part of jStar 
	src/symbexe/symexec.ml
   Release 
        $Release$
   Version 
        $Rev$
   $Copyright$
   
   jStar is distributed under a BSD license,  see, 
      LICENSE.txt
 ********************************************************)

open Cfg_core
open Methdec_core
open Psyntax
open Sepprover
open Spec
open Specification
open Vars


(* global variables *)

let curr_logic : Psyntax.logic ref = ref Psyntax.empty_logic
let curr_abs_rules : Psyntax.logic ref = ref Psyntax.empty_logic





(* ================  transition system ==================  *)
type ntype = 
    Plain | Good | Error | Abs | UnExplored

type id = int

let file = ref ""

let set_group,grouped = let x = ref false in (fun y -> x := y),(fun () -> !x )

let fresh_node = let node_counter = ref 0 in fun () ->  let x = !node_counter in node_counter := x+1; x

let fresh_file = let file_id = ref 0 in fun () -> let x = !file_id in file_id := x+1;  Sys.getcwd() ^  "/" ^ !file ^ ".proof_file_"^(string_of_int x)^".txt"


type node = {mutable content : string; id : id; mutable ntype : ntype; mutable url : string; mutable edges : edge list; cfg : stmt_core option}
and  edge = string * string * node * node * string option
  (** An edge has a label, a ???, source, target, and perhaps an URL. *)

let graphe = ref []


let mk_node c id nt url ed cfg =
 { content =c; 
   id =id; 
   ntype =nt; 
   url =url; 
   edges =ed; 
   cfg =cfg
 }

let node_get_content (n:node) : string = 
  n.content 

let node_get_idd (n:node) : id = 
  n.id 

let node_get_ntype (n:node) : ntype = 
  n.ntype 

let node_get_url (n:node) : string = 
  n.url 


module Idmap = 
  Map.Make(struct 
	     type t = int option 
	     let compare = compare
	   end)

let graphn = ref  Idmap.empty
let startnodes : node list ref = ref []

let make_start_node node = startnodes := node::!startnodes

let pp_dotty_transition_system () =
  let foname = (!file) ^ ".execution_core.dot~" in
  let dotty_outf=open_out foname in
  if Config.symb_debug() then Printf.printf "\n Writing transition system file execution_core.dot  \n";
  Printf.fprintf dotty_outf "digraph main { \nnode [shape=box,  labeljust=l];\n\n";
  Idmap.iter 
    (fun cfg nodes -> (
      (* Print Abs nodes. *)
      (if grouped () then 
        match cfg with Some cfg -> Printf.fprintf dotty_outf "subgraph cluster_cfg%i {\n"  cfg | _ -> ());
      List.iter (fun {content=label;id=id;ntype=ty;url=url;cfg=cfg} ->
	let label=Dot.escape_for_label label in
	let url = if url = "" then "" else ", URL=\"file://" ^ url ^"\"" in
	match ty with 
	| Plain -> ()
	| Good ->  ()
	| Error ->  ()
	| UnExplored -> ()
	| Abs ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l, color=yellow, style=filled%s]\n" id label url)
	nodes;
      if grouped () then match cfg with Some _ -> Printf.fprintf dotty_outf "\n}\n" | _ -> ());
      (* Print non-Abs nodes. *)
      List.iter (fun {content=label;id=id;ntype=ty;url=url;cfg=cfg} ->
	let label=Dot.escape_for_label label in
	let url = if url = "" then "" else ", URL=\"file://" ^ url ^"\"" in
	match ty with 
	  Plain ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l%s]\n" id label url
	| Good ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l, color=green, style=filled%s]\n" id label url
	| Error ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l, color=red, style=filled%s]\n" id label url
	| UnExplored ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l, color=orange, style=filled%s]\n" id label url
	| Abs -> () )
	nodes;
    )
    !graphn;
  List.iter (fun (l,c,s,d,o) ->
    let l = Dot.escape_for_label l in
    let c = Dot.escape_for_label c in
    Printf.fprintf dotty_outf "\n state%i -> state%i [label=\"%s\", tooltip=\"%s\"%s]" s.id d.id l c
	    (match o with 
	      None -> ""
	    | Some f -> Printf.sprintf ", URL=\"file://%s\", fontcolor=blue" f))
    !graphe;
  Printf.fprintf dotty_outf "\n\n\n}";
  close_out dotty_outf;
  let fname = (!file) ^ ".execution_core.dot" in
  if Sys.file_exists fname then Sys.remove fname;
  Sys.rename foname (!file ^ ".execution_core.dot")


let add_node (label : string) (ty : ntype) (cfg : stmt_core option) = 
  let id = fresh_node () in 
  let node = {content=label; id=id;ntype=ty;url=""; edges=[]; cfg = cfg} in 
  let cfgid = 
    match cfg with 
      None -> None 
    | Some cfg -> Some (cfg.sid) in 
  graphn := Idmap.add cfgid (node::(try Idmap.find cfgid !graphn with Not_found -> [])) !graphn;
  node

let add_error_node label = add_node label Error None
let add_abs_node label cfg = add_node label Abs (Some cfg)
let add_good_node label = add_node label Good None
let add_node_unexplored label cfg = add_node label UnExplored (Some cfg)
let add_node label cfg = add_node label UnExplored (Some cfg)

let explore_node src = if src.ntype = UnExplored then src.ntype <- Plain

let add_abs_heap_node (heap : Sepprover.inner_form) cfg= 
  (Format.fprintf (Format.str_formatter) "%a" Sepprover.string_inner_form heap);
  add_abs_node (Format.flush_str_formatter ()) cfg

let add_heap_node (heap : inner_form) cfg = 
  (Format.fprintf (Format.str_formatter) "%a" Sepprover.string_inner_form heap);
  add_node (Format.flush_str_formatter ()) cfg

let add_error_heap_node (heap : inner_form) = 
  (Format.fprintf (Format.str_formatter) "%a" Sepprover.string_inner_form heap);
  add_error_node (Format.flush_str_formatter ())

let x = ref 0


let add_edge src dest label = 
  let edge = (label, "", src, dest, None) in
  graphe := edge::!graphe;
  src.edges <- edge::src.edges;
  explore_node src;
  x := (!x + 1) mod 5;
  if !x = 0 then pp_dotty_transition_system ()


let add_edge_with_proof src dest label = 
  let f = fresh_file() in
  let out = open_out f in
  Sepprover.pprint_proof out;
  close_out out;
  explore_node src;
  let edge = (label, "", src, dest, Some f) in 
  graphe := edge::!graphe;
  src.edges <- edge::src.edges;
  if !x = 5 then (x:=0; pp_dotty_transition_system ()) else x :=!x+1

let add_url_to_node src proof = 
  let f = fresh_file() in
  let out = open_out f in
  List.iter (output_string out) proof;
  close_out out;
  src.url <- f

let add_id_form h cfg =
    let id=add_heap_node h cfg in
    (h,id)

let add_id_formset sheaps cfg =  List.map (fun h -> add_id_form h cfg) sheaps

let add_id_formset_edge src label sheaps cfg =  
  match sheaps with 
    [] ->
      if Config.symb_debug() then Printf.printf "\n\nInconsistent heap. Skip it!\n";
      let idd = add_good_node "Inconsistent" in add_edge_with_proof src idd (label ^"\n Inconsistent");
	[]
  | _ -> 
  let sheaps_id = add_id_formset sheaps cfg in
  List.iter (fun dest -> add_edge_with_proof src (snd dest) label) sheaps_id;
  sheaps_id

let add_id_abs_form cfg h =
    let id=add_abs_heap_node h cfg in
    (h,id)

let add_id_abs_formset sheaps cfg =  List.map (add_id_abs_form cfg) sheaps
<commit_msg>Small tweak.<commit_after>(********************************************************
   This file is part of jStar 
	src/symbexe/symexec.ml
   Release 
        $Release$
   Version 
        $Rev$
   $Copyright$
   
   jStar is distributed under a BSD license,  see, 
      LICENSE.txt
 ********************************************************)

open Cfg_core
open Methdec_core
open Psyntax
open Sepprover
open Spec
open Specification
open Vars


(* global variables *)

let curr_logic : Psyntax.logic ref = ref Psyntax.empty_logic
let curr_abs_rules : Psyntax.logic ref = ref Psyntax.empty_logic





(* ================  transition system ==================  *)
type ntype = 
    Plain | Good | Error | Abs | UnExplored

type id = int

let file = ref ""

let set_group,grouped = let x = ref false in (fun y -> x := y),(fun () -> !x )

let fresh_node = let node_counter = ref 0 in fun () ->  let x = !node_counter in node_counter := x+1; x

let fresh_file = let file_id = ref 0 in fun () -> let x = !file_id in file_id := x+1;  Sys.getcwd() ^  "/" ^ !file ^ ".proof_file_"^(string_of_int x)^".txt"


type node = {mutable content : string; id : id; mutable ntype : ntype; mutable url : string; mutable edges : edge list; cfg : stmt_core option}
and  edge = string * string * node * node * string option
  (** An edge has a label, a ???, source, target, and perhaps an URL. *)

let graphe = ref []


let mk_node c id nt url ed cfg =
 { content =c; 
   id =id; 
   ntype =nt; 
   url =url; 
   edges =ed; 
   cfg =cfg
 }

let node_get_content (n:node) : string = 
  n.content 

let node_get_idd (n:node) : id = 
  n.id 

let node_get_ntype (n:node) : ntype = 
  n.ntype 

let node_get_url (n:node) : string = 
  n.url 


module Idmap = 
  Map.Make(struct 
	     type t = int option 
	     let compare = compare
	   end)

let graphn = ref  Idmap.empty
let startnodes : node list ref = ref []

let make_start_node node = startnodes := node::!startnodes

let pp_dotty_transition_system () =
  let foname = (!file) ^ ".execution_core.dot~" in
  let dotty_outf=open_out foname in
  if Config.symb_debug() then Printf.printf "\n Writing transition system file execution_core.dot  \n";
  Printf.fprintf dotty_outf "digraph main { \nnode [shape=box,  labeljust=l];\n\n";
  Idmap.iter 
    (fun cfg nodes -> (
      (* Print Abs nodes. *)
      (if grouped () then 
        match cfg with Some cfg -> Printf.fprintf dotty_outf "subgraph cluster_cfg%i {\n"  cfg | _ -> ());
      List.iter (fun {content=label;id=id;ntype=ty;url=url;cfg=cfg} ->
	let label=Dot.escape_for_label label in
	let url = if url = "" then "" else ", URL=\"file://" ^ url ^"\"" in
	match ty with 
	| Plain -> ()
	| Good ->  ()
	| Error ->  ()
	| UnExplored -> ()
	| Abs ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l, color=yellow, style=filled%s]\n" id label url)
	nodes;
      if grouped () then match cfg with Some _ -> Printf.fprintf dotty_outf "\n}\n" | _ -> ());
      (* Print non-Abs nodes. *)
      List.iter (fun {content=label;id=id;ntype=ty;url=url;cfg=cfg} ->
	let label=Dot.escape_for_label label in
	let url = if url = "" then "" else ", URL=\"file://" ^ url ^"\"" in
	match ty with 
	  Plain ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l%s]\n" id label url
	| Good ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l, color=green, style=filled%s]\n" id label url
	| Error ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l, color=red, style=filled%s]\n" id label url
	| UnExplored ->  Printf.fprintf dotty_outf "\n state%i[label=\"%s\",labeljust=l, color=orange, style=filled%s]\n" id label url
	| Abs -> () )
	nodes;
    )
    !graphn;
  List.iter (fun (l,c,s,d,o) ->
    let l = Dot.escape_for_label l in
    let c = Dot.escape_for_label c in
    Printf.fprintf dotty_outf "\n state%i -> state%i [label=\"%s\", tooltip=\"%s\"%s]" s.id d.id l c
	    (match o with 
	      None -> ""
	    | Some f -> Printf.sprintf ", URL=\"file://%s\", fontcolor=blue" f))
    !graphe;
  Printf.fprintf dotty_outf "\n\n\n}";
  close_out dotty_outf;
  let fname = (!file) ^ ".execution_core.dot" in
  if Sys.file_exists fname then Sys.remove fname;
  Sys.rename foname (!file ^ ".execution_core.dot")


let add_node (label : string) (ty : ntype) (cfg : stmt_core option) = 
  let id = fresh_node () in 
  let node = {content=label; id=id;ntype=ty;url=""; edges=[]; cfg = cfg} in 
  let cfgid = 
    match cfg with 
      None -> None 
    | Some cfg -> Some (cfg.sid) in 
  graphn := Idmap.add cfgid (node::(try Idmap.find cfgid !graphn with Not_found -> [])) !graphn;
  node

let add_error_node label = add_node label Error None
let add_abs_node label cfg = add_node label Abs (Some cfg)
let add_good_node label = add_node label Good None
let add_node_unexplored label cfg = add_node label UnExplored (Some cfg)
let add_node label cfg = add_node label UnExplored (Some cfg)

let explore_node src = if src.ntype = UnExplored then src.ntype <- Plain

let add_abs_heap_node (heap : Sepprover.inner_form) cfg= 
  (Format.fprintf (Format.str_formatter) "%a" Sepprover.string_inner_form heap);
  add_abs_node (Format.flush_str_formatter ()) cfg

let add_heap_node (heap : inner_form) cfg = 
  (Format.fprintf (Format.str_formatter) "%a" Sepprover.string_inner_form heap);
  add_node (Format.flush_str_formatter ()) cfg

let add_error_heap_node (heap : inner_form) = 
  (Format.fprintf (Format.str_formatter) "%a" Sepprover.string_inner_form heap);
  add_error_node (Format.flush_str_formatter ())

let add_edge_common = 
  let x = ref 0 in
  fun src dst lbl f ->
  let e = (lbl, "", src, dst, f) in
  graphe := e :: !graphe;
  src.edges <- e :: src.edges;
  explore_node src;
  x := (!x + 1) mod 5;
  if !x = 0 then pp_dotty_transition_system ()

let add_edge src dest label = 
  add_edge_common src dest label None

let add_edge_with_proof src dest label = 
  let f = fresh_file() in
  let out = open_out f in
  Sepprover.pprint_proof out;
  close_out out;
  add_edge_common src dest label (Some f)

let add_url_to_node src proof = 
  let f = fresh_file() in
  let out = open_out f in
  List.iter (output_string out) proof;
  close_out out;
  src.url <- f

let add_id_form h cfg =
    let id=add_heap_node h cfg in
    (h,id)

let add_id_formset sheaps cfg =  List.map (fun h -> add_id_form h cfg) sheaps

let add_id_formset_edge src label sheaps cfg =  
  match sheaps with 
    [] ->
      if Config.symb_debug() then Printf.printf "\n\nInconsistent heap. Skip it!\n";
      let idd = add_good_node "Inconsistent" in add_edge_with_proof src idd (label ^"\n Inconsistent");
	[]
  | _ -> 
  let sheaps_id = add_id_formset sheaps cfg in
  List.iter (fun dest -> add_edge_with_proof src (snd dest) label) sheaps_id;
  sheaps_id

let add_id_abs_form cfg h =
    let id=add_abs_heap_node h cfg in
    (h,id)

let add_id_abs_formset sheaps cfg =  List.map (add_id_abs_form cfg) sheaps

{'fraction_non_alphanumeric': 0.14724721122706008, 'fraction_numerical': 0.0013673983447283196, 'mean_word_length': 3.3766929133858268, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 68, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7424361', 'n_tokens_mistral': 5200, 'n_tokens_neox': 5016, 'n_words': 1477}