package rdbg

  1. Overview
  2. Docs

Source file lutinRdbg.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
(* Time-stamp: <modified the 16/03/2020 (at 11:33) by Erwan Jahier> *)


type lut_evt =
  | Ltop | Call | Exit 
  | Quit (* when a run is quited*)
  | Try  (* Try a constraint to compute the current step *)
  | Sat  (* the tryied constraint is Satisfiable *)
  | Nsat (* the tryied constraint is Not satisfiable *)
(*   | Deadlock *)
(* 
   (Ltop (Call (Try.Nsat*.Sat))* Exit)* )*
 *)


let (to_lut_evt: RdbgEvent.kind -> lut_evt) = function 
  | RdbgEvent.Ltop -> Ltop
  | RdbgEvent.Call -> Call
  | RdbgEvent.Exit -> Exit
(*   | RdbgEvent.Abort -> Deadlock *)
  | RdbgEvent.MicroStep "try " -> Try
  | RdbgEvent.MicroStep "sat " -> Sat
  | RdbgEvent.MicroStep "usat" -> Nsat
  | RdbgEvent.MicroStep "quit" -> Quit
  | RdbgEvent.MicroStep e -> failwith (e^": Unknown event")

let (from_lut_evt: lut_evt  -> RdbgEvent.kind) = function
  | Ltop -> RdbgEvent.Ltop
  | Call -> RdbgEvent.Call
  | Exit -> RdbgEvent.Exit
  | Quit -> RdbgEvent.MicroStep "quit"
  | Try  -> RdbgEvent.MicroStep "try "
  | Sat  -> RdbgEvent.MicroStep "sat "
  | Nsat -> RdbgEvent.MicroStep "usat"
(*   | Deadlock -> RdbgEvent.Abort *)


(***************************************************************************)
(* a very simple Lutin Profiler *)
open RdbgEvent

let prof_tbl = Hashtbl.create 50 

let incr_prof (si:RdbgEvent.src_info_atom) = 
  try 
    let cpt = Hashtbl.find prof_tbl si in
      Hashtbl.replace prof_tbl si (cpt+1)
  with 
      Not_found -> Hashtbl.add prof_tbl si 1
 
let (prof_add: RdbgEvent.t -> unit) =
  fun e ->     
    match to_lut_evt e.kind, e.sinfo with
      | (Sat | Nsat), Some src -> List.iter incr_prof (src()).atoms
      | _ -> ()

let (profiler : bool -> unit) = 
  fun on -> 
    if on then RdbgStdLib.add_hook "profile" prof_add 
          else RdbgStdLib.del_hook "profile"

let (reset_profiler : unit -> unit) = 
  fun () -> 
    Hashtbl.clear prof_tbl

let (dump_profile_info : unit -> string) =
  fun () -> 
    let str_l = 
      Hashtbl.fold
        (fun si cpt acc-> 
           (Printf.sprintf "| %3i-%-3i | %5i-%-5i | %4i | %40s | %10s | \n" 
              (fst si.line) (snd si.line) (fst si.char) (snd si.char) 
              cpt si.str (Filename.basename si.file))::acc
        )
        prof_tbl
        []
    in
    let str_l = List.sort compare str_l in
      ("
|---------+-------------+------+------------------------------------------+------------+ 
|  lines  |    chars    | hits |             source code                  | file name  |
|---------+-------------+------+------------------------------------------+------------+
") ^
        (String.concat "" str_l) ^
        ("|---------+-------------+------+------------------------------------------+------------+ \n")


(***************************************************************************)
let (explain_failure : RdbgEvent.t -> unit) = 
  fun e ->
    (match to_lut_evt e.kind, e.sinfo with
      | Nsat, Some src_info -> 
        let si = src_info () in 
        print_string "\n\nThe current constraint is unsatisfiable:\n";
        Expr.dump si.expr;
        (match si.more with
          | None -> () 
          | Some more -> 
            print_string "\nBecause this one is unsatisfiable:\n";
            Expr.dump (more ()))
      | Nsat, None -> print_string "No source info is avaible.\n"
      | _,_ -> print_string "Current RdbgEvent is not a usat event.\n"
    );
    flush stdout