diff options
Diffstat (limited to 'cil/src/ext/sfi.ml')
-rwxr-xr-x | cil/src/ext/sfi.ml | 337 |
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 00000000..9886526c --- /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; + } + |