diff options
Diffstat (limited to 'cil/src/ext/simplemem.ml')
-rw-r--r-- | cil/src/ext/simplemem.ml | 132 |
1 files changed, 132 insertions, 0 deletions
diff --git a/cil/src/ext/simplemem.ml b/cil/src/ext/simplemem.ml new file mode 100644 index 00000000..1b27815c --- /dev/null +++ b/cil/src/ext/simplemem.ml @@ -0,0 +1,132 @@ +(* + * + * 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. + * + *) + +(* + * Simplemem: Transform a program so that all memory expressions are + * "simple". Introduce well-typed temporaries to hold intermediate values + * for expressions that would normally involve more than one memory + * reference. + * + * If simplemem succeeds, each lvalue should contain only one Mem() + * constructor. + *) +open Cil + +(* current context: where should we put our temporaries? *) +let thefunc = ref None + +(* build up a list of assignments to temporary variables *) +let assignment_list = ref [] + +(* turn "int a[5][5]" into "int ** temp" *) +let rec array_to_pointer tau = + match unrollType tau with + TArray(dest,_,al) -> TPtr(array_to_pointer dest,al) + | _ -> tau + +(* create a temporary variable in the current function *) +let make_temp tau = + let tau = array_to_pointer tau in + match !thefunc with + Some(fundec) -> makeTempVar fundec ~name:("mem_") tau + | None -> failwith "simplemem: temporary needed outside a function" + +(* separate loffsets into "scalar addition parts" and "memory parts" *) +let rec separate_loffsets lo = + match lo with + NoOffset -> NoOffset, NoOffset + | Field(fi,rest) -> + let s,m = separate_loffsets rest in + Field(fi,s) , m + | Index(_) -> NoOffset, lo + +(* Recursively decompose the lvalue so that what is under a "Mem()" + * constructor is put into a temporary variable. *) +let rec handle_lvalue (lb,lo) = + let s,m = separate_loffsets lo in + match lb with + Var(vi) -> + handle_loffset (lb,s) m + | Mem(Lval(Var(_),NoOffset)) -> + (* special case to avoid generating "tmp = ptr;" *) + handle_loffset (lb,s) m + | Mem(e) -> + begin + let new_vi = make_temp (typeOf e) in + assignment_list := (Set((Var(new_vi),NoOffset),e,!currentLoc)) + :: !assignment_list ; + handle_loffset (Mem(Lval(Var(new_vi),NoOffset)),NoOffset) lo + end +and handle_loffset lv lo = + match lo with + NoOffset -> lv + | Field(f,o) -> handle_loffset (addOffsetLval (Field(f,NoOffset)) lv) o + | Index(exp,o) -> handle_loffset (addOffsetLval (Index(exp,NoOffset)) lv) o + +(* the transformation is implemented as a Visitor *) +class simpleVisitor = object + inherit nopCilVisitor + + method vfunc fundec = (* we must record the current context *) + thefunc := Some(fundec) ; + DoChildren + + method vlval lv = ChangeDoChildrenPost(lv, + (fun lv -> handle_lvalue lv)) + + method unqueueInstr () = + let result = List.rev !assignment_list in + assignment_list := [] ; + result +end + +(* Main entry point: apply the transformation to a file *) +let simplemem (f : file) = + try + visitCilFileSameGlobals (new simpleVisitor) f; + f + with e -> Printf.printf "Exception in Simplemem.simplemem: %s\n" + (Printexc.to_string e) ; raise e + +let feature : featureDescr = + { fd_name = "simpleMem"; + fd_enabled = Cilutil.doSimpleMem; + fd_description = "simplify all memory expressions" ; + fd_extraopt = []; + fd_doit = (function (f: file) -> ignore (simplemem f)) ; + fd_post_check = true; + } |