diff options
Diffstat (limited to 'cil/src/testcil.ml')
| -rw-r--r-- | cil/src/testcil.ml | 440 |
1 files changed, 0 insertions, 440 deletions
diff --git a/cil/src/testcil.ml b/cil/src/testcil.ml deleted file mode 100644 index 0c0ef01..0000000 --- a/cil/src/testcil.ml +++ /dev/null @@ -1,440 +0,0 @@ -(* - * - * 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. - * - *) - -(* A test for CIL *) -open Pretty -open Cil -module E = Errormsg - -let lu = locUnknown - -(* If you have trouble try to reproduce the problem on a smaller type. Try - * limiting the maxNesting and integerKinds *) -let integerKinds = [ IChar; ISChar; IUChar; IInt; IUInt; IShort; IUShort; - ILong; IULong; ILongLong; IULongLong ] -let floatKinds = [ FFloat; FDouble ] - -let baseTypes = - (List.map (fun ik -> (1, fun _ -> TInt(ik, []))) integerKinds) - @ (List.map (fun fk -> (1, fun _ -> TFloat(fk, []))) floatKinds) - - -(* Make a random struct *) -let maxNesting = ref 3 (* Maximum number of levels for struct nesting *) -let maxFields = ref 8 (* The maximum number of fields in a struct *) -let useBitfields = ref false -let useZeroBitfields = ref true - - - -(* Collect here the globals *) -let globals: global list ref = ref [] -let addGlobal (g:global) = globals := g :: !globals -let getGlobals () = List.rev !globals - -(* Collect here the statements for main *) -let statements: stmt list ref = ref [] -let addStatement (s: stmt) = statements := s :: !statements -let getStatements () = List.rev !statements - -(* Keep here the main function *) -let main: fundec ref = ref dummyFunDec -let mainRetVal: varinfo ref = ref dummyFunDec.svar - -let assertId = ref 0 -let addAssert (b: exp) (extra: stmt list) : unit = - incr assertId; - addStatement (mkStmt (If(UnOp(LNot, b, intType), - mkBlock (extra @ - [mkStmt (Return (Some (integer !assertId), - lu))]), - mkBlock [], lu))) - -let addSetRetVal (b: exp) (extra: stmt list) : unit = - addStatement - (mkStmt (If(UnOp(LNot, b, intType), - mkBlock (extra @ - [mkStmtOneInstr (Set(var !mainRetVal, one, lu))]), - mkBlock [], lu))) - - -let printfFun: fundec = - let fdec = emptyFunction "printf" in - fdec.svar.vtype <- - TFun(intType, Some [ ("format", charPtrType, [])], true, []); - fdec - - -let memsetFun: fundec = - let fdec = emptyFunction "memset" in - fdec.svar.vtype <- - TFun(voidPtrType, Some [ ("start", voidPtrType, []); - ("v", intType, []); - ("len", uintType, [])], false, []); - fdec - -let checkOffsetFun: fundec = - let fdec = emptyFunction "checkOffset" in - fdec.svar.vtype <- - TFun(voidType, Some [ ("start", voidPtrType, []); - ("len", uintType, []); - ("expected_start", intType, []); - ("expected_width", intType, []); - ("name", charPtrType, []) ], false, []); - fdec - -let checkSizeOfFun: fundec = - let fdec = emptyFunction "checkSizeOf" in - fdec.svar.vtype <- - TFun(voidType, Some [ ("len", uintType, []); - ("expected", intType, []); - ("name", charPtrType, []) ], false, []); - fdec - - -let doPrintf format args = - mkStmtOneInstr (Call(None, Lval(var printfFun.svar), - (Const(CStr format)) :: args, lu)) - - -(* Select among the choices, each with a given weight *) -type 'a selection = int * (unit -> 'a) -let select (choices: 'a selection list) : 'a = - (* Find the total weight *) - let total = List.fold_left (fun sum (w, _) -> sum + w) 0 choices in - if total = 0 then E.s (E.bug "Total for choices = 0\n"); - (* Pick a random number *) - let thechoice = Random.int total in - (* Now get the choice *) - let rec loop thechoice = function - [] -> E.s (E.bug "Ran out of choices\n") - | (w, c) :: rest -> - if thechoice < w then c () else loop (thechoice - w) rest - in - loop thechoice choices - - -(* Generate a new name *) -let nameId = ref 0 -let newName (base: string) = - incr nameId; - base ^ (string_of_int !nameId) - - -(********** Testing of SIZEOF ***********) - -(* The current selection of types *) -let typeChoices : typ selection list ref = ref [] - -let baseTypeChoices : typ selection list ref = ref [] - - -let currentNesting = ref 0 -let mkCompType (iss: bool) = - if !currentNesting >= !maxNesting then (* Replace it with an int *) - select !baseTypeChoices - else begin - incr currentNesting; - let ci = - mkCompInfo iss (newName "comp") - (fun _ -> - let nrFields = 1 + (Random.int !maxFields) in - let rec mkFields (i: int) = - if i = nrFields then [] else begin - let ft = select !typeChoices in - let fname = "f" ^ string_of_int i in - let fname', width = - if not !useBitfields || not (isIntegralType ft) - || (Random.int 8 >= 6) then - fname, None - else begin - let tw = bitsSizeOf ft in (* Assume this works for TInt *) - let w = (if !useZeroBitfields then 0 else 1) + - Random.int (3 * tw / 4) in - (if w = 0 then "___missing_field_name" else fname), Some w - end - in - (fname', ft, width, [], lu) :: mkFields (i + 1) - end - in - mkFields 0) - [] - in - decr currentNesting; - (* Register it with the file *) - addGlobal (GCompTag(ci, lu)); - TComp(ci, []) - end - -(* Make a pointer type. They are all equal so make one to void *) -let mkPtrType () = TPtr(TVoid([]), []) - -(* Make an array type. *) -let mkArrayType () = - if !currentNesting >= !maxNesting then - select !baseTypeChoices - else begin - incr currentNesting; - let at = TArray(select !typeChoices, Some (integer (1 + (Random.int 32))), - []) in - decr currentNesting; - at - end - - -let testSizeOf () = - let doOne (i: int) = -(* ignore (E.log "doOne %d\n" i); *) - (* Make a random type *) - let t = select !typeChoices in - (* Create a global with that type *) - let g = makeGlobalVar (newName "g") t in - addGlobal (GVar(g, {init=None}, lu)); - addStatement (mkStmtOneInstr(Call(None, Lval(var memsetFun.svar), - [ mkAddrOrStartOf (var g); zero; - SizeOfE(Lval(var g))], lu))); - try -(* if i = 0 then ignore (E.log "0: %a\n" d_plaintype t); *) - let bsz = - try bitsSizeOf t (* This is what we are testing *) - with e -> begin - ignore (E.log "Exception %s caught while computing bitsSizeOf(%a)\n" - (Printexc.to_string e) d_type t); - raise (Failure "") - end - in -(* ignore (E.log "1 "); *) - if bsz mod 8 <> 0 then begin - ignore (E.log "bitsSizeOf did not return a multiple of 8\n"); - raise (Failure ""); - end; -(* ignore (E.log "2 "); *) - (* Check the offset of all fields in there *) - let rec checkOffsets (lv: lval) (lvt: typ) = - match lvt with - TComp(c, _) -> - List.iter - (fun f -> - if f.fname <> "___missing_field_name" then - checkOffsets (addOffsetLval (Field(f, NoOffset)) lv) f.ftype) - c.cfields - | TArray (bt, Some len, _) -> - let leni = - match isInteger len with - Some i64 -> Int64.to_int i64 - | None -> E.s (E.bug "Array length is not a constant") - in - let i = Random.int leni in - checkOffsets (addOffsetLval (Index(integer i, NoOffset)) lv) bt - - | _ -> (* Now a base type *) - let _, off = lv in - let start, width = bitsOffset t off in - let setLv (v: exp) = - match lvt with - TFloat (FFloat, _) -> - Set((Mem (mkCast (AddrOf lv) intPtrType), NoOffset), - v, lu) - | TFloat (FDouble, _) -> - Set((Mem (mkCast (AddrOf lv) - (TPtr(TInt(IULongLong, []), []))), NoOffset), - mkCast v (TInt(IULongLong, [])), lu) - - | (TPtr _ | TInt((IULongLong|ILongLong), _)) -> - Set(lv, mkCast v lvt, lu) - | _ -> Set(lv, v, lu) - in - let ucharPtrType = TPtr(TInt(IUChar, []), []) in - let s = - mkStmt (Instr ([ setLv mone; - Call(None, Lval(var checkOffsetFun.svar), - [ mkCast (mkAddrOrStartOf (var g)) - ucharPtrType; - SizeOfE (Lval(var g)); - integer start; - integer width; - (Const(CStr(sprint 80 - (d_lval () lv))))],lu); - setLv zero])) in - addStatement s - in - checkOffsets (var g) t; -(* ignore (E.log "3 ");*) - (* Now check the size of *) - let s = mkStmtOneInstr (Call(None, Lval(var checkSizeOfFun.svar), - [ SizeOfE (Lval (var g)); - integer (bitsSizeOf t); - mkString g.vname ], lu)) in - addStatement s; -(* ignore (E.log "10\n"); *) - with _ -> () - in - - (* Make the composite choices more likely *) - typeChoices := - [ (1, mkPtrType); - (5, mkArrayType); - (5, fun _ -> mkCompType true); - (5, fun _ -> mkCompType false); ] - @ baseTypes; - baseTypeChoices := baseTypes; - useBitfields := false; - maxFields := 4; - for i = 0 to 100 do - doOne i - done; - - (* Now test the bitfields. *) - typeChoices := [ (1, fun _ -> mkCompType true) ]; - baseTypeChoices := [(1, fun _ -> TInt(IInt, []))]; - useBitfields := true; - - for i = 0 to 100 do - doOne i - done; - - (* Now make it a bit more complicated *) - baseTypeChoices := - List.map (fun ik -> (1, fun _ -> TInt(ik, []))) - [IInt; ILong; IUInt; IULong ]; - useBitfields := true; - for i = 0 to 100 do - doOne i - done; - - (* An really complicated now *) - baseTypeChoices := baseTypes; - useBitfields := true; - for i = 0 to 100 do - doOne i - done; - - () - - -(* Now the main tester. Pass to it the name of a command "cmd" that when - * invoked will compile "testingcil.c" and run the result *) -let createFile () = - - assertId := 0; - nameId := 0; - - (* Start a new file *) - globals := []; - statements := []; - - (* Now make a main function *) - main := emptyFunction "main"; - !main.svar.vtype <- TFun(intType, None, false, []); - mainRetVal := makeGlobalVar "retval" intType; - - addGlobal (GVar(!mainRetVal, {init=None}, lu)); - addGlobal (GText("#include \"testcil.h\"\n")); - addStatement (mkStmtOneInstr(Set(var !mainRetVal, zero, lu))); - - (* Add prototype for printf *) - addGlobal (GVar(printfFun.svar, {init=None}, lu)); - addGlobal (GVar(memsetFun.svar, {init=None}, lu)); - - (* now fill in the composites and the code of main. For simplicity we add - * the statements of main in reverse order *) - - testSizeOf (); - - - (* Now add a return 0 at the end *) - addStatement (mkStmt (Return(Some (Lval(var !mainRetVal)), lu))); - - - (* Add main at the end *) - addGlobal (GFun(!main, lu)); - !main.sbody.bstmts <- getStatements (); - - (* Now build the CIL.file *) - let file = - { fileName = "testingcil.c"; - globals = getGlobals (); - globinit = None; - globinitcalled = false; - } - in - (* Print the file *) - let oc = open_out "testingcil.c" in - dumpFile defaultCilPrinter oc "testingcil.c" file; - close_out oc - - - - - -(* initialization code for the tester *) -let randomStateFile = "testcil.random" (* The name of a file where we store - * the state of the random number - * generator last time *) -let doit (command: string) = - while true do - (* Initialize the random no generator *) - begin - try - let randomFile = open_in randomStateFile in - (* The file exists so restore the Random state *) - Random.set_state (Marshal.from_channel randomFile); - ignore (E.log "!! Restoring Random state from %s\n" randomStateFile); - close_in randomFile; - (* Leave the file there until we succeed *) - with _ -> begin - (* The file does not exist *) - Random.self_init (); - (* Save the state of the generator *) - let randomFile = open_out randomStateFile in - Marshal.to_channel randomFile (Random.get_state()) [] ; - close_out randomFile; - end - end; - createFile (); - (* Now compile and run the file *) - ignore (E.log "Running %s\n" command); - let err = Sys.command command in - if err <> 0 then - E.s (E.bug "Failed to run the command: %s (errcode=%d)" command err) - else begin - ignore (E.log "Successfully ran one more round. Press CTRL-C to stop\n"); - (* Delete the file *) - Sys.remove randomStateFile - end - done - |