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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* TODO: Proper author information *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
(*
This file implements the [branch_target] oracle that identifies "nop" branches in a RTL function,
and computes their target node with the distance (ie the number of cummulated nops) toward this target.
See [RTLTunneling.v]
*)
open Coqlib
open RTL
open Maps
open Camlcoq
open Tunnelinglibs
let nopcounter = ref 0
module LANG = struct
type code_unit = RTL.instruction
type funct = RTL.coq_function
end
module OPT = struct
let langname = "RTL"
let limit_tunneling = None
let debug_flag = ref false
let final_dump = false
end
module rec T: sig
val get_node: cfg -> positive -> node
val set_branch: cfg -> positive -> node -> unit
val debug: ('a, out_channel, unit) format -> 'a
val string_of_labeli: ('a, node) Hashtbl.t -> 'a -> string
exception BugOnPC of int
val branch_target: RTL.coq_function -> (positive * Z.t) PTree.t
end = Tunnelinglibs.Tunneling(LANG)(OPT)(FUNS)
and FUNS: sig
val build_simplified_cfg: cfg -> node list -> positive -> LANG.code_unit -> node list
val print_code_unit: cfg -> bool -> int * LANG.code_unit -> bool
val fn_code: LANG.funct -> LANG.code_unit PTree.t
val fn_entrypoint: LANG.funct -> positive
val check_code_unit: (positive * integer) PTree.t -> positive -> LANG.code_unit -> unit
end = struct
let build_simplified_cfg c acc pc i =
match i with
| Inop s ->
let ns = T.get_node c s in
T.set_branch c pc ns;
incr nopcounter;
acc
| Icond (_, _, s1, s2, _) ->
c.num_rems <- c.num_rems + 1;
let ns1 = T.get_node c s1 in
let ns2 = T.get_node c s2 in
let npc = T.get_node c pc in
npc.inst <- COND(ns1, ns2);
npc::acc
| _ -> acc
let print_code_unit c println (pc, i) =
match i with
| Inop s -> (if println then T.debug "\n"); T.debug "%d:Inop %d %s\n" pc (P.to_int s) (T.string_of_labeli c.nodes pc); false
| Icond (_, _, s1, s2, _) -> (if println then T.debug "\n"); T.debug "%d:Icond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (T.string_of_labeli c.nodes pc); false
| _ -> T.debug "%d " pc; true
let fn_code f = f.fn_code
let fn_entrypoint f = f.fn_entrypoint
(*************************************************************)
(* Copy-paste of the extracted code of the verifier *)
(* with [raise (BugOnPC (P.to_int pc))] instead of [Error.*] *)
let get td pc =
match PTree.get pc td with
| Some p -> let (t0, d) = p in (t0, d)
| None -> (pc, Z.of_uint 0)
let check_code_unit td pc i =
match PTree.get pc td with
| Some p ->
let (tpc, dpc) = p in
let dpc0 = dpc in begin
match i with
| Inop s ->
let (ts, ds) = get td s in
if peq tpc ts
then if zlt ds dpc0
then ()
else raise (T.BugOnPC (P.to_int pc))
else raise (T.BugOnPC (P.to_int pc))
| Icond (_, _, s1, s2, _) ->
let (ts1, ds1) = get td s1 in
let (ts2, ds2) = get td s2 in
if peq tpc ts1
then if peq tpc ts2
then if zlt ds1 dpc0
then if zlt ds2 dpc0
then ()
else raise (T.BugOnPC (P.to_int pc))
else raise (T.BugOnPC (P.to_int pc))
else raise (T.BugOnPC (P.to_int pc))
else raise (T.BugOnPC (P.to_int pc))
| _ ->
raise (T.BugOnPC (P.to_int pc)) end
| None -> ()
end
let branch_target = T.branch_target
|
