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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
open BinPos
open Coqlib
open Datatypes
open LTL
open Lattice
open CList
open Maps
open Camlcoq
(* Trivial enumeration, in decreasing order of PC *)
(***
let enumerate_aux f reach =
positive_rec
Coq_nil
(fun pc nodes ->
if PMap.get pc reach
then Coq_cons (pc, nodes)
else nodes)
f.fn_nextpc
***)
(* More clever enumeration that flattens basic blocks *)
let rec int_of_pos = function
| Coq_xI p -> (int_of_pos p lsl 1) + 1
| Coq_xO p -> int_of_pos p lsl 1
| Coq_xH -> 1
let rec pos_of_int n =
if n = 0 then assert false else
if n = 1 then Coq_xH else
if n land 1 = 0
then Coq_xO (pos_of_int (n lsr 1))
else Coq_xI (pos_of_int (n lsr 1))
(* Build the enumeration *)
module IntSet = Set.Make(struct type t = int let compare = compare end)
let enumerate_aux f reach =
let enum = ref [] in
let emitted = Array.make (int_of_pos f.fn_nextpc) false in
let rec emit_block pending pc =
let npc = int_of_pos pc in
if emitted.(npc)
then emit_restart pending
else begin
enum := pc :: !enum;
emitted.(npc) <- true;
match PTree.get pc f.fn_code with
| None -> assert false
| Some i ->
match i with
| Lnop s -> emit_block pending s
| Lop (op, args, res, s) -> emit_block pending s
| Lload (chunk, addr, args, dst, s) -> emit_block pending s
| Lstore (chunk, addr, args, src, s) -> emit_block pending s
| Lcall (sig0, ros, args, res, s) -> emit_block pending s
| Ltailcall (sig0, ros, args) -> emit_restart pending
| Lalloc (arg, res, s) -> emit_block pending s
| Lcond (cond, args, ifso, ifnot) ->
emit_restart (IntSet.add (int_of_pos ifso)
(IntSet.add (int_of_pos ifnot) pending))
| Lreturn optarg -> emit_restart pending
end
and emit_restart pending =
if not (IntSet.is_empty pending) then begin
let npc = IntSet.max_elt pending in
emit_block (IntSet.remove npc pending) (pos_of_int npc)
end in
emit_block IntSet.empty f.fn_entrypoint;
CList.rev !enum
|
