-
Notifications
You must be signed in to change notification settings - Fork 0
/
preproc.ml
85 lines (67 loc) · 2.97 KB
/
preproc.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
open Cil
module P = Printf
module L = List
module CM = Common
class mainQVisitor = object(self)
inherit nopCilVisitor
method private create_rb_rc (f:fundec) : stmt =
let x = CM.exp_of_vi (makeVarinfo false "x" intType) in
let y = CM.exp_of_vi (makeVarinfo false "y" intType) in
let z = CM.exp_of_vi (makeVarinfo false "z" intType) in
let tmp3 = makeLocalVar f "rb" intType in
let tmp4 = makeLocalVar f "rc" intType in
let rb = CM.mkCall ~ftype:intType ~av:(Some (var tmp3)) "buggyQ" [x; y; z] in
let rc = CM.mkCall ~ftype:intType ~av:(Some (var tmp4)) "correctQ" [x; y; z] in
mkStmt (Instr [rb; rc])
method private create_if_block (f:fundec) : stmt =
let tmp3 = makeVarinfo false "rb" intType in
let tmp4 = makeVarinfo false "rc" intType in
let pc: instr = CM.mkCall "$pathCondition" [] in
let true_block: block = mkBlock [mkStmt (Instr [pc])] in
let pcBlock: stmtkind = If (BinOp (Ne, CM.exp_of_vi tmp3, CM.exp_of_vi tmp4, intType), true_block, mkBlock [], !currentLoc) in
mkStmt pcBlock
method vfunc (f: fundec) =
(* let return = CM.mkCall "return" [0] in *)
let action (f: fundec) : fundec =
if f.svar.vname = "mainQ" then( f.slocals <- [];
f.sbody.bstmts <- [self#create_rb_rc f; self#create_if_block f]
);
f in
ChangeDoChildrenPost(f, action)
(* method vfunc (fd: fundec) =
let action (fd: fundec) : fundec =
if fd.svar.vname = "mainQ" then ( (*make this more robust: mainQ should be input*)
let pcCall : instr = CM.mkCall "$pathCondition" [] in
let pcStmt : stmt = mkStmt (Instr[pcCall]) in
let continue : stmt = mkStmt (Continue !currentLoc) in
let insert_stmt (s:stmt) =
match s.skind with
|If(_,b1,b2,_) -> (b1.bstmts <- [continue]; b2.bstmts <- [pcStmt])
|_ -> ()
in L.hd (L.map insert_stmt fd.sbody.bstmts)
(* fd.sbody.bstmts <- fd.sbody.bstmts @ [continue] *)
);
fd in
ChangeDoChildrenPost(fd, action) *)
end
let () = begin
initCIL();
Cil.lineDirectiveStyle := None;
(*Get input from cmd line*)
let src = Sys.argv.(1) in
let preproc = (String.sub src 0 (String.index src '.')) ^ ".preproc.c" in (*save here*)
(*Parse the source file*)
let ast = Frontc.parse src () in
let mainFd:fundec = CM.findFun ast "main" in
let x : exp = CM.exp_of_vi (makeVarinfo false "x" intType) in
let y : exp = CM.exp_of_vi (makeVarinfo false "y" intType) in
let z : exp = CM.exp_of_vi (makeVarinfo false "z" intType) in
let mainQCall : instr = CM.mkCall "mainQ" [x; y; z] in (*make this more robust: mainQ should be input*)
mainFd.sbody.bstmts <- [mkStmt (Instr [mainQCall])];
mainFd.slocals <- [];
visitCilFileSameGlobals (new mainQVisitor) ast;
ast.globals <- (GText "$input int x, y, z;") :: ast.globals;
ast.globals <- (GText "#include <stdio.h>") :: ast.globals;
ast.globals <- (GText "#include <civlc.cvh>") :: ast.globals;
CM.writeSrc preproc ast;
end