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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

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 = Fileloc.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 wm opt =
    if opt = true then
      List.iter (fun op ->
          let newExp = Exp_builder.binop op lexp rexp in
          let labelExp = Exp_builder.binop Ne newExp e 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 "COR" !corOption
    | BinOp(LOr, lexp, rexp, _ty) ->
      self#mk_op_labels e [LAnd] lexp rexp "COR" !corOption
    | BinOp(Div, lexp, rexp, _ty) ->
      self#mk_op_labels e [Mult;PlusA;MinusA] lexp rexp "AOR" !aorOption
    | BinOp(Mult, lexp, rexp, _ty) ->
      self#mk_op_labels e [Div;PlusA;MinusA] lexp rexp "AOR" !aorOption
    | BinOp(PlusA, lexp, rexp, _ty) ->
      self#mk_op_labels e [Mult;Div;MinusA] lexp rexp "AOR" !aorOption
    | BinOp(MinusA, lexp, rexp, _ty) ->
      self#mk_op_labels e [Mult;Div;PlusA] lexp rexp "AOR" !aorOption
    | BinOp(Lt, lexp, rexp, _ty) ->
      self#mk_op_labels e [Le;Gt;Ge] lexp rexp "ROR" !rorOption
    | BinOp(Gt, lexp, rexp, _ty) ->
      self#mk_op_labels e [Lt;Le;Ge] lexp rexp "ROR" !rorOption
    | BinOp(Le, lexp, rexp, _ty) ->
      self#mk_op_labels e [Lt;Gt;Ge] lexp rexp "ROR" !rorOption
    | BinOp(Ge, lexp, rexp, _ty) ->
      self#mk_op_labels e [Lt;Le;Gt] lexp rexp "ROR" !rorOption
    | BinOp(Eq, lexp, rexp, _ty) ->
      self#mk_op_labels e [Ne] lexp rexp "ROR" !rorOption
    | BinOp(Ne, lexp, rexp, _ty) ->
      self#mk_op_labels e [Eq] lexp rexp "ROR" !rorOption
    | BinOp(Shiftlt, lexp, rexp, _ty) ->
      self#mk_op_labels e [Shiftrt] lexp rexp "AOR" !aorOption
    | BinOp(Shiftrt, lexp, rexp, _ty) ->
      self#mk_op_labels e [Shiftlt] lexp rexp "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.binop Ne exp e 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.zero () in
        let labelExp = Exp_builder.binop Lt e zeroExp 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)