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
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(* Test interpretation as a single cycle of relaxations *)
module Make(A:AutoArch.S) = struct
module R = A.R
module L = A.L
type t = R.Set.t
type outcome = L.outcome
type relax = R.relax
type relax_set = R.Set.t
type count = int R.Map.t
let pp = R.pp_set
let interpret _ o = R.Set.of_list (o.L.relaxs @ o.L.safes)
let intest rs = rs
let expand_cumul i = R.expand_cumul i
let get_relaxed_assuming safe rs k =
match R.Set.as_singleton ( R.Set.diff rs safe) with
| None -> k
| Some r -> r::k
let shows_relax safe r rs =
match R.Set.as_singleton (R.Set.diff rs safe) with
| None -> false
| Some s -> R.compare r s = 0
let simplify_for_safes relaxed testing i =
if R.Set.is_empty (R.Set.inter relaxed i) then
let i = R.Set.inter i testing in
if R.Set.is_empty i then
None
else
Some i
else
None
(* Safe heuristics *)
let safe_by_inter _i = R.Set.empty
let safe_by_cardinal i k = (i,1)::k
(* Relaxation count for false safe heuristic *)
let unexplained safe cy =
if R.Set.subset cy safe then Some cy
else None
let count _name safe cy m =
if R.Set.subset cy safe then begin
R.Set.fold
(fun r m ->
let v = try R.Map.find r m with Not_found -> 0 in
R.Map.add r (v+1) m)
cy m
end else m
end
|
