000001| (** Overall analysis lattice *)
000002|
000003| module LabelMap = Map.Make(struct type t = int
000004| let compare i i' = (*[1499631]*)i - i' end)
000005|
000006| type elem = Statelattice.elem LabelMap.t
000007|
000008| (* leq : elem -> elem -> bool *)
000009| let leq st0 st1 =
000010| (*[16000]*)LabelMap.fold (fun lab obj acc ->
000011| (*[71230]*)let obj' = try (*[71230]*)LabelMap.find lab st1
000013| in (*[71230]*)acc && (*[71230]*)Statelattice.leq obj obj') st0 true
000014|
000015| (* eq : elem -> elem -> bool *)
000016| let eq = (*[1]*)LabelMap.equal (Statelattice.eq)
000017|
000018| (* join : elem -> elem -> elem *)
000019| let join st0 st1 = (*[13000]*)LabelMap.merge (fun lab obj0 obj1 -> match obj0,obj1 with
000020| | None,_ -> (*[62520]*)obj1
000021| | _,None -> (*[52081]*)obj0
000022| | Some obj0,Some obj1 -> (*[39166]*)Some (Statelattice.join obj0 obj1)) st0 st1
000023|
000024| (* meet : elem -> elem -> elem *)
000025| let meet st0 st1 = (*[13000]*)LabelMap.merge (fun lab obj0 obj1 -> match obj0,obj1 with
000026| | None,_ -> (*[60143]*)None
000027| | _,None -> (*[37895]*)None
000028| | Some obj0,Some obj1 -> (*[41332]*)Some (Statelattice.meet obj0 obj1)) st0 st1
000029|
000030| (* bot : elem *)
000031| let bot = (*[1]*)LabelMap.empty
000032|
000033|
000034| (** {3 Lattice operations } *)
000035|
000036| (* init : elem *)
000037| let init = (*[1]*)LabelMap.empty
000038|
000039| (* lookup : elem -> label -> Statelattice.elem *)
000040| let lookup lat lab =
000041| (*[5000]*)try (*[5000]*)LabelMap.find lab lat
000042| with Not_found -> (*[4124]*)Statelattice.bot
000043|
000044| (* add : elem -> label -> Statelattice.elem -> elem *)
000045| let add lat lab sl =
000046| (*[8000]*)LabelMap.add lab sl lat
000047|
000048|
000049| (** {2 Pretty printing} *)
000050|
000051| (* pprint : elem -> unit *)
000052| let pprint alat =
000053| begin
000054| Format.printf "{ @[<v 0>";
000055| ignore (LabelMap.fold (fun lab slat first ->
000056| begin
000057| (if first then () else Format.print_space ());
000058| Format.printf "%-is -> " lab;
000059| Statelattice.pprint slat;
000060| false
000061| end) alat true);
000062| Format.printf "@] }";
000063| end
000064|
000065| (* to_string : elem -> string *)
000066| let to_string alat =
000067| let buf = Buffer.create 512 in
000068| let out,flush = Format.get_formatter_output_functions () in (* save previous outputters *)
000069| begin
000070| Format.set_formatter_output_functions (Buffer.add_substring buf) (fun () -> ());
000071| pprint alat;
000072| Format.print_flush ();
000073| Format.set_formatter_output_functions out flush; (* restore previous outputters *)
000074| Buffer.contents buf
000075| end
000012| with Not_found -> (*[0]*)Statelattice.bot