From 93d89c2b5e8497365be152fb53cb6cd4c5764d34 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 10:25:25 +0000 Subject: Getting rid of CIL git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cil/src/ext/simplemem.ml | 132 ----------------------------------------------- 1 file changed, 132 deletions(-) delete mode 100644 cil/src/ext/simplemem.ml (limited to 'cil/src/ext/simplemem.ml') diff --git a/cil/src/ext/simplemem.ml b/cil/src/ext/simplemem.ml deleted file mode 100644 index 1b27815c..00000000 --- a/cil/src/ext/simplemem.ml +++ /dev/null @@ -1,132 +0,0 @@ -(* - * - * Copyright (c) 2001-2002, - * George C. Necula - * Scott McPeak - * Wes Weimer - * 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; - } -- cgit