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
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* Pierre Goutagny ENS-Lyon, VERIMAG *)
(* *)
(* 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
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 Partial = Tunnelinglibs.Tunneling(LANG)(OPT)
module FUNS = struct
let build_simplified_cfg c acc pc i =
match i with
| Inop s ->
let ns = get_node c s in
set_branch c pc ns;
incr nopcounter;
acc
| Icond (_, _, s1, s2, _) ->
c.num_rems <- c.num_rems + 1;
let ns1 = get_node c s1 in
let ns2 = get_node c s2 in
let npc = 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 Partial.debug "\n");
Partial.debug "%d:Inop %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc);
false
| Icond (_, _, s1, s2, _) -> (if println then Partial.debug "\n");
Partial.debug "%d:Icond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (string_of_labeli c.nodes pc);
false
| _ -> Partial.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 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 (BugOnPC (P.to_int pc))
else raise (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 (BugOnPC (P.to_int pc))
else raise (BugOnPC (P.to_int pc))
else raise (BugOnPC (P.to_int pc))
else raise (BugOnPC (P.to_int pc))
| _ ->
raise (BugOnPC (P.to_int pc)) end
| None -> ()
end
module T = Partial.T(FUNS)
let branch_target = T.branch_target
|