diff options
Diffstat (limited to 'cil/src/ext/partial.ml')
| -rw-r--r-- | cil/src/ext/partial.ml | 851 |
1 files changed, 851 insertions, 0 deletions
diff --git a/cil/src/ext/partial.ml b/cil/src/ext/partial.ml new file mode 100644 index 0000000..4beca3f --- /dev/null +++ b/cil/src/ext/partial.ml @@ -0,0 +1,851 @@ +(* See copyright notice at the end of the file *) +(***************************************************************************** + * Partial Evaluation & Constant Folding + * + * Soundness Assumptions: + * (1) Whole program analysis. You may call functions that are not defined + * (e.g., library functions) but they may not call back. + * (2) An undefined function may not return the address of a function whose + * address is not already taken in the code I can see. + * (3) A function pointer call may only call a function that has its + * address visibly taken in the code I can see. + * + * (More assumptions in the comments below) + *****************************************************************************) +open Cil +open Pretty + +(***************************************************************************** + * A generic signature for Alias Analysis information. Used to compute the + * call graph and do symbolic execution. + ****************************************************************************) +module type AliasInfo = + sig + val can_have_the_same_value : Cil.exp -> Cil.exp -> bool + val resolve_function_pointer : Cil.exp -> (Cil.fundec list) + end + +(***************************************************************************** + * A generic signature for Symbolic Execution execution algorithms. Such + * algorithms are used below to perform constant folding and dead-code + * elimination. You write a "basic-block" symex algorithm, we'll make it + * a whole-program CFG-pruner. + ****************************************************************************) +module type Symex = + sig + type t (* the type of a symex algorithm state object *) + val empty : t (* all values unknown *) + val equal : t -> t -> bool (* are these the same? *) + val assign : t -> Cil.lval -> Cil.exp -> (Cil.exp * t) + (* incorporate an assignment, return the RHS *) + val unassign : t -> Cil.lval -> t + (* lose all information about the given lvalue: assume an + * unknown external value has been assigned to it *) + val assembly : t -> Cil.instr -> t (* handle ASM *) + val assume : t -> Cil.exp -> t (* incorporate an assumption *) + val evaluate : t -> Cil.exp -> Cil.exp (* symbolic evaluation *) + val join : (t list) -> t (* join a bunch of states *) + val call : t -> Cil.fundec -> (Cil.exp list) -> (Cil.exp list * t) + (* we are calling the given function with the given actuals *) + val return : t -> Cil.fundec -> t + (* we are returning from the given function *) + val call_to_unknown_function : t -> t + (* throw away information that may have been changed *) + val debug : t -> unit + end + +(***************************************************************************** + * A generic signature for whole-progam call graphs. + ****************************************************************************) +module type CallGraph = + sig + type t (* the type of a call graph *) + val compute : Cil.file -> t (* file for which we compute the graph *) + val can_call : t -> Cil.fundec -> (Cil.fundec list) + val can_be_called_by : t -> Cil.fundec -> (Cil.fundec list) + val fundec_of_varinfo : t -> Cil.varinfo -> Cil.fundec + end + +(***************************************************************************** + * My cheap-o Alias Analysis. Assume all expressions can have the same + * value and any function with its address taken can be the target of + * any function pointer. + * + * Soundness Assumptions: + * (1) Someone must call "find_all_functions_With_address_taken" before the + * results are valid. This is already done in the code below. + ****************************************************************************) +let all_functions_with_address_taken = ref [] +let find_all_functions_with_address_taken (f : Cil.file) = + iterGlobals f (fun g -> match g with + GFun(fd,_) -> if fd.svar.vaddrof then + all_functions_with_address_taken := fd :: + !all_functions_with_address_taken + | _ -> ()) + +module EasyAlias = + struct + let can_have_the_same_value e1 e2 = true + let resolve_function_pointer e1 = !all_functions_with_address_taken + end + +(***************************************************************************** + * My particular method for computing the Call Graph. + ****************************************************************************) +module EasyCallGraph = functor (A : AliasInfo) -> + struct + type callGraphNode = { + fd : Cil.fundec ; + mutable calledBy : Cil.fundec list ; + mutable calls : Cil.fundec list ; + } + type t = (Cil.varinfo, callGraphNode) Hashtbl.t + + let cgCreateNode cg fundec = + let newnode = { fd = fundec ; calledBy = [] ; calls = [] } in + Hashtbl.add cg fundec.svar newnode + + let cgFindNode cg svar = Hashtbl.find cg svar + + let cgAddEdge cg caller callee = + try + let n1 = cgFindNode cg caller in + let n2 = cgFindNode cg callee in + n1.calls <- n2.fd :: n1.calls ; + n1.calledBy <- n1.fd :: n1.calledBy + with _ -> () + + class callGraphVisitor cg = object + inherit nopCilVisitor + val the_fun = ref None + + method vinst i = + let _ = match i with + Call(_,Lval(Var(callee),NoOffset),_,_) -> begin + (* known function call *) + match !the_fun with + None -> failwith "callGraphVisitor: call outside of any function" + | Some(enclosing) -> cgAddEdge cg enclosing callee + end + | Call(_,e,_,_) -> begin + (* unknown function call *) + match !the_fun with + None -> failwith "callGraphVisitor: call outside of any function" + | Some(enclosing) -> let lst = A.resolve_function_pointer e in + List.iter (fun possible_target_fd -> + cgAddEdge cg enclosing possible_target_fd.svar) lst + end + | _ -> () + in SkipChildren + + method vfunc f = the_fun := Some(f.svar) ; DoChildren + end + + let compute (f : Cil.file) = + let cg = Hashtbl.create 511 in + iterGlobals f (fun g -> match g with + GFun(fd,_) -> cgCreateNode cg fd + | _ -> () + ) ; + visitCilFileSameGlobals (new callGraphVisitor cg) f ; + cg + + let can_call cg fd = + let n = cgFindNode cg fd.svar in n.calls + let can_be_called_by cg fd = + let n = cgFindNode cg fd.svar in n.calledBy + let fundec_of_varinfo cg vi = + let n = cgFindNode cg vi in n.fd + end (* END OF: module EasyCallGraph *) + +(***************************************************************************** + * Necula's Constant Folding Strategem (re-written to be applicative) + * + * Soundness Assumptions: + * (1) Inline assembly does not affect constant folding. + ****************************************************************************) +module OrderedInt = + struct + type t = int + let compare = compare + end +module IntMap = Map.Make(OrderedInt) + +module NeculaFolding = functor (A : AliasInfo) -> + struct + (* Register file. Maps identifiers of local variables to expressions. + * We also remember if the expression depends on memory or depends on + * variables that depend on memory *) + type reg = { + rvi : varinfo ; + rval : exp ; + rmem : bool + } + type t = reg IntMap.t + let empty = IntMap.empty + let equal t1 t2 = (compare t1 t2 = 0) (* use OCAML here *) + let dependsOnMem = ref false + (* Rewrite an expression based on the current register file *) + class rewriteExpClass (regFile : t) = object + inherit nopCilVisitor + method vexpr = function + | Lval (Var v, NoOffset) -> begin + try + let defined = (IntMap.find v.vid regFile) in + if (defined.rmem) then dependsOnMem := true; + (match defined.rval with + | Const(x) -> ChangeTo (defined.rval) + | _ -> DoChildren) + with Not_found -> DoChildren + end + | Lval (Mem _, _) -> dependsOnMem := true; DoChildren + | _ -> DoChildren + end + (* Rewrite an expression and return the new expression along with an + * indication of whether it depends on memory *) + let rewriteExp r (e: exp) : exp * bool = + dependsOnMem := false; + let e' = constFold true (visitCilExpr (new rewriteExpClass r) e) in + e', !dependsOnMem + let eval r e = + let new_e, depends = rewriteExp r e in + new_e + + let setMemory regFile = + (* Get a list of all mappings that depend on memory *) + let depids = ref [] in + IntMap.iter (fun id v -> if v.rmem then depids := id :: !depids) regFile; + (* And remove them from the register file *) + List.fold_left (fun acc id -> IntMap.remove id acc) regFile !depids + + let setRegister regFile (v: varinfo) ((e,b): exp * bool) = + IntMap.add v.vid { rvi = v ; rval = e ; rmem = b; } regFile + + let resetRegister regFile (id: int) = + IntMap.remove id regFile + + class findLval lv contains = object + inherit nopCilVisitor + method vlval l = + if l = lv then + (contains := true ; SkipChildren) + else + DoChildren + end + + let removeMappingsThatDependOn regFile l = + (* Get a list of all mappings that depend on l *) + let depids = ref [] in + IntMap.iter (fun id reg -> + let found = ref false in + ignore (visitCilExpr (new findLval l found) reg.rval) ; + if !found then + depids := id :: !depids + ) regFile ; + (* And remove them from the register file *) + List.fold_left (fun acc id -> IntMap.remove id acc) regFile !depids + + let assign r l e = + let (newe,b) = rewriteExp r e in + let r' = match l with + (Var v, NoOffset) -> + let r'' = setRegister r v (newe,b) in + removeMappingsThatDependOn r'' l + | (Mem _, _) -> setMemory r + | _ -> r + in newe, r' + + let unassign r l = + let r' = match l with + (Var v, NoOffset) -> + let r'' = resetRegister r v.vid in + removeMappingsThatDependOn r'' l + | (Mem _, _) -> setMemory r + | _ -> r + in r' + + let assembly r i = r (* no-op in Necula-world *) + let assume r e = r (* no-op in Necula-world *) + + let evaluate r e = + let (newe,_) = rewriteExp r e in + newe + + (* Join two symex states *) + let join2 (r1 : t) (r2 : t) = + let keep = ref [] in + IntMap.iter (fun id reg -> + try + let reg' = IntMap.find id r2 in + if reg'.rval = reg.rval && reg'.rmem = reg.rmem then + keep := (id,reg) :: !keep + with _ -> () + ) r1 ; + List.fold_left (fun acc (id,v) -> + IntMap.add id v acc) (IntMap.empty) !keep + + let join (lst : t list) = match lst with + [] -> failwith "empty list" + | r :: tl -> List.fold_left + (fun (acc : t) (elt : t) -> join2 acc elt) r tl + + let call r fd el = + let new_arg_list = ref [] in + let final_r = List.fold_left2 (fun r vi e -> + let newe, r' = assign r ((Var(vi),NoOffset)) e in + new_arg_list := newe :: !new_arg_list ; + r' + ) r fd.sformals el in + (List.rev !new_arg_list), final_r + + let return r fd = + let regFile = + List.fold_left (fun r vi -> IntMap.remove vi.vid r) r fd.sformals + in + (* Get a list of all globals *) + let depids = ref [] in + IntMap.iter (fun vid reg -> + if reg.rvi.vglob || reg.rvi.vaddrof then depids := vid :: !depids + ) regFile ; + (* And remove them from the register file *) + List.fold_left (fun acc id -> IntMap.remove id acc) regFile !depids + + + let call_to_unknown_function r = + setMemory r + + let debug r = + IntMap.iter (fun key reg -> + ignore (Pretty.printf "%s <- %a (%b)@!" reg.rvi.vname d_exp reg.rval reg.rmem) + ) r + end (* END OF: NeculaFolding *) + +(***************************************************************************** + * A transformation to make every function call end its statement. So + * { x=1; Foo(); y=1; } + * becomes at least: + * { { x=1; Foo(); } + * { y=1; } } + * But probably more like: + * { { x=1; } { Foo(); } { y=1; } } + ****************************************************************************) +let rec contains_call il = match il with + [] -> false + | Call(_) :: tl -> true + | _ :: tl -> contains_call tl + +class callBBVisitor = object + inherit nopCilVisitor + + method vstmt s = + match s.skind with + Instr(il) when contains_call il -> begin + let list_of_stmts = List.map (fun one_inst -> + mkStmtOneInstr one_inst) il in + let block = mkBlock list_of_stmts in + ChangeDoChildrenPost(s, (fun _ -> + s.skind <- Block(block) ; + s)) + end + | _ -> DoChildren + + method vvdec _ = SkipChildren + method vexpr _ = SkipChildren + method vlval _ = SkipChildren + method vtype _ = SkipChildren +end + +let calls_end_basic_blocks f = + let thisVisitor = new callBBVisitor in + visitCilFileSameGlobals thisVisitor f + +(***************************************************************************** + * A transformation that gives each variable a unique identifier. + ****************************************************************************) +class vidVisitor = object + inherit nopCilVisitor + val count = ref 0 + + method vvdec vi = + vi.vid <- !count ; + incr count ; SkipChildren +end + +let globally_unique_vids f = + let thisVisitor = new vidVisitor in + visitCilFileSameGlobals thisVisitor f + +(***************************************************************************** + * The Weimeric Partial Evaluation Data-Flow Engine + * + * This functor performs flow-sensitive, context-insensitive whole-program + * data-flow analysis with an eye toward partial evaluation and constant + * folding. + * + * Toposort the whole-program inter-procedural CFG to compute + * (1) the number of actual predecessors for each statement + * (2) the global toposort ordering + * + * Perform standard data-flow analysis (joins, etc) on the ICFG until you + * hit a fixed point. If this changed the structure of the ICFG (by + * removing an IF-branch or an empty function call), redo the whole thing. + * + * Soundness Assumptions: + * (1) A "call instruction" is the last thing in its statement. + * Use "calls_end_basic_blocks" to get this. cil/src/main.ml does + * this when you pass --makeCFG. + * (2) All variables have globally unique identifiers. + * Use "globally_unique_vids" to get this. cil/src/main.ml does + * this when you pass --makeCFG. + * (3) This may not be a strict soundness requirement, but I wrote this + * assuming that the input file has all switch/break/continue + * statements removed. + ****************************************************************************) +module MakePartial = + functor (S : Symex) -> + functor (C : CallGraph) -> + functor (A : AliasInfo) -> + struct + + let debug = false + + (* We keep this information about every statement. Ideally this should + * be put in the stmt itself, but CIL doesn't give us space. *) + type sinfo = { (* statement info *) + incoming_state : (int, S.t) Hashtbl.t ; + (* mapping from stmt.sid to Symex.state *) + reachable_preds : (int, bool) Hashtbl.t ; + (* basically a set of all of the stmt.sids that can really + * reach this statement *) + mutable last_used_state : S.t option ; + (* When we last did the Post() of this statement, what + * incoming state did we use? If our new incoming state is + * the same, we don't have to do it again. *) + mutable priority : int ; + (* Whole-program toposort priority. High means "do me first". + * The first stmt in "main()" will have the highest priority. + *) + } + let sinfo_ht = Hashtbl.create 511 + let clear_sinfo () = Hashtbl.clear sinfo_ht + + (* We construct sinfo nodes lazily: if you ask for one that isn't + * there, we build it. *) + let get_sinfo stmt = + try + Hashtbl.find sinfo_ht stmt.sid + with _ -> + let new_sinfo = { incoming_state = Hashtbl.create 3 ; + reachable_preds = Hashtbl.create 3 ; + last_used_state = None ; + priority = (-1) ; } in + Hashtbl.add sinfo_ht stmt.sid new_sinfo ; + new_sinfo + + (* Topological Sort is a DFS in which you assign a priority right as + * you finished visiting the children. While we're there we compute + * the actual number of unique predecessors for each statement. The CIL + * information may be out of date because we keep changing the CFG by + * removing IFs and whatnot. *) + let toposort_counter = ref 1 + let add_edge s1 s2 = + let si2 = get_sinfo s2 in + Hashtbl.replace si2.reachable_preds s1.sid true + + let rec toposort c stmt = + let si = get_sinfo stmt in + if si.priority >= 0 then + () (* already visited! *) + else begin + si.priority <- 0 ; (* currently visiting *) + (* handle function calls in this basic block *) + (match stmt.skind with + (Instr(il)) -> + List.iter (fun i -> + let fd_list = match i with + Call(_,Lval(Var(vi),NoOffset),_,_) -> + begin + try + let fd = C.fundec_of_varinfo c vi in + [fd] + with e -> [] (* calling external function *) + end + | Call(_,e,_,_) -> + A.resolve_function_pointer e + | _ -> [] + in + List.iter (fun fd -> + if List.length fd.sbody.bstmts > 0 then + let fun_stmt = List.hd fd.sbody.bstmts in + add_edge stmt fun_stmt ; + toposort c fun_stmt + ) fd_list + ) il + | _ -> ()); + List.iter (fun succ -> + add_edge stmt succ ; toposort c succ) stmt.succs ; + si.priority <- !toposort_counter ; + incr toposort_counter + end + + (* we set this to true whenever we eliminate an IF or otherwise + * change the CFG *) + let changed_cfg = ref false + + (* Partially evaluate / constant fold a statement. Basically this just + * asks the Symex algorithm to evaluate the RHS in the current state + * and then compute a new state that incorporates the assignment. + * + * However, we have special handling for ifs and calls. If we can + * evaluate an if predicate to a constant, we remove the if. + * + * If we are going to make a call to a function with an empty body, we + * remove the function call. *) + let partial_stmt c state stmt handle_funcall = + let result = match stmt.skind with + Instr(il) -> + let state = ref state in + let new_il = List.map (fun i -> + if debug then begin + ignore (Pretty.printf "Instr %a@!" d_instr i ) + end ; + match i with + | Set(l,e,loc) -> + let e', state' = S.assign !state l e in + state := state' ; + [Set(l,e',loc)] + | Call(lo,(Lval(Var(vi),NoOffset)),al,loc) -> + let result = begin + try + let fd = C.fundec_of_varinfo c vi in + begin + match fd.sbody.bstmts with + [] -> [] (* no point in making this call *) + | hd :: tl -> + let al', state' = S.call !state fd al in + handle_funcall stmt hd state' ; + let state'' = S.return state' fd in + state := state'' ; + [Call(lo,(Lval(Var(vi),NoOffset)),al',loc)] + end + with e -> + let state'' = S.call_to_unknown_function !state in + let al' = List.map (S.evaluate !state) al in + state := state'' ; + [Call(lo,(Lval(Var(vi),NoOffset)),al',loc)] + end in + (* handle return value *) + begin + match lo with + Some(lv) -> state := S.unassign !state lv + | _ -> () + end ; + result + | Call(lo,f,al,loc) -> + let al' = List.map (S.evaluate !state) al in + state := S.call_to_unknown_function !state ; + (match lo with + Some(lv) -> state := S.unassign !state lv + | None -> ()) ; + [Call(lo,f,al',loc)] + | Asm(_) -> state := S.assembly !state i ; [i] + ) il in + stmt.skind <- Instr(List.flatten new_il) ; + if debug then begin + ignore (Pretty.printf "New Stmt is %a@!" d_stmt stmt) ; + end ; + !state + + | If(e,b1,b2,loc) -> + let e' = S.evaluate state e in + (* Pretty.printf "%a evals to %a\n" d_exp e d_exp e' ; *) + + (* helper function to remove an IF branch *) + let remove b remains = begin + changed_cfg := true ; + (match b.bstmts with + | [] -> () + | hd :: tl -> + stmt.succs <- List.filter (fun succ -> succ.sid <> hd.sid) + stmt.succs + ) + end in + + if (e' = one) then begin + if b2.bstmts = [] && b2.battrs = [] then begin + stmt.skind <- Block(b1) ; + match b1.bstmts with + [] -> failwith "partial: completely empty if" + | hd :: tl -> stmt.succs <- [hd] + end else + stmt.skind <- Block( + { bstmts = + [ mkStmt (Block(b1)) ; + mkStmt (If(zero,b2,{bstmts=[];battrs=[];},loc)) ] ; + battrs = [] } ) ; + remove b2 b1 ; + state + end else if (e' = zero) then begin + if b1.bstmts = [] && b1.battrs = [] then begin + stmt.skind <- Block(b2) ; + match b2.bstmts with + [] -> failwith "partial: completely empty if" + | hd :: tl -> stmt.succs <- [hd] + end else + stmt.skind <- Block( + { bstmts = + [ mkStmt (Block(b2)) ; + mkStmt (If(zero,b1,{bstmts=[];battrs=[];},loc)) ] ; + battrs = [] } ) ; + remove b1 b2 ; + state + end else begin + stmt.skind <- If(e',b1,b2,loc) ; + state + end + + | Return(Some(e),loc) -> + let e' = S.evaluate state e in + stmt.skind <- Return(Some(e'),loc) ; + state + + | Block(b) -> + if debug && List.length stmt.succs > 1 then begin + ignore (Pretty.printf "(%a) has successors [%a]@!" + d_stmt stmt + (docList ~sep:(chr '@') (d_stmt ())) + stmt.succs) + end ; + state + + | _ -> state + in result + + (* + * This is the main conceptual entry-point for the partial evaluation + * data-flow functor. + *) + let dataflow (file : Cil.file) (* whole program *) + (c : C.t) (* control-flow graph *) + (initial_state : S.t) (* any assumptions? *) + (initial_stmt : Cil.stmt) (* entry point *) + = begin + (* count the total number of statements in the program *) + let num_stmts = ref 1 in + iterGlobals file (fun g -> match g with + GFun(fd,_) -> begin + match fd.smaxstmtid with + Some(i) -> if i > !num_stmts then num_stmts := i + | None -> () + end + | _ -> () + ) ; + (if debug then + Printf.printf "Dataflow: at most %d statements in program\n" !num_stmts); + + (* create a priority queue in which to store statements *) + let worklist = Heap.create !num_stmts in + + let finished = ref false in + let passes = ref 0 in + + (* add something to the work queue *) + let enqueue caller callee state = begin + let si = get_sinfo callee in + Hashtbl.replace si.incoming_state caller.sid state ; + Heap.insert worklist si.priority callee + end in + + (* we will be finished when we complete a round of data-flow that + * does not change the ICFG *) + while not !finished do + clear_sinfo () ; + incr passes ; + + (* we must recompute the ordering and the predecessor information + * because we may have changed it by removing IFs *) + (if debug then Printf.printf "Dataflow: Topological Sorting & Reachability\n" ); + toposort c initial_stmt ; + + let initial_si = get_sinfo initial_stmt in + Heap.insert worklist initial_si.priority initial_stmt ; + + while not (Heap.is_empty worklist) do + let (p,s) = Heap.extract_max worklist in + if debug then begin + ignore (Pretty.printf "Working on stmt %d (%a) %a@!" + s.sid + (docList ~sep:(chr ',' ++ break) (fun s -> dprintf "%d" s.sid)) + s.succs + d_stmt s) ; + flush stdout ; + end ; + let si = get_sinfo s in + + (* Even though this stmt is on the worklist, we may not have + * to do anything with it if the join of all of the incoming + * states is the same as the last state we used here. *) + let must_recompute, incoming_state = + begin + let list_of_incoming_states = ref [] in + Hashtbl.iter (fun true_pred_sid b -> + let this_pred_state = + try + Hashtbl.find si.incoming_state true_pred_sid + with _ -> + (* this occurs when we're evaluating a statement and we + * have not yet evaluated all of its predecessors (the + * first time we look at a loop head, say). We must be + * conservative. We'll come back later with better + * information (as we work toward the fix-point). *) + S.empty + in + if debug then begin + Printf.printf " Incoming State from %d\n" true_pred_sid ; + S.debug this_pred_state ; + flush stdout ; + end ; + list_of_incoming_states := this_pred_state :: + !list_of_incoming_states + ) si.reachable_preds ; + let merged_incoming_state = + if !list_of_incoming_states = [] then + (* this occurs when we're looking at the first statement + * in "main" -- it has no preds *) + initial_state + else + S.join !list_of_incoming_states + in + if debug then begin + Printf.printf " Merged State:\n" ; + S.debug merged_incoming_state ; + flush stdout ; + end ; + let must_recompute = match si.last_used_state with + None -> true + | Some(last) -> not (S.equal merged_incoming_state last) + in must_recompute, merged_incoming_state + end + in + if must_recompute then begin + si.last_used_state <- Some(incoming_state) ; + let outgoing_state = + (* partially evaluate and optimize the statement *) + partial_stmt c incoming_state s enqueue in + let fresh_succs = s.succs in + (* touch every successor so that we will reconsider it *) + List.iter (fun succ -> + enqueue s succ outgoing_state + ) fresh_succs ; + end else begin + if debug then begin + Printf.printf "No need to recompute.\n" + end + end + done ; + (if debug then Printf.printf "Dataflow: Pass %d Complete\n" !passes) ; + if !changed_cfg then begin + (if debug then Printf.printf "Dataflow: Restarting (CFG Changed)\n") ; + changed_cfg := false + end else + finished := true + done ; + (if debug then Printf.printf "Dataflow: Completed (%d passes)\n" !passes) + + end + + let simplify file c fd (assumptions : (Cil.lval * Cil.exp) list) = + let starting_state = List.fold_left (fun s (l,e) -> + let e',s' = S.assign s l e in + s' + ) S.empty assumptions in + dataflow file c starting_state (List.hd fd.sbody.bstmts) + + end + + +(* + * Currently our partial-eval optimizer is built out of basically nothing. + * The alias analysis is fake, the call grpah is cheap, and we're using + * George's old basic-block symex. Still, it works. + *) +(* Don't you love Functor application? *) +module BasicCallGraph = EasyCallGraph(EasyAlias) +module BasicSymex = NeculaFolding(EasyAlias) +module BasicPartial = MakePartial(BasicSymex)(BasicCallGraph)(EasyAlias) + +(* + * A very easy entry-point to partial evaluation/symbolic execution. + * You pass the Cil file and a list of assumptions (lvalue, exp pairs that + * should be treated as assignments that occur before the program starts). + * + * We partially evaluate and optimize starting from "main". The Cil.file + * is modified in place. + *) +let partial (f : Cil.file) (assumptions : (Cil.lval * Cil.exp) list) = + try + find_all_functions_with_address_taken f ; + let c = BasicCallGraph.compute f in + try + iterGlobals f (fun g -> match g with + GFun(fd,_) when fd.svar.vname = "main" -> + BasicPartial.simplify f c fd assumptions + | _ -> ()) ; + with e -> begin + Printf.printf "Error in DataFlow: %s\n" (Printexc.to_string e) ; + raise e + end + with e -> begin + Printf.printf "Error in Partial: %s\n" (Printexc.to_string e) ; + raise e + end + +let feature : featureDescr = + { fd_name = "partial"; + fd_enabled = Cilutil.doPartial; + fd_description = "interprocedural partial evaluation and constant folding" ; + fd_extraopt = []; + fd_doit = (function (f: file) -> + if not !Cilutil.makeCFG then begin + Errormsg.s (Errormsg.error "--dopartial: you must also specify --domakeCFG\n") + end ; + partial f [] ) ; + fd_post_check = false; + } + +(* + * + * Copyright (c) 2001-2002, + * George C. Necula <necula@cs.berkeley.edu> + * Scott McPeak <smcpeak@cs.berkeley.edu> + * Wes Weimer <weimer@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. + * + *) |