1 files changed, 337 insertions, 0 deletions
diff --git a/cil/src/ext/sfi.ml b/cil/src/ext/sfi.ml
new file mode 100755
index 0000000..9886526
--- /dev/null
+++ b/cil/src/ext/sfi.ml
@@ -0,0 +1,337 @@
+(*
+ *
+ * Copyright (c) 2005, 
+ *  George C. Necula    <necula@cs.berkeley.edu>
+ * All rights reserved.
+ * 
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * 3. The names of the contributors may not be used to endorse or promote
+ * products derived from this software without specific prior written
+ * permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+ * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ *)
+
+(** This is a module that inserts runtime checks for memory reads/writes and 
+ * allocations *)
+
+open Pretty
+open Cil
+module E = Errormsg
+module H = Hashtbl
+
+let doSfi = ref false
+let doSfiReads = ref false
+let doSfiWrites = ref true
+
+(* A number of functions to be skipped *)
+let skipFunctions : (string, unit) H.t = H.create 13
+let mustSfiFunction (f: fundec) : bool = 
+  not (H.mem skipFunctions f.svar.vname)
+
+(** Some functions are known to be allocators *)
+type dataLocation = 
+    InResult  (* Interesting data is in the return value *)
+  | InArg of int (* in the nth argument. Starts from 1. *)
+  | InArgTimesArg of int * int (* (for size) data is the product of two 
+                                * arguments *)
+  | PointedToByArg of int (* pointed to by nth argument *)
+
+(** Compute the data based on the location and the actual argument list *)
+let extractData (dl: dataLocation) (args: exp list) (res: lval option) : exp = 
+  let getArg (n: int) = 
+    try List.nth args (n - 1) (* Args are based at 1 *)
+    with _ -> E.s (E.bug "Cannot extract argument %d at %a" 
+                     n d_loc !currentLoc)
+  in
+  match dl with 
+    InResult -> begin
+      match res with 
+        None -> 
+          E.s (E.bug "Cannot extract InResult data (at %a)" d_loc !currentLoc)
+      | Some r -> Lval r
+    end
+  | InArg n -> getArg n
+  | InArgTimesArg (n1, n2) -> 
+      let a1 = getArg n1 in
+      let a2 = getArg n2 in 
+      BinOp(Mult, mkCast ~e:a1 ~newt:longType, 
+            mkCast ~e:a2 ~newt:longType, longType)
+  | PointedToByArg n -> 
+      let a = getArg n in 
+      Lval (mkMem a NoOffset)
+      
+
+
+(* for each allocator, where is the length and where is the result *)
+let allocators: (string, (dataLocation * dataLocation)) H.t = H.create 13
+let _ = 
+  H.add allocators "malloc" (InArg 1, InResult);
+  H.add allocators "calloc" (InArgTimesArg (1, 2), InResult);
+  H.add allocators "realloc" (InArg 2, InResult)
+
+(* for each deallocator, where is the data being deallocated *)
+let deallocators: (string, dataLocation) H.t = H.create 13
+let _= 
+  H.add deallocators "free" (InArg 1);
+  H.add deallocators "realloc" (InArg 1)
+  
+(* Returns true if the given lvalue offset ends in a bitfield access. *) 
+let rec is_bitfield lo = match lo with
+  | NoOffset -> false
+  | Field(fi,NoOffset) -> not (fi.fbitfield = None)
+  | Field(_,lo) -> is_bitfield lo
+  | Index(_,lo) -> is_bitfield lo 
+
+(* Return an expression that evaluates to the address of the given lvalue.
+ * For most lvalues, this is merely AddrOf(lv). However, for bitfields
+ * we do some offset gymnastics. 
+ *)
+let addr_of_lv (lv: lval) = 
+  let lh, lo = lv in 
+  if is_bitfield lo then begin
+    (* we figure out what the address would be without the final bitfield
+     * access, and then we add in the offset of the bitfield from the
+     * beginning of its enclosing comp *) 
+    let rec split_offset_and_bitfield lo = match lo with 
+      | NoOffset -> failwith "logwrites: impossible" 
+      | Field(fi,NoOffset) -> (NoOffset,fi)
+      | Field(e,lo) ->  let a,b = split_offset_and_bitfield lo in 
+                        ((Field(e,a)),b)
+      | Index(e,lo) ->  let a,b = split_offset_and_bitfield lo in
+                        ((Index(e,a)),b)
+    in 
+    let new_lv_offset, bf = split_offset_and_bitfield lo in
+    let new_lv = (lh, new_lv_offset) in 
+    let enclosing_type = TComp(bf.fcomp, []) in 
+    let bits_offset, bits_width = 
+      bitsOffset enclosing_type (Field(bf,NoOffset)) in
+    let bytes_offset = bits_offset / 8 in
+    let lvPtr = mkCast ~e:(mkAddrOf (new_lv)) ~newt:(charPtrType) in
+    (BinOp(PlusPI, lvPtr, (integer bytes_offset), ulongType))
+  end else 
+    (mkAddrOf (lh,lo)) 
+
+
+let mustLogLval (forwrite: bool) (lv: lval) : bool = 
+  match lv with
+    Var v, off -> (* Inside a variable. We assume the array offsets are fine *)
+      false
+  | Mem e, off -> 
+      if forwrite && not !doSfiWrites then 
+        false
+      else if not forwrite && not !doSfiReads then 
+        false
+
+      (* If this is an lval of function type, we do not log it *) 
+      else if isFunctionType (typeOfLval lv) then 
+        false
+      else 
+        true
+
+(* Create prototypes for the logging functions *)
+let mkProto (name: string) (args: (string * typ * attributes) list) = 
+  let fdec = emptyFunction name in
+  fdec.svar.vtype <- TFun(voidType, 
+                          Some args, false, []);
+  fdec
+  
+
+let logReads = mkProto "logRead" [ ("addr", voidPtrType, []);
+                                   ("what", charPtrType, []);
+                                   ("file", charPtrType, []);
+                                   ("line", intType, []) ]
+let callLogRead (lv: lval) = 
+  let what = Pretty.sprint 80 (d_lval () lv) in
+  Call(None, 
+       Lval(Var(logReads.svar),NoOffset), 
+       [ addr_of_lv lv; mkString what; mkString !currentLoc.file;
+         integer !currentLoc.line], !currentLoc )
+
+let logWrites = mkProto "logWrite" [ ("addr", voidPtrType, []);
+                                     ("what", charPtrType, []);
+                                     ("file", charPtrType, []);
+                                     ("line", intType, []) ]
+let callLogWrite (lv: lval) = 
+  let what = Pretty.sprint 80 (d_lval () lv) in
+  Call(None, 
+       Lval(Var(logWrites.svar), NoOffset), 
+       [ addr_of_lv lv; mkString what; mkString !currentLoc.file;
+         integer !currentLoc.line], !currentLoc )
+
+let logStackFrame  = mkProto "logStackFrame" [ ("func", charPtrType, []) ]
+let callLogStack (fname: string) = 
+  Call(None, 
+       Lval(Var(logStackFrame.svar), NoOffset), 
+       [ mkString fname; ], !currentLoc )
+
+let logAlloc = mkProto "logAlloc" [ ("addr", voidPtrType, []);
+                                    ("size", intType, []);
+                                    ("file", charPtrType, []);
+                                    ("line", intType, []) ]
+let callLogAlloc (szloc: dataLocation) 
+                 (resLoc: dataLocation) 
+                 (args: exp list) 
+                 (res: lval option) = 
+  let sz = extractData szloc args res in 
+  let res = extractData resLoc args res in 
+  Call(None, 
+       Lval(Var(logAlloc.svar), NoOffset), 
+       [ res; sz; mkString !currentLoc.file;
+         integer !currentLoc.line ], !currentLoc )
+    
+  
+let logFree = mkProto "logFree" [ ("addr", voidPtrType, []);
+                                  ("file", charPtrType, []);
+                                  ("line", intType, []) ]
+let callLogFree  (dataloc: dataLocation) 
+                 (args: exp list) 
+                 (res: lval option) = 
+  let data = extractData dataloc args res in 
+  Call(None, 
+       Lval(Var(logFree.svar), NoOffset), 
+       [ data; mkString !currentLoc.file;
+         integer !currentLoc.line ], !currentLoc )
+
+class sfiVisitorClass : Cil.cilVisitor = object (self)
+  inherit nopCilVisitor
+      
+  method vexpr (e: exp) : exp visitAction = 
+    match e with 
+      Lval lv when mustLogLval false lv -> (* A read *)
+        self#queueInstr [ callLogRead lv ];
+        DoChildren
+
+    | _ -> DoChildren
+        
+    
+  method vinst (i: instr) : instr list visitAction = 
+    match i with 
+      Set(lv, e, l) when mustLogLval true lv ->
+        self#queueInstr [ callLogWrite lv ];
+        DoChildren
+
+    | Call(lvo, f, args, l) -> 
+        (* Instrument the write *)
+        (match lvo with 
+          Some lv when mustLogLval true lv -> 
+            self#queueInstr [ callLogWrite lv ]
+        | _ -> ());
+        (* Do the expressions in the call, and then see if we need to 
+         * instrument the function call *)
+        ChangeDoChildrenPost
+          ([i], 
+           (fun il -> 
+             currentLoc := l;
+             match f with 
+               Lval (Var fv, NoOffset) -> begin 
+                 (* Is it an allocator? *)
+                 try 
+                   let szloc, resloc = H.find allocators fv.vname in
+                   il @ [callLogAlloc szloc resloc args lvo]
+                 with Not_found -> begin
+                   (* Is it a deallocator? *)
+                   try 
+                     let resloc = H.find deallocators fv.vname in 
+                     il @ [ callLogFree resloc args lvo ]
+                   with Not_found -> 
+                     il
+                 end
+               end
+             | _ -> il))
+
+    | _ -> DoChildren
+
+  method vfunc (fdec: fundec) = 
+    (* Instead a stack log at the start of a function *)
+    ChangeDoChildrenPost 
+      (fdec,
+       fun fdec -> 
+         fdec.sbody <- 
+           mkBlock 
+             [ mkStmtOneInstr (callLogStack fdec.svar.vname);
+               mkStmt (Block fdec.sbody) ];
+         fdec)
+      
+end
+
+let doit (f: file) =
+  let sfiVisitor = new sfiVisitorClass in
+  let compileLoc (l: location) = function
+      ACons("inres", []) -> InResult
+    | ACons("inarg", [AInt n]) -> InArg n
+    | ACons("inargxarg", [AInt n1; AInt n2]) -> InArgTimesArg (n1, n2)
+    | ACons("pointedby", [AInt n]) -> PointedToByArg n
+    | _ -> E.warn "Invalid location at %a" d_loc l;
+        InResult
+  in
+  iterGlobals f
+    (fun glob -> 
+      match glob with 
+        GFun(fdec, _) when mustSfiFunction fdec -> 
+          ignore (visitCilFunction sfiVisitor fdec)
+      | GPragma(Attr("sfiignore", al), l) -> 
+          List.iter 
+            (function AStr fn -> H.add skipFunctions fn ()
+              | _ -> E.warn "Invalid argument in \"sfiignore\" pragma at %a"
+                            d_loc l)
+            al
+
+      | GPragma(Attr("sfialloc", al), l) -> begin
+          match al with 
+            AStr fname :: locsz :: locres :: [] -> 
+              H.add allocators fname (compileLoc l locsz, compileLoc l locres)
+          | _ -> E.warn "Invalid sfialloc pragma at %a" d_loc l
+      end
+                
+      | GPragma(Attr("sfifree", al), l) -> begin
+          match al with 
+            AStr fname :: locwhat :: [] -> 
+              H.add deallocators fname (compileLoc l locwhat)
+          | _ -> E.warn "Invalid sfifree pragma at %a" d_loc l
+      end
+                
+
+      | _ -> ());
+  (* Now add the prototypes for the instrumentation functions *)
+  f.globals <-
+    GVarDecl (logReads.svar, locUnknown) ::
+    GVarDecl (logWrites.svar, locUnknown) ::
+    GVarDecl (logStackFrame.svar, locUnknown) ::
+    GVarDecl (logAlloc.svar, locUnknown) :: 
+    GVarDecl (logFree.svar, locUnknown) :: f.globals
+
+
+let feature : featureDescr = 
+  { fd_name = "sfi";
+    fd_enabled = doSfi;
+    fd_description = "instrument memory operations";
+    fd_extraopt = [
+    "--sfireads", Arg.Set doSfiReads, "SFI for reads";
+    "--sfiwrites", Arg.Set doSfiWrites, "SFI for writes";
+    ];
+    fd_doit = doit;
+    fd_post_check = true;
+  } 
+