Commit cc6fafbb authored by Mickaël Delahaye's avatar Mickaël Delahaye
Browse files

Modularize annotators, add decision and function coverage

parent 64728ec0
......@@ -6,7 +6,7 @@ PLUGIN_NAME = Genlabels
PLUGIN_TESTS_DIRS:=bubblesort
PLUGIN_CMO = options config utils instru register
PLUGIN_CMO = options config utils annotators instru decision function register
include $(FRAMAC_SHARE)/Makefile.dynamic
open Cil_types
type annotation = int * string * exp * location
type annotator = {
name:string;
descr: string;
compute: int ref -> annotation list ref -> Cil_types.file -> unit
}
module type ANNOTATOR = sig
val name : string
val descr : string
val compute : (Cil_types.exp -> Cil_types.location -> Cil_types.stmt) -> Cil_types.file -> unit
end
module type ANNOTATOR_WITH_EXTRA_TAGS = sig
val name : string
val descr : string
val compute : (extra:string list -> Cil_types.exp -> Cil_types.location -> Cil_types.stmt) -> Cil_types.file -> unit
end
module type S = sig
val self : annotator
end
let annotators = Hashtbl.create 10
let nextId = ref 1
let annotate_with ?(acc=[]) ?(nextId=nextId) annotator ast =
let acc = ref acc in
Options.feedback "apply annotations for %s@." annotator.name;
annotator.compute nextId acc ast;
!acc
let annotate names ast =
let f acc name =
try
annotate_with ~acc (Hashtbl.find annotators name) ast
with Not_found ->
Options.warning "unknown annotators `%s`" name;
acc
in
List.fold_left f [] names
let mk_compute compute name nextId acc ast =
let label_maker cond loc =
let tag = name in
let id = !nextId in
incr nextId;
acc := (id,tag,cond,loc) :: !acc;
let tagExp = Utils.mk_exp (Const (CStr tag)) in
let idExp = Utils.mk_exp (Const (CInt64 (Integer.of_int id, IInt, None))) in
Utils.mk_call "pc_label" [ cond; idExp; tagExp ]
in
compute label_maker ast
let mk_compute_extras compute name nextId acc ast =
let label_maker ~extra cond loc =
let tag = String.concat " " (name::extra) in
let id = !nextId in
incr nextId;
acc := (id,tag,cond,loc) :: !acc;
let tagExp = Utils.mk_exp (Const (CStr tag)) in
let idExp = Utils.mk_exp (Const (CInt64 (Integer.of_int id, IInt, None))) in
Utils.mk_call "pc_label" [ cond; idExp; tagExp ]
in
compute label_maker ast
let register_annotator ann =
Hashtbl.replace annotators ann.name ann;
Options.Annotators.set_possible_values (Hashtbl.fold (fun k _v acc -> k :: acc) annotators [])
module Register (A : ANNOTATOR) = struct
let self = { name = A.name; descr = A.descr; compute = mk_compute A.compute A.name }
let () = register_annotator self
end
module RegisterWithExtraTags (A : ANNOTATOR_WITH_EXTRA_TAGS) = struct
let self = { name = A.name; descr = A.descr; compute = mk_compute_extras A.compute A.name }
let () = register_annotator self
end
let shouldInstrument fun_varinfo =
let names = Options.FunctionNames.get () in
(* TODO filter builtin functions *)
if Datatype.String.Set.is_empty names then
true
else
Datatype.String.Set.mem fun_varinfo.vname names
type annotation = int * string * Cil_types.exp * Cil_types.location
type annotator
(** Module type of annotators *)
module type ANNOTATOR = sig
val name : string
val descr : string
(** Insert IN PLACE the annotation on the given AST.
*
* In addition of the AST, it also takes a function as parameter.
* This function is provided by Annotators, it makes a label statement
* from a boolean condition and an "origin" location (e.g. the
* if-then-else condition's location in the case of a MCC label).
*)
val compute : (Cil_types.exp -> Cil_types.location -> Cil_types.stmt) -> Cil_types.file -> unit
end
module type ANNOTATOR_WITH_EXTRA_TAGS = sig
val name : string
val descr : string
val compute : (extra:string list -> Cil_types.exp -> Cil_types.location -> Cil_types.stmt) -> Cil_types.file -> unit
end
module type S = sig
val self : annotator
end
(**
* Register an annotator
*)
module Register (A : ANNOTATOR) : S
(**
* Register an annotator that provides extra tags (for instance, mutator tags)
* in addition of the annotator name
*)
module RegisterWithExtraTags (A : ANNOTATOR_WITH_EXTRA_TAGS) : S
val annotate_with : ?acc:annotation list -> ?nextId:int ref -> annotator -> Cil_types.file -> annotation list
val annotate : string list -> Cil_types.file -> annotation list
val shouldInstrument : Cil_types.varinfo -> bool
open Cil_types
open Annotators
include Register (struct
let name = "D"
let descr = "Decision coverage"
(**
* Add one label of each branch of a If.
* Operates IN PLACE (it does returns the parameter though)
*)
let add_decision_labels mk_label stmt =
let mk_label_true loc = mk_label (Cil.one (Lexing.dummy_pos, Lexing.dummy_pos)) loc in
match stmt.skind with
| If (_, thenBlock, elseBlock, loc) ->
thenBlock.bstmts <- mk_label_true loc :: thenBlock.bstmts;
elseBlock.bstmts <- mk_label_true loc :: elseBlock.bstmts;
stmt
| _ -> stmt
(** A visitor that calls add_decision_labels AFTER visiting each If *)
let visitor mk_label = object
inherit Visitor.frama_c_inplace
method! vfunc dec =
if shouldInstrument dec.svar then
Cil.DoChildren
else
Cil.SkipChildren
method! vstmt_aux stmt =
match stmt.skind with
| If _ ->
Cil.ChangeDoChildrenPost (stmt, add_decision_labels mk_label)
| _ ->
Cil.DoChildren
end
let compute mk_label ast =
Visitor.visitFramacFile (visitor mk_label) ast
end)
open Cil_types
open Annotators
include Register (struct
let name = "F"
let descr = "Function coverage"
(** A visitor that adds a label at the start of each function's body *)
let visitor mk_label = object
inherit Visitor.frama_c_inplace
method! vfunc dec =
if shouldInstrument dec.svar then begin
let label = mk_label (Cil.one Cil_datatype.Location.unknown) dec.svar.vdecl in
dec.sbody.bstmts <- label :: dec.sbody.bstmts;
end;
Cil.SkipChildren
end
let compute f ast =
Visitor.visitFramacFileSameGlobals (visitor f) ast
end)
......@@ -2,19 +2,12 @@ open Cil
open Cil_types
open Lexing
let nextLabelId : int ref = ref 1
let multiCondOption : bool ref = ref false
let aorOption : bool ref = ref false
let rorOption : bool ref = ref false
let corOption : bool ref = ref false
let absOption : bool ref = ref false
let partitionOption : bool ref = ref false
let simpleOption : bool ref = ref false
(* (file,line, id, cond, type) *)
let labelsList : (string*int*int*exp*string) list ref = ref []
(*
(* val print_project: Project.t -> string *)
let print_project prj filename =
let out = open_out filename in
......@@ -24,14 +17,30 @@ let print_project prj filename =
let _ = Format.set_formatter_out_channel Pervasives.stdout in
filename
let shouldInstrument fun_varinfo =
let names = Options.FunctionNames.get () in
(* TODO filter builtin functions *)
if Datatype.String.Set.is_empty names then
true
else
Datatype.String.Set.mem fun_varinfo.vname names
let prepareLabelsBuffer labelsList myBuffer =
Buffer.add_string myBuffer "<labels>\n";
let rec printLabels labels =
match labels with
| (fileName,lineNb, id, cond, ltype)::rest ->
let myBuf = Buffer.create 128 in
let fmt = Format.formatter_of_buffer myBuf in
Printer.pp_exp fmt cond;
Format.pp_print_flush fmt ();
Buffer.add_string myBuffer ("<label>\n");
Buffer.add_string myBuffer ("<id>" ^ (string_of_int id) ^ "</id>\n");
Buffer.add_string myBuffer ("<cond>" ^ (Buffer.contents myBuf) ^ "</cond>\n");
Buffer.add_string myBuffer ("<file>" ^ fileName ^ "</file>\n");
Buffer.add_string myBuffer ("<line>" ^ (string_of_int lineNb) ^ "</line>\n");
Buffer.add_string myBuffer ("<type>" ^ ltype ^ "</type>\n");
Buffer.add_string myBuffer ("</label>\n");
printLabels rest
| [] -> ()
in
printLabels (List.rev !labelsList);
Buffer.add_string myBuffer "</labels>\n"
*)
(*
let makeLabel cond loc ltype =
let labelTypeExp = Utils.mk_exp (Const(CStr(ltype))) in
let labelIdExp = Utils.mk_exp (Const(CInt64(Integer.of_int(!nextLabelId),IInt,None))) in
......@@ -40,59 +49,64 @@ let makeLabel cond loc ltype =
labelsList := (fileName,lineNumber,!nextLabelId, cond, ltype)::!labelsList;
nextLabelId := !nextLabelId+1;
Utils.mk_call "pc_label" [ cond; labelIdExp; labelTypeExp ]
*)
let rec genLabelPerExp exp loc =
module CC = Annotators.Register (struct
let name = "CC"
let descr = "Condition Coverage"
let rec genLabelPerExp mk_label exp loc =
match exp.enode with
| BinOp(LAnd, e1, e2, _) ->
List.append (genLabelPerExp e1 loc) (genLabelPerExp e2 loc)
List.append (genLabelPerExp mk_label e1 loc) (genLabelPerExp mk_label e2 loc)
| BinOp(LOr, e1, e2, _) ->
List.append (genLabelPerExp e1 loc) (genLabelPerExp e2 loc)
List.append (genLabelPerExp mk_label e1 loc) (genLabelPerExp mk_label e2 loc)
| BinOp(Lt, e1, e2, t) ->
let nonExp = Utils.mk_exp(BinOp(Ge, e1, e2, t)) in
[makeLabel exp loc "CC"; makeLabel nonExp loc "CC"]
[mk_label exp loc; mk_label nonExp loc]
| BinOp(Gt, e1, e2, t) ->
let nonExp = Utils.mk_exp(BinOp(Le, e1, e2, t)) in
[makeLabel exp loc "CC"; makeLabel nonExp loc "CC"]
[mk_label exp loc; mk_label nonExp loc]
| BinOp(Le, e1, e2, t) ->
let nonExp = Utils.mk_exp(BinOp(Gt, e1, e2, t)) in
[makeLabel exp loc "CC"; makeLabel nonExp loc "CC"]
[mk_label exp loc; mk_label nonExp loc]
| BinOp(Ge, e1, e2, t) ->
let nonExp = Utils.mk_exp(BinOp(Lt, e1, e2, t)) in
[makeLabel exp loc "CC"; makeLabel nonExp loc "CC"]
[mk_label exp loc; mk_label nonExp loc]
| BinOp(Eq, e1, e2, t) ->
let nonExp = Utils.mk_exp(BinOp(Ne, e1, e2, t)) in
[makeLabel exp loc "CC"; makeLabel nonExp loc "CC"]
[mk_label exp loc; mk_label nonExp loc]
| BinOp(Ne, e1, e2, t) ->
let nonExp = Utils.mk_exp(BinOp(Eq, e1, e2, t)) in
[makeLabel exp loc "CC"; makeLabel nonExp loc "CC"]
[mk_label exp loc; mk_label nonExp loc]
| BinOp(_, _e1, _e2, _) ->
let nonExp = Utils.mk_exp(UnOp(LNot, exp, intType)) in
[makeLabel exp loc "CC"; makeLabel nonExp loc "CC"]
[mk_label exp loc; mk_label nonExp loc]
| Lval(_lv) ->
let nonExp = Utils.mk_exp(UnOp(LNot, exp, intType)) in
[makeLabel exp loc "CC"; makeLabel nonExp loc "CC"]
[mk_label exp loc; mk_label nonExp loc]
| UnOp(LNot, e1, _) ->
genLabelPerExp e1 loc
genLabelPerExp mk_label e1 loc
| _ -> []
class genLabelsVisitor = object(_self)
class genLabelsVisitor mk_label = object(_self)
inherit Visitor.frama_c_inplace
method! vfunc dec =
if shouldInstrument dec.svar then DoChildren else SkipChildren
if Annotators.shouldInstrument dec.svar then DoChildren else SkipChildren
method! vstmt_aux stmt =
let genLabels s =
......@@ -100,7 +114,7 @@ class genLabelsVisitor = object(_self)
| If(e, _, _, _) ->
let loc = Utils.get_stmt_loc s in
let finalList = List.append (genLabelPerExp e loc) ([s]) in
let finalList = List.append (genLabelPerExp mk_label e loc) ([s]) in
let b2 = mkBlock finalList in
let i = mkStmt (Block(b2)) in
i
......@@ -113,6 +127,13 @@ class genLabelsVisitor = object(_self)
| _ -> DoChildren
end
let compute mk_label ast =
Visitor.visitFramacFileSameGlobals
(new genLabelsVisitor mk_label :> Visitor.frama_c_inplace)
ast
end)
(* ******************************************************* *)
(* ******************************************************* *)
(* pow(2,10) = 2^10 *)
......@@ -138,31 +159,31 @@ let rec getConditionsNumber exp =
| _ -> 0
end
module MCC = Annotators.Register (struct
let name = "MCC"
let descr = "Multiple Condition Coverage"
let generateStatementFromConditionsList conds loc =
let rec mergeConds condsList =
match condsList with
let generateStatementFromConditionsList mk_label conds loc =
let rec mergeConds condsList =
match condsList with
| [] -> assert false
| a::[] -> a
| a::b::tail->
let newExp = Utils.mk_exp(BinOp(LAnd, a, b, intType)) in
mergeConds (List.append [newExp] tail)
in
match conds with
in
match conds with
| [] ->
let stmt = makeLabel (Cil.one Cil_datatype.Location.unknown) loc "MCC" in
let stmt = mk_label (Cil.one Cil_datatype.Location.unknown) loc in
stmt
| _ ->
let newCond = mergeConds conds in
let lineNumber = (fst loc).pos_lnum in
let fileName = (fst loc).pos_fname in
labelsList := (fileName,lineNumber,!nextLabelId, newCond, "MCC")::!labelsList;
let stmt = makeLabel newCond loc "MCC" in
stmt
let stmt = mk_label newCond loc in
stmt
let getNegativeCond exp =
match exp.enode with
let getNegativeCond exp =
match exp.enode with
| BinOp(Lt, e1, e2, t) ->
Utils.mk_exp(BinOp(Ge, e1, e2, t))
......@@ -188,10 +209,10 @@ let getNegativeCond exp =
| _ -> Utils.mk_exp(UnOp(LNot, exp, Cil.intType))
let rec genMultiLabel allConds conditionsNb currentNb newConds cumul loc =
match allConds with
let rec genMultiLabel mk_label allConds conditionsNb currentNb newConds cumul loc =
match allConds with
| [] ->
generateStatementFromConditionsList newConds loc
generateStatementFromConditionsList mk_label newConds loc
| a :: tail ->
(* let ex = pow(2, conditionsNb) in *)
......@@ -201,93 +222,75 @@ let rec genMultiLabel allConds conditionsNb currentNb newConds cumul loc =
let curCond = a in
let newCumul = cumul + ( pow(2, conditionsNb) ) in
let newNewConds = List.append newConds [curCond] in
genMultiLabel tail (conditionsNb-1) currentNb newNewConds newCumul loc
genMultiLabel mk_label tail (conditionsNb-1) currentNb newNewConds newCumul loc
end
else
begin
let curCond = getNegativeCond a in
let newCumul = cumul in
let newNewConds = List.append newConds [curCond] in
genMultiLabel tail (conditionsNb-1) currentNb newNewConds newCumul loc
genMultiLabel mk_label tail (conditionsNb-1) currentNb newNewConds newCumul loc
end
let rec genMultiLabels allConds conditionsNb currentNb labelStmts loc =
let casesNb = pow(2, conditionsNb) in
let rec genMultiLabels mk_label allConds conditionsNb currentNb labelStmts loc =
let casesNb = pow(2, conditionsNb) in
if currentNb = casesNb then
begin
labelStmts
end
else
begin
let curStmt = genMultiLabel allConds (conditionsNb-1) currentNb [] 0 loc in
let curStmt = genMultiLabel mk_label allConds (conditionsNb-1) currentNb [] 0 loc in
let newStmts = List.append labelStmts [curStmt] in
genMultiLabels allConds conditionsNb (currentNb+1) newStmts loc
genMultiLabels mk_label allConds conditionsNb (currentNb+1) newStmts loc
end
let rec getUnitaryConditionsInExp exp =
match exp.enode with
| BinOp(LAnd, e1, e2, _) ->
List.append (getUnitaryConditionsInExp e1) (getUnitaryConditionsInExp e2)
| BinOp(LOr, e1, e2, _) ->
List.append (getUnitaryConditionsInExp e1) (getUnitaryConditionsInExp e2)
| BinOp(_, _e1, _e2, _) -> [exp]
let rec getUnitaryConditionsInExp exp =
match exp.enode with
| BinOp(LAnd, e1, e2, _) ->
List.append (getUnitaryConditionsInExp e1) (getUnitaryConditionsInExp e2)
| BinOp(LOr, e1, e2, _) ->
List.append (getUnitaryConditionsInExp e1) (getUnitaryConditionsInExp e2)
| BinOp(_, _e1, _e2, _) -> [exp]
| Lval(_lv) -> [exp]
| Lval(_lv) -> [exp]
| UnOp(LNot, e1, _) -> getUnitaryConditionsInExp e1
| UnOp(LNot, e1, _) -> getUnitaryConditionsInExp e1
| _ -> []
| _ -> []
let prepareLabelsBuffer labelsList myBuffer =
Buffer.add_string myBuffer "<labels>\n";
class genMultiLabelsVisitor mk_label = object(_self)
inherit Visitor.frama_c_inplace
let rec printLabels labels =
match labels with
| (fileName,lineNb, id, cond, ltype)::rest ->
let myBuf = Buffer.create 128 in
let fmt = Format.formatter_of_buffer myBuf in
Printer.pp_exp fmt cond;
Format.pp_print_flush fmt ();
Buffer.add_string myBuffer ("<label>\n");
Buffer.add_string myBuffer ("<id>" ^ (string_of_int id) ^ "</id>\n");
Buffer.add_string myBuffer ("<cond>" ^ (Buffer.contents myBuf) ^ "</cond>\n");
Buffer.add_string myBuffer ("<file>" ^ fileName ^ "</file>\n");
Buffer.add_string myBuffer ("<line>" ^ (string_of_int lineNb) ^ "</line>\n");
Buffer.add_string myBuffer ("<type>" ^ ltype ^ "</type>\n");
Buffer.add_string myBuffer ("</label>\n");
printLabels rest
| [] -> ()
in
printLabels (List.rev !labelsList);
Buffer.add_string myBuffer "</labels>\n"
method! vfunc dec =
if Annotators.shouldInstrument dec.svar then DoChildren else SkipChildren
(*****************************************)
class genMultiLabelsVisitor = object(_self)
inherit Visitor.frama_c_inplace
method! vfunc dec =
if shouldInstrument dec.svar then DoChildren else SkipChildren
method! vstmt_aux stmt =
let genLabels s =
match s.skind with
| If(e, _, _, _) ->
let loc = Utils.get_stmt_loc s in
let nbCond = getConditionsNumber e in
let allConds = getUnitaryConditionsInExp e in
let finalList = List.append (genMultiLabels mk_label allConds nbCond 0 [] loc) ([s]) in
let b2 = mkBlock finalList in
let i = mkStmt (Block(b2)) in
i
| _ -> s
in
match stmt.skind with
| If _ ->
ChangeDoChildrenPost (stmt, genLabels)
| _ -> DoChildren
end
method! vstmt_aux stmt =
let genLabels s =
match s.skind with
| If(e, _, _, _) ->
let loc = Utils.get_stmt_loc s in
let nbCond = getConditionsNumber e in
let allConds = getUnitaryConditionsInExp e in
let finalList = List.append (genMultiLabels allConds nbCond 0 [] loc) ([s]) in
let b2 = mkBlock finalList in
let i = mkStmt (Block(b2)) in
i
| _ -> s
in
match stmt.skind with
| If _ ->
ChangeDoChildrenPost (stmt, genLabels)
| _ -> DoChildren
end
let compute mk_label ast =
Visitor.visitFramacFileSameGlobals
(new genMultiLabelsVisitor mk_label :> Visitor.frama_c_inplace)
ast
end)
(*****************************************)
......@@ -300,55 +303,77 @@ let getLocFromFunction f =
| a::_ -> Cil_datatype.Stmt.loc a
| [] -> Cil_datatype.Location.unknown
module Partition = Annotators.Register (struct
let name = "IDP"
let descr = "Input Domain Partition"
let makeLabelsFromInput myParam loc =
match myParam.vtype with
let makeLabelsFromInput mk_label myParam loc =
match myParam.vtype with
| TInt _
| TFloat _ ->
let formalExp = new_exp loc (Lval (var myParam)) in
let formalExp = Utils.mk_exp (Lval (var myParam)) in
let zeroExp = Utils.mk_exp (Const(CInt64(Integer.of_int(0),IInt,None))) in
let exp1 = Utils.mk_exp(BinOp(Lt, formalExp, zeroExp, intType)) in
let exp2 = Utils.mk_exp(BinOp(Gt, formalExp, zeroExp, intType)) in
let exp3 = Utils.mk_exp(BinOp(Eq, formalExp, zeroExp, intType)) in
let stmt1 = makeLabel exp1 loc "PARTITION" in
let stmt2 = makeLabel exp2 loc "PARTITION" in
let stmt3 = makeLabel exp3 loc "PARTITION" in
let exp1 = Utils.mk_exp (BinOp(Lt, formalExp, zeroExp, intType)) in
let exp2 = Utils.mk_exp (BinOp(Gt, formalExp, zeroExp, intType)) in
let exp3 = Utils.mk_exp (BinOp(Eq, formalExp, zeroExp, intType)) in
let stmt1 = mk_label exp1 loc in
let stmt2 = mk_label exp2 loc in
let stmt3 = mk_label exp3 loc in
[stmt1; stmt2; stmt3]
| TPtr _ ->
let formalExp = new_exp loc (Lval (var myParam)) in
| TPtr _ ->
let formalExp = Utils.mk_exp (Lval (var myParam)) in
let zeroExp = Utils.mk_exp (Const(CInt64(Integer.of_int(0),IInt,None))) in
let exp1 = Utils.mk_exp(BinOp(Eq, formalExp, zeroExp, intType)) in
let exp2 = Utils.mk_exp(BinOp(Ne, formalExp, zeroExp, intType)) in
let stmt1 = makeLabel exp1 loc "PARTITION" in
let stmt2 = makeLabel exp2 loc "PARTITION" in
let stmt1 = mk_label exp1 loc in
let stmt2 = mk_label exp2 loc in