Source file l_wm.ml
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
141
142
143
144
145
146
147
open Cil
open Cil_types
open Ast_const
let aorOption : bool ref = ref false
let rorOption : bool ref = ref false
let corOption : bool ref = ref false
let absOption : bool ref = ref false
class mutationVisitor mk_label = object(self)
inherit Visitor.frama_c_inplace
val mutable exprs = []
val mutable currloc = Cil_datatype.Location.unknown
method private makeLabel cond category =
let le = mk_label ~extra:[category] cond [] currloc in
exprs <- exprs @ [le]
method private mk_op_labels e lop lexp rexp ty wm opt =
if opt = true then
List.iter (fun op ->
let newExp = Exp_builder.mk (BinOp (op, lexp, rexp, ty)) in
let labelExp = Exp_builder.mk (BinOp (Ne, newExp, e, ty)) in
self#makeLabel labelExp wm
) lop;
self#traitExp lexp;
self#traitExp rexp
method private traitExp e =
match e.enode with
| BinOp(LAnd, lexp, rexp, ty) ->
self#mk_op_labels e [LOr] lexp rexp ty "COR" !corOption
| BinOp(LOr, lexp, rexp, ty) ->
self#mk_op_labels e [LAnd] lexp rexp ty "COR" !corOption
| BinOp(Div, lexp, rexp, ty) ->
self#mk_op_labels e [Mult;PlusA;MinusA] lexp rexp ty "AOR" !aorOption
| BinOp(Mult, lexp, rexp, ty) ->
self#mk_op_labels e [Div;PlusA;MinusA] lexp rexp ty "AOR" !aorOption
| BinOp(PlusA, lexp, rexp, ty) ->
self#mk_op_labels e [Mult;Div;MinusA] lexp rexp ty "AOR" !aorOption
| BinOp(MinusA, lexp, rexp, ty) ->
self#mk_op_labels e [Mult;Div;PlusA] lexp rexp ty "AOR" !aorOption
| BinOp(Lt, lexp, rexp, ty) ->
self#mk_op_labels e [Le;Gt;Ge] lexp rexp ty "ROR" !rorOption
| BinOp(Gt, lexp, rexp, ty) ->
self#mk_op_labels e [Lt;Le;Ge] lexp rexp ty "ROR" !rorOption
| BinOp(Le, lexp, rexp, ty) ->
self#mk_op_labels e [Lt;Gt;Ge] lexp rexp ty "ROR" !rorOption
| BinOp(Ge, lexp, rexp, ty) ->
self#mk_op_labels e [Lt;Le;Gt] lexp rexp ty "ROR" !rorOption
| BinOp(Eq, lexp, rexp, ty) ->
self#mk_op_labels e [Ne] lexp rexp ty "ROR" !rorOption
| BinOp(Ne, lexp, rexp, ty) ->
self#mk_op_labels e [Eq] lexp rexp ty "ROR" !rorOption
| BinOp(Shiftlt, lexp, rexp, ty) ->
self#mk_op_labels e [Shiftrt] lexp rexp ty "AOR" !aorOption
| BinOp(Shiftrt, lexp, rexp, ty) ->
self#mk_op_labels e [Shiftlt] lexp rexp ty "AOR" !aorOption
| BinOp(_op, lexp, rexp, _ty) ->
self#traitExp lexp;
self#traitExp rexp
| UnOp(Neg, exp, ty) ->
if !aorOption = true then begin
let labelExp = Exp_builder.mk (BinOp (Ne, exp, e, ty)) in
self#makeLabel labelExp "AOR"
end;
self#traitExp exp
| UnOp(_op, exp, _ty)->
self#traitExp exp
| Lval(_l) ->
if !absOption = true then begin
let zeroExp = Exp_builder.mk (Const (CInt64(Integer.of_int(0),IInt,None))) in
let labelExp = Exp_builder.mk (BinOp (Lt, e, zeroExp, intType)) in
self#makeLabel labelExp "ABS"
end
| _ -> ()
method! vfunc f =
if Annotators.shouldInstrumentFun f.svar then
DoChildren
else
SkipChildren
method! vstmt_aux stmt =
begin match stmt.skind with
| Instr(Set(_l, e, loc)) ->
currloc <- loc;
self#traitExp e
| If(e, _l, _ll, loc) ->
currloc <- loc;
self#traitExp e
| Return(e, loc) ->
begin match e with
| Some exp ->
currloc <- loc;
self#traitExp exp
| _ -> ()
end
| Switch(e, _l,_ll, loc) ->
currloc <- loc;
self#traitExp e
| _ -> ()
end;
let stmtExprsLabels = exprs in
exprs <- [];
DoChildrenPost (fun stmt ->
match stmtExprsLabels with
| [] -> stmt
| _ ->
stmt.skind <- Block (Cil.mkBlock (stmtExprsLabels @ [Stmt_builder.mk stmt.skind]));
stmt
)
end
module WM = Annotators.RegisterWithExtraTags (struct
let name = "WM"
let help = "Weak Mutation"
let apply mk_label ast =
Visitor.visitFramacFileSameGlobals
(new mutationVisitor mk_label :> Visitor.frama_c_inplace)
ast
end)