-
Notifications
You must be signed in to change notification settings - Fork 0
/
Driver.v
140 lines (111 loc) · 4.24 KB
/
Driver.v
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
130
131
132
133
134
135
136
137
138
139
140
Require Import ZArith.
Require Import Coq.Strings.String.
Require Import List. Import ListNotations.
Require Import QuickChick.
Require Import Show.
Require Import Test.
Require Import Rules.
Require Import TestingCommon.
Require Import Generation.
Require Import Shrinking.
Require Import SSNI.
Require Import Reachability.
Require Import SingleStateArb.
Require Import SanityChecks.
(* Testing well-formedness first *)
QuickCheck prop_stamp_generation.
QuickCheck prop_generate_indist.
QuickCheck (prop_fstep_preserves_well_formed default_table).
(* Testing non-interference second (default table) *)
Definition testSSNI t := quickCheck (propSSNI t).
QuickCheck (propSSNI default_table).
(* Testing mutants third *)
Require Import Mutate.
Require Import MutateCheck.
Instance mutateable_table : Mutateable table :=
{|
mutate := mutate_table
|}.
(*
Eval simpl in (nth 24 (mutate_table default_table) default_table).
*)
MutateCheckMany default_table (fun t => [propSSNI t;
prop_fstep_preserves_well_formed t]).
(* The rest of this file is mostly garbage *)
(*
Eval lazy -[labelCount helper] in
nth 26 (mutate_table default_table) default_table.
*)
Definition testMutantX x y :=
let mutant := fun o' =>
(helper x y o' (default_table o')) in
testSSNI mutant.
Definition testMutant7 := testMutantX
OpBCall (≪TRUE, JOIN Lab2 LabPC, Lab1 ≫).
(* CH: most often we catch this one; but sometimes it escapes *)
Definition testMutant9 := testMutantX
OpBRet (≪LE Lab1 (JOIN Lab2 Lab3), Lab2, Lab3 ≫).
(* Problem: we weren't generating _any_ HIGH -> LOW cases;
doing a very bad job at generating stacks!
("Some OpBRet, Failed",484),
("Some OpBRet, HIGH -> HIGH",206),
("Some OpBRet, LOW -> *",224),
("Some OpBRet, Second failed H",28),
("Some OpBRet, Second not low",83),
After expedient fix this finds the bug and looks like this:
("Some OpBRet, Failed",85),
("Some OpBRet, HIGH -> HIGH",23),
("Some OpBRet, LOW -> *",40),
("Some OpBRet, Second failed H",6),
("Some OpBRet, HIGH -> LOW",7), <---- this case was missing
*)
Definition testMutant26 := testMutantX
OpBNZ (≪TRUE, __ , LabPC ≫).
(* This was found, just not often enough (once in 20000-30000 tests)
We weren't generating zeroes often enough (1 in 200)
Changed to 1 in 10 and we're finding this just fine. *)
Definition testMutant29 := testMutantX
OpLoad (≪TRUE, Lab3, JOIN Lab1 Lab2 ≫).
(* CH: this one is at the limit (with 10000 tests sometimes we catch
it and sometimes we don't)*)
Definition testMutant36 := testMutantX
OpAlloc (≪TRUE, Lab2, LabPC ≫).
(* XXX: this and the next mutants break well-formedness;
but we don't test that as a precondition to SSNI
DONE: for each mutant we should also test well-formedness
and if that fails the mutant is also killed *)
Definition testMutantWF x y :=
let mutant := fun o' =>
(helper x y o' (default_table o')) in
quickCheck (prop_fstep_preserves_well_formed mutant).
Definition testMutant36wf := testMutantWF
OpAlloc (≪TRUE, Lab2, LabPC ≫).
(* XXX: this sometimes fails, and otherwise gives stack overflow
during shrinking (probably an infinite loop of some sort) *)
Definition testMutant37 := testMutantX
OpAlloc (≪TRUE, Lab1, LabPC ≫).
Definition testMutant37wf := testMutantWF
OpAlloc (≪TRUE, Lab1, LabPC ≫).
(* XXX: this sometimes fails, and otherwise gives stack overflow
during shrinking (probably an infinite loop of some sort) *)
(* Definition testNI := testMutant37wf. *)
(* QuickCheck testMutants.*)
(* Definition testNI := testMutant9.*)
(* Definition testNI := testSSNI default_table. *)
(* Definition testNI := quickCheck prop_stamp_generation. *)
(* Definition testNI :=
quickCheck (prop_preserves_well_formed default_table). *)
(* Definition testNI := quickCheck prop_generate_indist. *)
(*(forAllShrink (fun _ => "implement me!")
genSingleExecState
(fun _ => nil)
(propWellFormednessPreserved default_table)).*)
(*Definition testNI :=
let l := lab_of_list [Pos.of_nat 1] in
let h := lab_of_list [Pos.of_nat 1; Pos.of_nat 2] in
match alloc 2%Z l bot (Vint Z0 @ bot) (Mem.empty Atom Label) with
| Some (mf, m') =>
map (Mem.get_frame m') (Mem.get_all_blocks h m')
| _ => []
end.
*)