diff options
Diffstat (limited to 'cil/src/ext/dataslicing.ml')
-rw-r--r-- | cil/src/ext/dataslicing.ml | 462 |
1 files changed, 462 insertions, 0 deletions
diff --git a/cil/src/ext/dataslicing.ml b/cil/src/ext/dataslicing.ml new file mode 100644 index 00000000..35390b40 --- /dev/null +++ b/cil/src/ext/dataslicing.ml @@ -0,0 +1,462 @@ +(* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) + +(* + * + * Copyright (c) 2004, + * Jeremy Condit <jcondit@cs.berkeley.edu> + * 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. + * + *) +open Cil +open Pretty +module E = Errormsg + +let debug = false + +let numRegions : int = 2 + +let newGlobals : global list ref = ref [] + +let curFundec : fundec ref = ref dummyFunDec +let curLocation : location ref = ref locUnknown + +let applyOption (fn : 'a -> 'b) (ao : 'a option) : 'b option = + match ao with + | Some a -> Some (fn a) + | None -> None + +let getRegion (attrs : attributes) : int = + try + match List.hd (filterAttributes "region" attrs) with + | Attr (_, [AInt i]) -> i + | _ -> E.s (bug "bad region attribute") + with Failure _ -> + 1 + +let checkRegion (i : int) (attrs : attributes) : bool = + (getRegion attrs) = i + +let regionField (i : int) : string = + "r" ^ (string_of_int i) + +let regionStruct (i : int) (name : string) : string = + name ^ "_r" ^ (string_of_int i) + +let foldRegions (fn : int -> 'a -> 'a) (base : 'a) : 'a = + let rec helper (i : int) : 'a = + if i <= numRegions then + fn i (helper (i + 1)) + else + base + in + helper 1 + +let rec getTypeName (t : typ) : string = + match t with + | TVoid _ -> "void" + | TInt _ -> "int" + | TFloat _ -> "float" + | TComp (cinfo, _) -> "comp_" ^ cinfo.cname + | TNamed (tinfo, _) -> "td_" ^ tinfo.tname + | TPtr (bt, _) -> "ptr_" ^ (getTypeName bt) + | TArray (bt, _, _) -> "array_" ^ (getTypeName bt) + | TFun _ -> "fn" + | _ -> E.s (unimp "typename") + +let isAllocFunction (fn : exp) : bool = + match fn with + | Lval (Var vinfo, NoOffset) when vinfo.vname = "malloc" -> true + | _ -> false + +let isExternalFunction (fn : exp) : bool = + match fn with + | Lval (Var vinfo, NoOffset) when vinfo.vstorage = Extern -> true + | _ -> false + +let types : (int * typsig, typ) Hashtbl.t = Hashtbl.create 113 +let typeInfos : (int * string, typeinfo) Hashtbl.t = Hashtbl.create 113 +let compInfos : (int * int, compinfo) Hashtbl.t = Hashtbl.create 113 +let varTypes : (typsig, typ) Hashtbl.t = Hashtbl.create 113 +let varCompInfos : (typsig, compinfo) Hashtbl.t = Hashtbl.create 113 + +let rec sliceCompInfo (i : int) (cinfo : compinfo) : compinfo = + try + Hashtbl.find compInfos (i, cinfo.ckey) + with Not_found -> + mkCompInfo cinfo.cstruct (regionStruct i cinfo.cname) + (fun cinfo' -> + Hashtbl.add compInfos (i, cinfo.ckey) cinfo'; + List.fold_right + (fun finfo rest -> + let t = sliceType i finfo.ftype in + if not (isVoidType t) then + (finfo.fname, t, finfo.fbitfield, + finfo.fattr, finfo.floc) :: rest + else + rest) + cinfo.cfields []) + cinfo.cattr + +and sliceTypeInfo (i : int) (tinfo : typeinfo) : typeinfo = + try + Hashtbl.find typeInfos (i, tinfo.tname) + with Not_found -> + let result = + { tinfo with tname = regionStruct i tinfo.tname; + ttype = sliceType i tinfo.ttype; } + in + Hashtbl.add typeInfos (i, tinfo.tname) result; + result + +and sliceType (i : int) (t : typ) : typ = + let ts = typeSig t in + try + Hashtbl.find types (i, ts) + with Not_found -> + let result = + match t with + | TVoid _ -> t + | TInt (_, attrs) -> if checkRegion i attrs then t else TVoid [] + | TFloat (_, attrs) -> if checkRegion i attrs then t else TVoid [] + | TComp (cinfo, attrs) -> TComp (sliceCompInfo i cinfo, attrs) + | TNamed (tinfo, attrs) -> TNamed (sliceTypeInfo i tinfo, attrs) + | TPtr (TVoid _, _) -> t (* Avoid discarding void*. *) + | TPtr (bt, attrs) -> + let bt' = sliceType i bt in + if not (isVoidType bt') then TPtr (bt', attrs) else TVoid [] + | TArray (bt, eo, attrs) -> + TArray (sliceType i bt, applyOption (sliceExp 1) eo, attrs) + | TFun (ret, args, va, attrs) -> + if checkRegion i attrs then + TFun (sliceTypeAll ret, + applyOption + (List.map (fun (aname, atype, aattrs) -> + (aname, sliceTypeAll atype, aattrs))) + args, + va, attrs) + else + TVoid [] + | TBuiltin_va_list _ -> t + | _ -> E.s (unimp "type %a" d_type t) + in + Hashtbl.add types (i, ts) result; + result + +and sliceTypeAll (t : typ) : typ = + begin + match t with + | TComp (cinfo, _) when hasAttribute "var_type_sliced" cinfo.cattr -> + E.s (bug "tried to slice twice") + | _ -> () + end; + let ts = typeSig t in + try + Hashtbl.find varTypes ts + with Not_found -> + let cinfo = + let name = ("var_" ^ (getTypeName t)) in + if debug then ignore (E.log "creating %s\n" name); + try + Hashtbl.find varCompInfos ts + with Not_found -> + mkCompInfo true name + (fun cinfo -> + Hashtbl.add varCompInfos ts cinfo; + foldRegions + (fun i rest -> + let t' = sliceType i t in + if not (isVoidType t') then + (regionField i, t', None, [], !curLocation) :: rest + else + rest) + []) + [Attr ("var_type_sliced", [])] + in + let t' = + if List.length cinfo.cfields > 1 then + begin + newGlobals := GCompTag (cinfo, !curLocation) :: !newGlobals; + TComp (cinfo, []) + end + else + t + in + Hashtbl.add varTypes ts t'; + t' + +and sliceLval (i : int) (lv : lval) : lval = + if debug then ignore (E.log "lval %a\n" d_lval lv); + let lh, offset = lv in + match lh with + | Var vinfo -> + let t = sliceTypeAll vinfo.vtype in + let offset' = + match t with + | TComp (cinfo, _) when hasAttribute "var_type_sliced" cinfo.cattr -> + Field (getCompField cinfo (regionField i), offset) + | _ -> offset + in + Var vinfo, offset' + | Mem e -> + Mem (sliceExp i e), offset + +and sliceExp (i : int) (e : exp) : exp = + if debug then ignore (E.log "exp %a\n" d_exp e); + match e with + | Const c -> Const c + | Lval lv -> Lval (sliceLval i lv) + | UnOp (op, e1, t) -> UnOp (op, sliceExp i e1, sliceType i t) + | BinOp (op, e1, e2, t) -> BinOp (op, sliceExp i e1, sliceExp i e2, + sliceType i t) + | CastE (t, e) -> sliceCast i t e + | AddrOf lv -> AddrOf (sliceLval i lv) + | StartOf lv -> StartOf (sliceLval i lv) + | SizeOf t -> SizeOf (sliceTypeAll t) + | _ -> E.s (unimp "exp %a" d_exp e) + +and sliceCast (i : int) (t : typ) (e : exp) : exp = + let te = typeOf e in + match t, te with + | TInt (k1, _), TInt (k2, attrs2) when k1 = k2 -> + (* Note: We strip off integer cast operations. *) + sliceExp (getRegion attrs2) e + | TInt (k1, _), TPtr _ -> + (* Note: We strip off integer cast operations. *) + sliceExp i e + | TPtr _, _ when isZero e -> + CastE (sliceType i t, sliceExp i e) + | TPtr (bt1, _), TPtr (bt2, _) when (typeSig bt1) = (typeSig bt2) -> + CastE (sliceType i t, sliceExp i e) + | _ -> + E.s (unimp "sketchy cast (%a) -> (%a)\n" d_type te d_type t) + +and sliceExpAll (e : exp) (l : location) : instr list * exp = + let t = typeOf e in + let t' = sliceTypeAll t in + match t' with + | TComp (cinfo, _) when hasAttribute "var_type_sliced" cinfo.cattr -> + let vinfo = makeTempVar !curFundec t in + let instrs = + foldRegions + (fun i rest -> + try + let finfo = getCompField cinfo (regionField i) in + if not (isVoidType finfo.ftype) then + Set ((Var vinfo, Field (finfo, NoOffset)), + sliceExp i e, l) :: rest + else + rest + with Not_found -> + rest) + [] + in + instrs, Lval (var vinfo) + | _ -> [], sliceExp 1 e + +let sliceVar (vinfo : varinfo) : unit = + if hasAttribute "var_sliced" vinfo.vattr then + E.s (bug "tried to slice a var twice"); + let t = sliceTypeAll vinfo.vtype in + if debug then ignore (E.log "setting %s type to %a\n" vinfo.vname d_type t); + vinfo.vattr <- addAttribute (Attr ("var_sliced", [])) vinfo.vattr; + vinfo.vtype <- t + +let sliceInstr (inst : instr) : instr list = + match inst with + | Set (lv, e, loc) -> + if debug then ignore (E.log "set %a %a\n" d_lval lv d_exp e); + let t = typeOfLval lv in + foldRegions + (fun i rest -> + if not (isVoidType (sliceType i t)) then + Set (sliceLval i lv, sliceExp i e, loc) :: rest + else + rest) + [] + | Call (ret, fn, args, l) when isAllocFunction fn -> + let lv = + match ret with + | Some lv -> lv + | None -> E.s (bug "malloc call has no return lval") + in + let t = typeOfLval lv in + foldRegions + (fun i rest -> + if not (isVoidType (sliceType i t)) then + Call (Some (sliceLval i lv), sliceExp 1 fn, + List.map (sliceExp i) args, l) :: rest + else + rest) + [] + | Call (ret, fn, args, l) when isExternalFunction fn -> + [Call (applyOption (sliceLval 1) ret, sliceExp 1 fn, + List.map (sliceExp 1) args, l)] + | Call (ret, fn, args, l) -> + let ret', set = + match ret with + | Some lv -> + let vinfo = makeTempVar !curFundec (typeOfLval lv) in + Some (var vinfo), [Set (lv, Lval (var vinfo), l)] + | None -> + None, [] + in + let instrs, args' = + List.fold_right + (fun arg (restInstrs, restArgs) -> + let instrs, arg' = sliceExpAll arg l in + instrs @ restInstrs, (arg' :: restArgs)) + args ([], []) + in + instrs @ (Call (ret', sliceExp 1 fn, args', l) :: set) + | _ -> E.s (unimp "inst %a" d_instr inst) + +let sliceReturnExp (eo : exp option) (l : location) : stmtkind = + match eo with + | Some e -> + begin + match sliceExpAll e l with + | [], e' -> Return (Some e', l) + | instrs, e' -> Block (mkBlock [mkStmt (Instr instrs); + mkStmt (Return (Some e', l))]) + end + | None -> Return (None, l) + +let rec sliceStmtKind (sk : stmtkind) : stmtkind = + match sk with + | Instr instrs -> Instr (List.flatten (List.map sliceInstr instrs)) + | Block b -> Block (sliceBlock b) + | If (e, b1, b2, l) -> If (sliceExp 1 e, sliceBlock b1, sliceBlock b2, l) + | Break l -> Break l + | Continue l -> Continue l + | Return (eo, l) -> sliceReturnExp eo l + | Switch (e, b, sl, l) -> Switch (sliceExp 1 e, sliceBlock b, + List.map sliceStmt sl, l) +(* + | Loop (b, l, so1, so2) -> Loop (sliceBlock b, l, + applyOption sliceStmt so1, + applyOption sliceStmt so2) +*) + | While (e, b, l) -> While (sliceExp 1 e, sliceBlock b, l) + | DoWhile (e, b, l) -> DoWhile (sliceExp 1 e, sliceBlock b, l) + | For (bInit, e, bIter, b, l) -> + For (sliceBlock bInit, sliceExp 1e, sliceBlock bIter, sliceBlock b, l) + | Goto _ -> sk + | _ -> E.s (unimp "statement") + +and sliceStmt (s : stmt) : stmt = + (* Note: We update statements destructively so that goto/switch work. *) + s.skind <- sliceStmtKind s.skind; + s + +and sliceBlock (b : block) : block = + ignore (List.map sliceStmt b.bstmts); + b + +let sliceFundec (fd : fundec) (l : location) : unit = + curFundec := fd; + curLocation := l; + ignore (sliceBlock fd.sbody); + curFundec := dummyFunDec; + curLocation := locUnknown + +let sliceGlobal (g : global) : unit = + match g with + | GType (tinfo, l) -> + newGlobals := + foldRegions (fun i rest -> GType (sliceTypeInfo i tinfo, l) :: rest) + !newGlobals + | GCompTag (cinfo, l) -> + newGlobals := + foldRegions (fun i rest -> GCompTag (sliceCompInfo i cinfo, l) :: rest) + !newGlobals + | GCompTagDecl (cinfo, l) -> + newGlobals := + foldRegions (fun i rest -> GCompTagDecl (sliceCompInfo i cinfo, l) :: + rest) + !newGlobals + | GFun (fd, l) -> + sliceFundec fd l; + newGlobals := GFun (fd, l) :: !newGlobals + | GVarDecl _ + | GVar _ -> + (* Defer processing of vars until end. *) + newGlobals := g :: !newGlobals + | _ -> + E.s (unimp "global %a\n" d_global g) + +let sliceGlobalVars (g : global) : unit = + match g with + | GFun (fd, l) -> + curFundec := fd; + curLocation := l; + List.iter sliceVar fd.slocals; + List.iter sliceVar fd.sformals; + setFunctionType fd (sliceType 1 fd.svar.vtype); + curFundec := dummyFunDec; + curLocation := locUnknown; + | GVar (vinfo, _, l) -> + curLocation := l; + sliceVar vinfo; + curLocation := locUnknown + | _ -> () + +class dropAttrsVisitor = object + inherit nopCilVisitor + + method vvrbl (vinfo : varinfo) = + vinfo.vattr <- dropAttribute "var_sliced" vinfo.vattr; + DoChildren + + method vglob (g : global) = + begin + match g with + | GCompTag (cinfo, _) -> + cinfo.cattr <- dropAttribute "var_type_sliced" cinfo.cattr; + | _ -> () + end; + DoChildren +end + +let sliceFile (f : file) : unit = + newGlobals := []; + List.iter sliceGlobal f.globals; + List.iter sliceGlobalVars f.globals; + f.globals <- List.rev !newGlobals; + visitCilFile (new dropAttrsVisitor) f + +let feature : featureDescr = + { fd_name = "DataSlicing"; + fd_enabled = ref false; + fd_description = "data slicing"; + fd_extraopt = []; + fd_doit = sliceFile; + fd_post_check = true; + } |