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
|
(* *************************************************************)
(* *)
(* 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 LTL function,
and computes their target node with the distance (ie the number of cummulated nops) toward this target.
See [LTLTunneling.v]
*)
open Coqlib
open LTL
open Maps
open Camlcoq
open Tunnelinglibs
module LANG = struct
type code_unit = LTL.bblock
type funct = LTL.coq_function
end
module OPT = struct
let langname = "LTL"
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 bb =
match bb with
| Lbranch s :: _ ->
let ns = get_node c s in
set_branch c pc ns;
acc
| Lcond (_, _, 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, bb) =
match bb with
| Lbranch s::_ -> (if println then Partial.debug "\n"); Partial.debug "%d:Lbranch %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc); false
| Lcond (_, _, s1, s2, _)::_ -> (if println then Partial.debug "\n"); Partial.debug "%d:Lcond (%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 bb =
match PTree.get pc td with
| Some p ->
let (tpc, dpc) = p in
let dpc0 = dpc in
(match bb with
| [] ->
raise (BugOnPC (P.to_int pc))
| i :: _ ->
(match i with
| Lbranch 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))
| Lcond (_, _, 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))))
| None -> ()
end
module T = Partial.T(FUNS)
let branch_target = T.branch_target
|
