diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | caml/Camlcoq.ml | 4 | ||||
| -rw-r--r-- | caml/Cil2Csyntax.ml | 863 | ||||
| -rw-r--r-- | caml/Main2.ml | 144 | ||||
| -rw-r--r-- | caml/PrintCsyntax.ml | 434 | ||||
| -rw-r--r-- | cil-1.3.5.tar.gz | bin | 0 -> 1139611 bytes | |||
| -rw-r--r-- | cil.patch/astslicer.ml.patch | 40 | ||||
| -rw-r--r-- | cil.patch/cabs2cil.ml.patch | 325 | ||||
| -rw-r--r-- | cil.patch/cfg.ml.patch | 55 | ||||
| -rw-r--r-- | cil.patch/check.ml.patch | 56 | ||||
| -rw-r--r-- | cil.patch/cil.ml.patch | 381 | ||||
| -rw-r--r-- | cil.patch/cil.mli.patch | 59 | ||||
| -rw-r--r-- | cil.patch/dataflow.ml.patch | 27 | ||||
| -rw-r--r-- | cil.patch/dataslicing.ml.patch | 28 | ||||
| -rw-r--r-- | cil.patch/formatparse.mly.patch | 40 | ||||
| -rw-r--r-- | cil.patch/mergecil.ml.patch | 25 | ||||
| -rw-r--r-- | cil.patch/oneret.ml.patch | 38 | ||||
| -rw-r--r-- | cil.patch/ptranal.ml.patch | 28 | ||||
| -rw-r--r-- | cil.patch/usedef.ml.patch | 38 | ||||
| -rw-r--r-- | extraction/.depend | 58 | ||||
| -rw-r--r-- | extraction/Makefile | 16 | ||||
| -rw-r--r-- | test/c/fft.c | 140 |
22 files changed, 2688 insertions, 119 deletions
@@ -1,6 +1,7 @@ COQC=coqc $(INCLUDES) COQDEP=coqdep $(INCLUDES) COQDOC=coqdoc +CILDISTRIB=cil-1.3.5.tar.gz INCLUDES=-I lib -I common -I backend -I cfrontend @@ -52,10 +53,17 @@ proof: $(FILES:.v=.vo) all: $(MAKE) proof + $(MAKE) cil $(MAKE) -C extraction extraction $(MAKE) -C extraction depend $(MAKE) -C extraction +cil: + tar xzf $(CILDISTRIB) + for i in cil.patch/*; do patch -p1 < $$i; done + cd cil; ./configure + $(MAKE) -C cil + documentation: $(COQDOC) --html -d doc $(FLATFILES:%.v=--glob-from doc/%.glob) $(FILES) doc/removeproofs doc/lib.*.html doc/backend.*.html diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index b0bb4ff..ab111c1 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -31,8 +31,8 @@ let rec positive_of_camlint n = if n = 0l then assert false else if n = 1l then Coq_xH else if Int32.logand n 1l = 0l - then Coq_xO (positive_of_camlint (Int32.shift_right n 1)) - else Coq_xI (positive_of_camlint (Int32.shift_right n 1)) + then Coq_xO (positive_of_camlint (Int32.shift_right_logical n 1)) + else Coq_xI (positive_of_camlint (Int32.shift_right_logical n 1)) let z_of_camlint n = if n = 0l then Z0 else diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml new file mode 100644 index 0000000..74bf0eb --- /dev/null +++ b/caml/Cil2Csyntax.ml @@ -0,0 +1,863 @@ +(************************************************************************** +CIL -> CabsCoq translator +**************************************************************************) + +open Cil +open Camlcoq +open AST +open Csyntax + + + + +module type TypeSpecifierTranslator = + sig + val convertIkind: Cil.ikind -> (intsize * signedness) option + val convertFkind: Cil.fkind -> floatsize option + end + + + + + +module Make(TS: TypeSpecifierTranslator) = struct +(*-----------------------------------------------------------------------*) + + +(** Exception raised when an unsupported feature is encountered *) +exception Unsupported of string + + +(** Pre-defined constants *) +let constInt32 = Tint (I32, Signed) +let constInt32uns = Tint (I32, Unsigned) +let const0 = Expr (Econst_int (coqint_of_camlint Int32.zero), constInt32) + + +(** Identifiers for struct and union fields *) +let fieldTable = Hashtbl.create 47 (* hash-table *) +let fieldNum = ref Int32.one (* identifier of the next field *) + + +(** Other global variables *) +let currentLocation = ref Cil.locUnknown +let mainFound = ref false +let currentGlobalPrefix = ref "" +let stringNum = ref 0 (* number of next global for string literals *) +let stringTable = Hashtbl.create 47 + +(** ** Functions related to [struct]s and [union]s *) + +(** Return a unique integer corresponding to a [struct] field *) +let ident_of_string str = + try Hashtbl.find fieldTable str + with Not_found -> let id = positive_of_camlint !fieldNum in + Hashtbl.add fieldTable str id; + fieldNum := Int32.succ !fieldNum; + id + +(* Return the type of a [struct] field *) +let rec getFieldType f = function + | Fnil -> raise Not_found + | Fcons(idf, t, rem) -> if idf = f then t else getFieldType f rem + + + +(** ** Some functions over lists *) + +(** Apply [f] to each element of the OCaml list [l] + and build a Coq list with the results returned by [f] *) +let rec map_coqlist f l = match l with + | [] -> CList.Coq_nil + | a :: b -> CList.Coq_cons (f a, map_coqlist f b) + +(** Keep the elements in a list from [elt] (included) to the end + (used for the translation of the [switch] statement) *) +let rec keepFrom elt = function + | [] -> [] + | (x :: l) as l' -> if x == elt then l' else keepFrom elt l + +(** Keep the elements in a list before [elt'] (excluded) + (used for the translation of the [switch] statement) *) +let rec keepUntil elt' = function + | [] -> [] + | x :: l -> if x == elt' then [] else x :: (keepUntil elt' l) + +(** Keep the elements in a list from [elt] (included) to [elt'] (excluded) + (used for the translation of the [switch] statement) *) +let keepBetween elt elt' l = + keepUntil elt' (keepFrom elt l) + +(** Reverse-append over Coq lists *) + +let rec revappend l1 l2 = + match l1 with + | CList.Coq_nil -> l2 + | CList.Coq_cons(hd, tl) -> revappend tl (CList.Coq_cons (hd, l2)) + +(** ** Functions used to handle locations *) + +(** Update the current location *) +let updateLoc loc = + currentLocation := loc + +(** Convert the current location into a string *) +let currentLoc() = + match !currentLocation with { line=l; file=f } -> + f ^ ":" ^ (if l = -1 then "?" else string_of_int l) ^ ": " + +(** ** Functions used to handle string literals *) +let name_for_string_literal s = + try + Hashtbl.find stringTable s + with Not_found -> + incr stringNum; + let symbol_name = + Printf.sprintf "_%s__stringlit_%d" + !currentGlobalPrefix !stringNum in + let symbol_ident = intern_string symbol_name in + Hashtbl.add stringTable s symbol_ident; + symbol_ident + +let typeStringLiteral s = + Tarray(Tint(I8, Unsigned), z_of_camlint(Int32.of_int(String.length s + 1))) + +let global_for_string s id = + let init = ref CList.Coq_nil in + let add_char c = + init := CList.Coq_cons( + AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c))), + !init) in + add_char '\000'; + for i = String.length s - 1 downto 0 do add_char s.[i] done; + Datatypes.Coq_pair(Datatypes.Coq_pair(id, !init), typeStringLiteral s) + +let globals_for_strings globs = + Hashtbl.fold + (fun s id l -> CList.Coq_cons(global_for_string s id, l)) + stringTable globs + +(** ** Translation functions *) + +(** Convert a [Cil.ikind] into a pair [(intsize * signedness)] *) +let convertIkind ik = + match TS.convertIkind ik with + | Some p -> p + | None -> raise (Unsupported (currentLoc() ^ "integer type specifier")) + + +(** Convert a [Cil.fkind] into a [floatsize] *) +let convertFkind fk = + match TS.convertFkind fk with + | Some fs -> fs + | None -> raise (Unsupported + (currentLoc() ^ "floating-point type specifier")) + + +(** Convert a [Cil.constant] into a [CabsCoq.expr] *) +let rec convertConstant = function + | CInt64 (i64, _, _) -> + let i = coqint_of_camlint (Int64.to_int32 i64) in + Expr (Econst_int i, constInt32) + | CStr s -> + let symb = name_for_string_literal s in + Expr (Evar symb, typeStringLiteral s) + | CWStr _ -> + raise (Unsupported (currentLoc() ^ "wide string literal")) + | CChr c -> + let i = coqint_of_camlint (Int32.of_int (Char.code c)) in + Expr (Econst_int i, constInt32) + | CReal (f, _, _) -> + Expr (Econst_float f, Tfloat F64) + | (CEnum (exp, str, enumInfo)) as enum -> + (* do constant folding on an enum constant *) + let e = Cil.constFold false (Const enum) in + convertExp e + + +(** Convert a [Cil.UnOp] into a [CabsCoq.expr] + ([t] is the type of the result of applying [uop] to [e]) *) +and convertUnop uop e t = + let e' = convertExp e in + let t' = convertTyp t in + let uop' = match uop with + | Neg -> Eunop (Oneg, e') + | BNot -> Eunop (Onotint, e') + | LNot -> Eunop (Onotbool, e') + in + Expr (uop', t') + + +(** Convert a [Cil.BinOp] into a [CabsCoq.expr] + ([t] is the type of the result of applying [bop] to [(e1, e2)], every + arithmetic conversion being made explicit by CIL for both arguments] *) +and convertBinop bop e1 e2 t = + let e1' = convertExp e1 in + let e2' = convertExp e2 in + let t' = convertTyp t in + let bop' = match bop with + | PlusA -> Ebinop (Oadd, e1', e2') + | PlusPI -> Ebinop (Oadd, e1', e2') + | IndexPI -> Ebinop (Oadd, e1', e2') + | MinusA -> Ebinop (Osub, e1', e2') + | MinusPI -> Ebinop (Osub, e1', e2') + | MinusPP -> Ebinop (Osub, e1', e2') + | Mult -> Ebinop (Omul, e1', e2') + | Div -> Ebinop (Odiv, e1', e2') + | Mod -> Ebinop (Omod, e1', e2') + | Shiftlt -> Ebinop (Oshl, e1', e2') + | Shiftrt -> Ebinop (Oshr, e1', e2') + | Lt -> Ebinop (Olt, e1', e2') + | Gt -> Ebinop (Ogt, e1', e2') + | Le -> Ebinop (Ole, e1', e2') + | Ge -> Ebinop (Oge, e1', e2') + | Eq -> Ebinop (Oeq, e1', e2') + | Ne -> Ebinop (One, e1', e2') + | BAnd -> Ebinop (Oand, e1', e2') + | BXor -> Ebinop (Oxor, e1', e2') + | BOr -> Ebinop (Oor, e1', e2') + | LAnd -> Eandbool (e1', e2') + | LOr -> Eorbool (e1', e2') + in + Expr (bop', t') + + +(** Test if two types are compatible + (in order to cast one of the types to the other) *) +and compatibleTypes t1 t2 = true +(* + let isArithmeticType = function + | Tint _ | Tfloat _ -> true + | _ -> false + in + let isPointerType = function + | Tpointer _ | Tarray _ -> true + | _ -> false + in + (t1 = t2) + || (isArithmeticType t1 && isArithmeticType t2) + || match (t1, t2) with + | (Tpointer Tvoid, t) | (t, Tpointer Tvoid) -> isPointerType t + | (Tint _, t) | (t, Tint _) -> isPointerType t + | _ -> false +*) + + +(** Convert a [Cil.CastE] into a [CabsCoq.expr] + (fail if the cast is illegal) *) +and processCast t e = + let t' = convertTyp t in + let te = convertTyp (Cil.typeOf e) in + if compatibleTypes t' te then + let e' = convertExp e in + Expr (Ecast (t', e'), t') + else failwith (currentLoc() ^ "processCast: illegal cast") + + +(** Convert a [Cil.exp list] into an [CamlCoq.exprlist] *) +and processParamsE = function + | [] -> Enil + | e :: l -> + let (Expr (_, t)) as e' = convertExp e in + match t with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "function parameter of type struct or union")) + | _ -> Econs (e', processParamsE l) + + +(** Convert a [Cil.exp] into a [CabsCoq.expr] *) +and convertExp = function + | Const c -> convertConstant c + | Lval lv -> convertLval lv + | SizeOf t -> Expr (Esizeof (convertTyp t), constInt32uns) + | SizeOfE e -> let ty = convertTyp (Cil.typeOf e) in + Expr (Esizeof ty, constInt32uns) + | SizeOfStr str -> raise (Unsupported + (currentLoc() ^ "size of a string literal")) + | AlignOf t -> raise (Unsupported + (currentLoc() ^ "GCC alignment directive")) + | AlignOfE e -> raise (Unsupported + (currentLoc() ^ "GCC alignment directive")) + | UnOp (uop, e, t) -> convertUnop uop e t + | BinOp (bop, e1, e2, t) -> convertBinop bop e1 e2 t + | CastE (t, e) -> processCast t e + | AddrOf lv -> let (Expr (_, t)) as e = convertLval lv in + Expr (Eaddrof e, Tpointer t) + | StartOf lv -> + (* convert an array into a pointer to the beginning of the array *) + match Cil.unrollType (Cil.typeOfLval lv) with + | TArray (t, _, _) -> + let t' = convertTyp t in + let tPtr = Tpointer t' in + let e = convertLval lv in + (* array A of type T replaced by (T* )A *) + Expr (Ecast (tPtr, e), tPtr) +(* + (* array A replaced by &(A[0]) *) + Expr (Eaddrof (Expr (Eindex (e, const0), t')), tPtr) +*) + | _ -> failwith (currentLoc() ^ "convertExp: StartOf applied to a \ + lvalue whose type is not an array") + + +(** Convert a [Cil.lval] into a [CabsCoq.expression] *) +and convertLval lv = + (* convert the offset of the lvalue *) + let rec processOffset ((Expr (_, t)) as e) = function + | NoOffset -> e + | Field (f, ofs) -> + begin match t with + | Tstruct fList -> + begin try + let idf = ident_of_string f.fname in + let t' = getFieldType idf fList in + processOffset (Expr (Efield (e, idf), t')) ofs + with Not_found -> + failwith (currentLoc() ^ "processOffset: no such struct field") + end + | Tunion fList -> + begin try + let idf = ident_of_string f.fname in + let t' = getFieldType idf fList in + processOffset (Expr (Efield (e, idf), t')) ofs + with Not_found -> + failwith (currentLoc() ^ "processOffset: no such union field") + end + | _ -> failwith + (currentLoc() ^ "processOffset: Field on a non-struct nor union") + end + | Index (e', ofs) -> + match t with + | Tarray (t', _) -> let e'' = Eindex (e, convertExp e') in + processOffset (Expr (e'', t')) ofs + | _ -> failwith + (currentLoc() ^ "processOffset: Index on a non-array") + in + (* convert the lvalue *) + match lv with + | (Var v, ofs) -> + let id = intern_string v.vname in + processOffset (Expr (Evar id, convertTyp v.vtype)) ofs + | (Mem e, ofs) -> + match Cil.unrollType (Cil.typeOf e) with + | TPtr (t, _) -> let e' = Ederef (convertExp e) in + processOffset (Expr (e', convertTyp t)) ofs + | _ -> failwith + (currentLoc() ^ "convertLval: Mem on a non-pointer") + + +(** Convert a [(Cil.string * Cil.typ * Cil.attributes)] list + into a [typelist] *) +and processParamsT convert = function + | [] -> Tnil + | (_, t, _) :: l -> + let t' = convert t in + match t' with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "function parameter of type struct or union")) + | _ -> Tcons (t', processParamsT convert l) + + +(** Convert a [Cil.typ] into a [coq_type] *) +and convertTyp = function + | TVoid _ -> Tvoid + | TInt (k, _) -> let (x,y) = convertIkind k in Tint (x, y) + | TFloat (k, _) -> Tfloat (convertFkind k) + | TPtr (t, _) -> Tpointer (convertTyp t) + | TArray (t, eOpt, _) -> + begin match eOpt with + | Some (Const (CInt64 (i64, _, _))) -> + Tarray (convertTyp t, coqint_of_camlint (Int64.to_int32 i64)) + | Some _ -> raise (Unsupported + (currentLoc() ^ "size of array type not an integer constant")) + | None -> raise (Unsupported + (currentLoc() ^ "array type of unspecified size")) + end + | TFun (t, argListOpt, vArg, _) -> + (* Treat unprototyped functions as 0-argument functions, + and treat variadic functions as fixed-arity functions. + We will get type mismatches at applications, which we + compensate by casting the function type to the type + derived from the types of the actual arguments. *) + let argList = + match argListOpt with + | None -> [] + | Some l -> l + in + let t' = convertTyp t in + begin match t' with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "return value of type struct or union")) + | _ -> Tfunction (processParamsT convertTyp argList, t') + end + | TNamed (tinfo, _) -> convertTyp tinfo.ttype + | TComp (c, _) -> + let rec convertFieldList = function + | [] -> Fnil + | {fname=str; ftype=t} :: rem -> + let idf = ident_of_string str in + let t' = convertCompositeType [c.ckey] t in + Fcons(idf, t', convertFieldList rem) in + let fList = convertFieldList c.cfields in + if c.cstruct then Tstruct fList else Tunion fList + | TEnum _ -> constInt32 (* enum constants are integers *) + | TBuiltin_va_list _ -> raise (Unsupported + (currentLoc() ^ "GCC built-in function")) + +(** Convert a [Cil.typ] within a composite structure into a [coq_type] *) +and convertCompositeType env = function + | TNamed (tinfo, _) -> convertCompositeType env tinfo.ttype + | TPtr _ -> Tpointer Tvoid + | TArray (ta, eOpt, _) -> + begin match eOpt with + | Some (Const (CInt64 (i64, _, _))) -> + let ta' = convertCompositeType env ta in + Tarray (ta', coqint_of_camlint (Int64.to_int32 i64)) + | Some _ -> raise (Unsupported + (currentLoc() ^ "size of array type not an integer constant")) + | None -> raise (Unsupported + (currentLoc() ^ "array type of unspecified size")) + end + | TFun (t, argListOpt, vArg, _) -> + if vArg then raise (Unsupported (currentLoc() ^ "variadic function")) + else + let argList = + match argListOpt with + | None -> + print_string ("Warning: " ^ + currentLoc() ^ "unknown function signature\n"); + [] + | Some l -> l + in + let convert = convertCompositeType env in + let t' = convert t in + begin match t' with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "return value of type struct or union")) + | _ -> Tfunction (processParamsT convert argList, t') + end + | TComp (c, _) -> + if List.mem c.ckey env then + failwith (currentLoc() ^ + "convertCompositeType: illegal recursive structure"); + let rec convertFieldList = function + | [] -> Fnil + | {fname=str; ftype=t} :: rem -> + let idf = ident_of_string str in + let t' = convertCompositeType (c.ckey :: env) t in + Fcons(idf, t', convertFieldList rem) in + let fList = convertFieldList c.cfields in + if c.cstruct then Tstruct fList else Tunion fList + | t -> convertTyp t + + +(** Convert a [Cil.varinfo] into a pair [(ident * coq_type)] *) +let convertVarinfo v = + updateLoc(v.vdecl); + let id = intern_string v.vname in + Datatypes.Coq_pair (id, convertTyp v.vtype) + + +(** Convert a [Cil.varinfo] into a pair [(ident * coq_type)] + (fail if the variable is of type struct or union) *) +let convertVarinfoParam v = + updateLoc(v.vdecl); + let id = intern_string v.vname in + let t' = convertTyp v.vtype in + match t' with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "function parameter of type struct or union")) + | _ -> Datatypes.Coq_pair (id, t') + + +(** Convert a [Cil.exp] which has a function type into a [CabsCoq.expr] + (used only to translate function calls) *) +let convertExpFuncall e tfun eList = + match tfun with + | TFun (t, argListOpt, vArg, _) -> + let params = processParamsE eList in + let (Expr (efun, tfun)) as e' = convertExp e in + begin match argListOpt, vArg with + | Some argList, false -> + if List.length argList = List.length eList then (e', params) + else failwith + (currentLoc() ^ "convertExpFuncall: wrong number of arguments") + | _, _ -> + (* For variadic or unprototyped functions, we synthesize the + "real" type of the function from that of the actual + arguments, and insert a cast around e'. *) + begin match tfun with + | Tfunction (_, tret) -> + let rec typeOfExprList = function + | Enil -> Tnil + | Econs (Expr (_, ty), rem) -> + Tcons (ty, typeOfExprList rem) in + let tfun = Tfunction (typeOfExprList params, tret) in + (Expr (Ecast(tfun, e'), tfun), params) + | _ -> failwith + (currentLoc() ^ "convertExpFuncall: incorrect function type") + end + end + | _ -> failwith (currentLoc() ^ "convertExpFuncall: not a function") + + +(** Convert a [Cil.instr list] into a [CabsCoq.statement] *) +let rec processInstrList l = + (* convert an instruction *) + let convertInstr = function + | Set (lv, e, loc) -> + updateLoc(loc); + begin match convertTyp (Cil.typeOf e) with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "struct or union assignment")) + | t -> Sassign (convertLval lv, convertExp e) + end + | Call (lvOpt, e, eList, loc) -> + updateLoc(loc); + begin match Cil.unrollType (Cil.typeOf e) with + | TFun (t, _, _, _) as tfun -> + let t' = convertTyp t in + let (efun, params) = convertExpFuncall e tfun eList in + let e' = Expr (Ecall (efun, params), t') in + begin match lvOpt with + | None -> Sexpr e' + | Some lv -> + let (Expr (_, tlv)) as elv = convertLval lv in + begin match tlv with + | Tstruct _ | Tunion _ -> raise (Unsupported + (currentLoc() ^ "struct or union assignment")) + | _ -> + if tlv = t' then + Sassign (elv, e') + else + (* a cast must be inserted *) + if compatibleTypes tlv t' then + Sassign (elv, + Expr (Ecast (tlv, e'), tlv)) + else failwith + (currentLoc() ^ "processCast: illegal cast") + end + end + | _ -> failwith (currentLoc() ^ "convertInstr: illegal call") + end + | Asm (_, _, _, _, _, loc) -> + updateLoc(loc); + raise (Unsupported (currentLoc() ^ "inline assembly")) + in + (* convert a list of instructions *) + match l with + | [] -> Sskip + | [s] -> convertInstr s + | s :: l -> Ssequence (convertInstr s, processInstrList l) + + +(** Convert a [Cil.stmt list] into a [CabsCoq.statement] *) +let rec processStmtList = function + | [] -> Sskip + | [s] -> convertStmt s + | s :: l -> Ssequence (convertStmt s, processStmtList l) + + +(** Return the list of the constant expressions in a label list + (return [None] if this is the default case) + (fail if the constant expression is not of type integer) *) +and getCaseList lblList = + match lblList with + | [] -> Some [] + | Label (_, loc, _) :: l -> updateLoc(loc); getCaseList l + | Default loc :: _ -> updateLoc(loc); None + | Case (e, loc) :: l -> + updateLoc(loc); + begin match convertExp e with + | Expr (Econst_int n, _) -> + begin match getCaseList l with + | None -> None + | Some cl -> Some (n :: cl) + end + | _ -> failwith (currentLoc() ^ "getCaseList: case label does not \ + reduce to an integer constant") + end + + +(** Convert a list of integers into a [CabsCoq.lblStatementList] *) +and processCaseList cl s lrem = + match cl with + | [] -> failwith + (currentLoc() ^ "processCaseList: syntax error in switch statement") + | [n] -> LScase (n, s, lrem) + | n1 :: l -> LScase (n1, Sskip, processCaseList l s lrem) + + +(** Convert a [Cil.stmt list] which is the body of a Switch structure + into a [CabsCoq.lblStatementList] + (Pre-condition: all the Case labels are supposed to be at the same level, + ie. no nested structures) *) +and processLblStmtList switchBody = function + | [] -> LSdefault Sskip + | [ls] -> + let s = processStmtList (keepFrom ls switchBody) in + begin match getCaseList ls.labels with + | None -> LSdefault s + | Some cl -> processCaseList cl s (LSdefault Sskip) + end + | ls :: ((ls' :: _) as l) -> + if ls.labels = ls'.labels then processLblStmtList switchBody l + else + begin match getCaseList ls.labels with + | None -> raise (Unsupported (currentLoc() ^ + "default case is not at the end of the switch structure")) + | Some cl -> + let s = processStmtList (keepBetween ls ls' switchBody) in + let lrem = processLblStmtList switchBody l in + processCaseList cl s lrem + end + + +(** Convert a [Cil.stmt] into a [CabsCoq.statement] *) +and convertStmt s = + match s.skind with + | Instr iList -> processInstrList iList + | Return (eOpt, loc) -> + updateLoc(loc); + let eOpt' = match eOpt with + | None -> Datatypes.None + | Some e -> Datatypes.Some (convertExp e) + in + Sreturn eOpt' + | Goto (_, loc) -> + updateLoc(loc); + raise (Unsupported (currentLoc() ^ "goto statement")) + | Break loc -> + updateLoc(loc); + Sbreak + | Continue loc -> + updateLoc(loc); + Scontinue + | If (e, b1, b2, loc) -> + updateLoc(loc); + let e1 = processStmtList b1.bstmts in + let e2 = processStmtList b2.bstmts in + Sifthenelse (convertExp e, e1, e2) + | Switch (e, b, l, loc) -> + updateLoc(loc); + Sswitch (convertExp e, processLblStmtList b.bstmts l) + | While (e, b, loc) -> + updateLoc(loc); + Swhile (convertExp e, processStmtList b.bstmts) + | DoWhile (e, b, loc) -> + updateLoc(loc); + Sdowhile (convertExp e, processStmtList b.bstmts) + | For (bInit, e, bIter, b, loc) -> + updateLoc(loc); + let sInit = processStmtList bInit.bstmts in + let e' = convertExp e in + let sIter = processStmtList bIter.bstmts in + Sfor (sInit, e', sIter, processStmtList b.bstmts) + | Block b -> processStmtList b.bstmts + | TryFinally (_, _, loc) -> + updateLoc(loc); + raise (Unsupported (currentLoc() ^ "try...finally statement")) + | TryExcept (_, _, _, loc) -> + updateLoc(loc); + raise (Unsupported (currentLoc() ^ "try...except statement")) + + +(** Convert a [Cil.GFun] into a pair [(ident * coq_fundecl)] *) +let convertGFun fdec = + let v = fdec.svar in + let ret = match v.vtype with + | TFun (t, _, vArg, _) -> + if vArg then raise (Unsupported (currentLoc() ^ "variadic function")) + else + begin match convertTyp t with + | Tstruct _ | Tunion _ -> raise (Unsupported (currentLoc() ^ + "return value of type struct or union")) + | t' -> t' + end + | _ -> failwith (currentLoc() ^ "convertGFun: incorrect function type") + in + let args = map_coqlist convertVarinfoParam fdec.sformals in (* parameters*) + let varList = map_coqlist convertVarinfo fdec.slocals in (* local vars *) + let s = processStmtList fdec.sbody.bstmts in (* function body *) + if v.vname = "main" then mainFound := true; + Datatypes.Coq_pair + (intern_string v.vname, + Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s }) + + +(** Auxiliary for [convertInit] *) + +let rec initDataLen accu = function + | CList.Coq_nil -> accu + | CList.Coq_cons(i1, il) -> + let sz = match i1 with + | Init_int8 _ -> 1l + | Init_int16 _ -> 2l + | Init_int32 _ -> 4l + | Init_float32 _ -> 4l + | Init_float64 _ -> 8l + | Init_space n -> camlint_of_z n in + initDataLen (Int32.add sz accu) il + +(** Convert a [Cil.init] into a list of [AST.init_data] prepended to + the given list [k]. *) + +let rec convertInit init k = + match init with + | SingleInit e -> + begin match Cil.constFold true e with + | Const (CInt64(n, ikind, _)) -> + begin match convertIkind ikind with + | (I8, _) -> + CList.Coq_cons(Init_int8 (coqint_of_camlint (Int64.to_int32 n)), k) + | (I16, _) -> + CList.Coq_cons(Init_int16 (coqint_of_camlint (Int64.to_int32 n)), k) + | (I32, _) -> + CList.Coq_cons(Init_int32 (coqint_of_camlint (Int64.to_int32 n)), k) + end + | Const (CReal(n, fkind, _)) -> + begin match convertFkind fkind with + | F32 -> + CList.Coq_cons(Init_float32 n, k) + | F64 -> + CList.Coq_cons(Init_float64 n, k) + end + | _ -> + raise (Unsupported (currentLoc() ^ + "this kind of expression is not supported in global initializers")) + end + | CompoundInit(ty, data) -> + let init = (* in reverse order *) + Cil.foldLeftCompoundAll + ~doinit: (fun ofs init ty k -> convertInit init k) + ~ct: ty + ~initl: data + ~acc: CList.Coq_nil in + (* For struct or union, pad to size of type *) + begin match Cil.unrollType ty with + | TComp _ -> + let act_len = initDataLen 0l init in + let exp_len = camlint_of_z (Csyntax.sizeof (convertTyp ty)) in + assert (act_len <= exp_len); + let init' = + if act_len < exp_len + then let spc = z_of_camlint (Int32.sub exp_len act_len) in + CList.Coq_cons(Init_space spc, init) + else init in + revappend init' k + | _ -> + revappend init k + end + +(** Convert a [Cil.initinfo] into a list of [AST.init_data] *) + +let convertInitInfo ty info = + match info.init with + | None -> + CList.Coq_cons(Init_space(Csyntax.sizeof (convertTyp ty)), CList.Coq_nil) + | Some init -> + convertInit init CList.Coq_nil + +(** Convert a [Cil.GVar] into a global variable definition *) + +let convertGVar v i = + updateLoc(v.vdecl); + let id = intern_string v.vname in + Datatypes.Coq_pair (Datatypes.Coq_pair(id, convertInitInfo v.vtype i), + convertTyp v.vtype) + + +(** Convert a [Cil.GVarDecl] into a global variable declaration *) + +let convertExtVar v = + updateLoc(v.vdecl); + let id = intern_string v.vname in + Datatypes.Coq_pair (Datatypes.Coq_pair(id, CList.Coq_nil), + convertTyp v.vtype) + +(** Convert a [Cil.GVarDecl] into an external function declaration *) + +let convertExtFun v = + updateLoc(v.vdecl); + match convertTyp v.vtype with + | Tfunction(args, res) -> + let id = intern_string v.vname in + Datatypes.Coq_pair (id, External(id, args, res)) + | _ -> + assert false + +(** Convert a [Cil.global list] into a pair whose first component, + of type [(ident * coq_function) coqlist], represents the definitions of the + functions and the second component, of type [(ident * coq_type) coqlist], + the definitions of the global variables of the program *) +let rec processGlobals = function + | [] -> (CList.Coq_nil, CList.Coq_nil) + | g :: l -> + let (fList, vList) as rem = processGlobals l in + match g with + | GType _ -> rem (* typedefs are unrolled... *) + | GCompTag _ -> rem + | GCompTagDecl _ -> rem + | GEnumTag _ -> rem (* enum constants are folded... *) + | GEnumTagDecl _ -> rem + | GVarDecl (v, loc) -> + updateLoc(loc); + (* Functions become external declarations, + variables become uninitialized variables *) + if Cil.isFunctionType v.vtype + then (CList.Coq_cons (convertExtFun v, fList), vList) + else (fList, CList.Coq_cons (convertExtVar v, vList)) + | GVar (v, init, loc) -> + updateLoc(loc); + (fList, CList.Coq_cons (convertGVar v init, vList)) + | GFun (fdec, loc) -> + updateLoc(loc); + (CList.Coq_cons (convertGFun fdec, fList), vList) + | GAsm (_, loc) -> + updateLoc(loc); + raise (Unsupported (currentLoc() ^ "asm statement")) + | GPragma (_, loc) -> + updateLoc(loc); + print_string ("Warning: " ^ + currentLoc() ^ "pragma directive ignored\n"); + rem + | GText _ -> rem (* comments are ignored *) + +(** Eliminate forward declarations of globals that are defined later *) + +let cleanupGlobals globs = + let defined = + List.fold_right + (fun g def -> + match g with GVar (v, init, loc) -> v.vname :: def + | _ -> def) + globs [] in + List.filter + (function GVarDecl(v, loc) -> not(List.mem v.vname defined) + | g -> true) + globs + +(** Convert a [Cil.file] into a [CabsCoq.program] *) +let convertFile f = + currentGlobalPrefix := + Filename.chop_extension (Filename.basename f.fileName); + stringNum := 0; + Hashtbl.clear stringTable; + let (funList, defList) = processGlobals (cleanupGlobals f.globals) in + let funList' = match f.globinit with + | Some fdec -> CList.Coq_cons (convertGFun fdec, funList) + | None -> funList in + let defList' = globals_for_strings defList in +(*** + if not !mainFound then (* no main function *) + print_string ("Warning: program has no main function! (you should \ + probably have used ccomp's -nomain option)\n"); +***) + { AST.prog_funct = funList'; + AST.prog_vars = defList'; + AST.prog_main = intern_string "main" } + + +(*-----------------------------------------------------------------------*) +end + diff --git a/caml/Main2.ml b/caml/Main2.ml index 4181575..713af82 100644 --- a/caml/Main2.ml +++ b/caml/Main2.ml @@ -1,5 +1,105 @@ open Printf -open Datatypes + +(* For the CIL -> Csyntax translator: + + * The meaning of some type specifiers may depend on compiler options: + the size of an int or the default signedness of char, for instance. + + * Those type conversions may be parameterized thanks to a functor. + + * Remark: [None] means that the type specifier is not supported + (that is, an Unsupported exception will be raised if that type + specifier is encountered in the program). +*) + +module TypeSpecifierTranslator = struct + + open Cil + open Csyntax + + (** Convert a Cil.ikind into an (intsize * signedness) option *) + let convertIkind = function + | IChar -> Some (I8, Unsigned) + | ISChar -> Some (I8, Signed) + | IUChar -> Some (I8, Unsigned) + | IInt -> Some (I32, Signed) + | IUInt -> Some (I32, Unsigned) + | IShort -> Some (I16, Signed) + | IUShort -> Some (I16, Unsigned) + | ILong -> Some (I32, Signed) + | IULong -> Some (I32, Unsigned) + | ILongLong -> (***Some (I32, Signed)***) None + | IULongLong -> (***Some (I32, Unsigned)***) None + + (** Convert a Cil.fkind into an floatsize option *) + let convertFkind = function + | FFloat -> Some F32 + | FDouble -> Some F64 + | FLongDouble -> (***Some F64***) None + +end + +module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator) + +let prepro_options = ref [] +let save_csyntax = ref false + +let preprocess file = + let temp = Filename.temp_file "compcert" ".i" in + let cmd = + sprintf "gcc %s -D__COMPCERT__ -E %s > %s" + (String.concat " " (List.rev !prepro_options)) + file + temp in + if Sys.command cmd = 0 + then temp + else (eprintf "Error during preprocessing.\n"; exit 2) + +let process_c_file sourcename = + let targetname = Filename.chop_suffix sourcename ".c" in + (* Preprocessing with cpp *) + let preproname = preprocess sourcename in + (* Parsing and production of a CIL.file *) + let cil = + try + Frontc.parse preproname () + with + Frontc.ParseError msg -> + eprintf "Error during parsing: %s\n" msg; + exit 2 in + Sys.remove preproname; + (* Restore source file name before preprocessing *) + cil.Cil.fileName <- sourcename; + (* Cleanup in the CIL.file *) + Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil; + (* Conversion to Csyntax *) + let csyntax = + try + Cil2CsyntaxTranslator.convertFile cil + with + | Cil2CsyntaxTranslator.Unsupported msg -> + eprintf "Unsupported C feature: %s\n" msg; + exit 2 + | Failure msg -> + eprintf "Error in translation CIL -> Csyntax:\n%s\n" msg; + exit 2 in + (* Save Csyntax if requested *) + if !save_csyntax then begin + let oc = open_out (targetname ^ ".csyntax") in + PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; + close_out oc + end; + (* Convert to PPC *) + let ppc = + match Main.transf_c_program csyntax with + | Datatypes.Some x -> x + | Datatypes.None -> + eprintf "Error in translation Csyntax -> PPC\n"; + exit 2 in + (* Save PPC asm *) + let oc = open_out (targetname ^ ".s") in + PrintPPC.print_program oc ppc; + close_out oc let process_cminor_file sourcename = let targetname = Filename.chop_suffix sourcename ".cm" ^ ".s" in @@ -9,10 +109,10 @@ let process_cminor_file sourcename = match Main.transf_cminor_program (CMtypecheck.type_program (CMparser.prog CMlexer.token lb)) with - | None -> + | Datatypes.None -> eprintf "Compiler failure\n"; exit 2 - | Some p -> + | Datatypes.Some p -> let oc = open_out targetname in PrintPPC.print_program oc p; close_out oc @@ -29,12 +129,36 @@ let process_cminor_file sourcename = sourcename msg; exit 2 -let process_file filename = - if Filename.check_suffix filename ".cm" then - process_cminor_file filename - else - raise (Arg.Bad ("unknown file type " ^ filename)) +(* Command-line parsing *) + +let starts_with s1 s2 = + String.length s1 >= String.length s2 && + String.sub s1 0 (String.length s2) = s2 + +let rec parse_cmdline i = + if i < Array.length Sys.argv then begin + let s = Sys.argv.(i) in + if s = "-dcsyntax" then begin + save_csyntax := true; + parse_cmdline (i + 1) + end else + if starts_with s "-I" || starts_with s "-D" || starts_with s "-U" + then begin + prepro_options := s :: !prepro_options; + parse_cmdline (i + 1) + end else + if Filename.check_suffix s ".cm" then begin + process_cminor_file s; + parse_cmdline (i + 1) + end else + if Filename.check_suffix s ".c" then begin + process_c_file s; + parse_cmdline (i + 1) + end else begin + eprintf "Unknown argument `%s'\n" s; + exit 2 + end + end let _ = - Arg.parse [] process_file - "Usage: ccomp <options> <files>\nOptions are:" + parse_cmdline 1 diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml new file mode 100644 index 0000000..ff2af16 --- /dev/null +++ b/caml/PrintCsyntax.ml @@ -0,0 +1,434 @@ +(** Pretty-printer for Csyntax *) + +open Format +open Camlcoq +open CList +open Datatypes +open AST +open Csyntax + +let name_unop = function + | Onotbool -> "!" + | Onotint -> "~" + | Oneg -> "-" + + +let name_binop = function + | Oadd -> "+" + | Osub -> "-" + | Omul -> "*" + | Odiv -> "/" + | Omod -> "%" + | Oand -> "&" + | Oor -> "|" + | Oxor -> "^" + | Oshl -> "<<" + | Oshr -> ">>" + | Oeq -> "==" + | One -> "!=" + | Olt -> "<" + | Ogt -> ">" + | Ole -> "<=" + | Oge -> ">=" + +let name_inttype sz sg = + match sz, sg with + | I8, Signed -> "signed char" + | I8, Unsigned -> "unsigned char" + | I16, Signed -> "short" + | I16, Unsigned -> "unsigned short" + | I32, Signed -> "int" + | I32, Unsigned -> "unsigned int" + +let name_floattype sz = + match sz with + | F32 -> "float" + | F64 -> "double" + +(* Naming of structs and unions *) + +type su_kind = Struct | Union + +let struct_union_names = ref [] +let struct_union_name_counter = ref 0 + +let register_struct_union kind fld = + if not (List.mem_assoc (kind, fld) !struct_union_names) then begin + incr struct_union_name_counter; + let s = + match kind with + | Struct -> sprintf "s%d" !struct_union_name_counter + | Union -> sprintf "u%d" !struct_union_name_counter in + struct_union_names := ((kind, fld), s) :: !struct_union_names + end + +let struct_union_name kind fld = + try List.assoc (kind, fld) !struct_union_names with Not_found -> "<unknown>" + +(* Declarator (identifier + type) *) + +let name_optid id = + if id = "" then "" else " " ^ id + +let parenthesize_if_pointer id = + if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id + +let rec name_cdecl id ty = + match ty with + | Tvoid -> + "void" ^ name_optid id + | Tint(sz, sg) -> + name_inttype sz sg ^ name_optid id + | Tfloat sz -> + name_floattype sz ^ name_optid id + | Tpointer t -> + name_cdecl ("*" ^ id) t + | Tarray(t, n) -> + name_cdecl + (sprintf "%s[%ld]" (parenthesize_if_pointer id) (camlint_of_coqint n)) + t + | Tfunction(args, res) -> + let b = Buffer.create 20 in + if id = "" + then Buffer.add_string b "(*)" + else Buffer.add_string b (parenthesize_if_pointer id); + Buffer.add_char b '('; + let rec add_args first = function + | Tnil -> () + | Tcons(t1, tl) -> + if not first then Buffer.add_string b ", "; + Buffer.add_string b (name_cdecl "" t1); + add_args false tl in + add_args true args; + Buffer.add_char b ')'; + name_cdecl (Buffer.contents b) res + | Tstruct fld -> + "struct " ^ struct_union_name Struct fld ^ name_optid id + | Tunion fld -> + "union " ^ struct_union_name Union fld ^ name_optid id + +(* Type *) + +let name_type ty = name_cdecl "" ty + +(* Expressions *) + +let parenthesis_level (Expr (e, ty)) = + match e with + | Econst_int _ -> 0 + | Econst_float _ -> 0 + | Evar _ -> 0 + | Eunop(_, _) -> 30 + | Ederef _ -> 20 + | Eaddrof _ -> 30 + | Ebinop(op, _, _) -> + begin match op with + | Oand | Oor | Oxor -> 75 + | Oeq | One | Olt | Ogt | Ole | Oge -> 70 + | Oadd | Osub | Oshl | Oshr -> 60 + | Omul | Odiv | Omod -> 40 + end + | Ecast _ -> 30 + | Eindex(_, _) -> 20 + | Ecall(_, _) -> 20 + | Eandbool(_, _) -> 80 + | Eorbool(_, _) -> 80 + | Esizeof _ -> 20 + | Efield _ -> 20 + +let rec print_expr p (Expr (eb, ty) as e) = + let level = parenthesis_level e in + match eb with + | Econst_int n -> + fprintf p "%ld" (camlint_of_coqint n) + | Econst_float f -> + fprintf p "%F" f + | Evar id -> + fprintf p "%s" (extern_atom id) + | Eunop(op, e1) -> + fprintf p "%s%a" (name_unop op) print_expr_prec (level, e1) + | Ederef e -> + fprintf p "*%a" print_expr_prec (level, e) + | Eaddrof e -> + fprintf p "&%a" print_expr_prec (level, e) + | Ebinop(op, e1, e2) -> + fprintf p "@[<hov 0>%a@ %s %a@]" + print_expr_prec (level, e1) + (name_binop op) + print_expr_prec (level, e2) + | Ecast(ty, e1) -> + fprintf p "@[<hov 2>(%s)@,%a@]" + (name_type ty) + print_expr_prec (level, e1) + | Eindex(e1, e2) -> + fprintf p "@[<hov 2>%a@,[%a]@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Ecall(e1, el) -> + fprintf p "@[<hov 2>%a@,(@[<hov 0>%a@])@]" + print_expr_prec (level, e1) + print_expr_list (true, el) + | Eandbool(e1, e2) -> + fprintf p "@[<hov 0>%a@ && %a@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Eorbool(e1, e2) -> + fprintf p "@[<hov 0>%a@ || %a@]" + print_expr_prec (level, e1) + print_expr_prec (level, e2) + | Esizeof ty -> + fprintf p "sizeof(%s)" (name_type ty) + | Efield(e1, id) -> + fprintf p "%a.%s" print_expr_prec (level, e1) (extern_atom id) + +and print_expr_prec p (context_prec, e) = + let this_prec = parenthesis_level e in + if this_prec >= context_prec + then fprintf p "(%a)" print_expr e + else print_expr p e + +and print_expr_list p (first, el) = + match el with + | Enil -> () + | Econs(e1, et) -> + if not first then fprintf p ",@ "; + print_expr p e1; + print_expr_list p (false, et) + +let rec print_stmt p s = + match s with + | Sskip -> + fprintf p "/*skip*/;" + | Sexpr e -> + fprintf p "%a;" print_expr e + | Sassign(e1, e2) -> + fprintf p "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2 + | Ssequence(s1, s2) -> + fprintf p "%a@ %a" print_stmt s1 print_stmt s2 + | Sifthenelse(e, s1, Sskip) -> + fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + print_stmt s2 + | Swhile(e, s) -> + fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s + | Sdowhile(e, s) -> + fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]" + print_stmt s + print_expr e + | Sfor(s_init, e, s_iter, s_body) -> + fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]" + print_stmt_for s_init + print_expr e + print_stmt_for s_iter + print_stmt s_body + | Sbreak -> + fprintf p "break;" + | Scontinue -> + fprintf p "continue;" + | Sswitch(e, cases) -> + fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_cases cases + | Sreturn None -> + fprintf p "return;" + | Sreturn (Some e) -> + fprintf p "return %a;" print_expr e + +and print_cases p cases = + match cases with + | LSdefault Sskip -> + () + | LSdefault s -> + fprintf p "@[<v 2>default:@ %a@]" print_stmt s + | LScase(lbl, Sskip, rem) -> + fprintf p "case %ld:@ %a" + (camlint_of_coqint lbl) + print_cases rem + | LScase(lbl, s, rem) -> + fprintf p "@[<v 2>case %ld:@ %a@]@ %a" + (camlint_of_coqint lbl) + print_stmt s + print_cases rem + +and print_stmt_for p s = + match s with + | Sskip -> + fprintf p "/*nothing*/" + | Sexpr e -> + fprintf p "%a" print_expr e + | Sassign(e1, e2) -> + fprintf p "%a = %a" print_expr e1 print_expr e2 + | Ssequence(s1, s2) -> + fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2 + | _ -> + fprintf p "<impossible>" + +let name_function_parameters fun_name params = + let b = Buffer.create 20 in + Buffer.add_string b fun_name; + Buffer.add_char b '('; + let rec add_params first = function + | Coq_nil -> () + | Coq_cons(Coq_pair(id, ty), rem) -> + if not first then Buffer.add_string b ", "; + Buffer.add_string b (name_cdecl (extern_atom id) ty); + add_params false rem in + add_params true params; + Buffer.add_char b ')'; + Buffer.contents b + +let print_function p id f = + fprintf p "%s@ " + (name_cdecl (name_function_parameters (extern_atom id) + f.fn_params) + f.fn_return); + fprintf p "@[<v 2>{@ "; + coqlist_iter + (fun (Coq_pair(id, ty)) -> + fprintf p "%s;@ " (name_cdecl (extern_atom id) ty)) + f.fn_vars; + print_stmt p f.fn_body; + fprintf p "@;<0 -2>}@]@ @ " + +let print_fundef p (Coq_pair(id, fd)) = + match fd with + | External(_, args, res) -> + fprintf p "extern %s;@ " + (name_cdecl (extern_atom id) (Tfunction(args, res))) + | Internal f -> + print_function p id f + +let print_init p = function + | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_int16 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_int32 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_float32 n -> fprintf p "%F,@ " n + | Init_float64 n -> fprintf p "%F,@ " n + | Init_space n -> fprintf p "/* skip %ld*/@ " (camlint_of_coqint n) + +let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = + match init with + | Coq_nil -> + fprintf p "extern %s;@ " + (name_cdecl (extern_atom id) ty) + | Coq_cons(Init_space _, Coq_nil) -> + fprintf p "%s;@ " + (name_cdecl (extern_atom id) ty) + | _ -> + fprintf p "@[<hov 2>%s = {@ " + (name_cdecl (extern_atom id) ty); + coqlist_iter (print_init p) init; + fprintf p "};@]@ " + +(* Collect struct and union types *) + +let rec collect_type = function + | Tvoid -> () + | Tint(sz, sg) -> () + | Tfloat sz -> () + | Tpointer t -> collect_type t + | Tarray(t, n) -> collect_type t + | Tfunction(args, res) -> collect_type_list args; collect_type res + | Tstruct fld -> register_struct_union Struct fld; collect_fields fld + | Tunion fld -> register_struct_union Union fld; collect_fields fld + +and collect_type_list = function + | Tnil -> () + | Tcons(hd, tl) -> collect_type hd; collect_type_list tl + +and collect_fields = function + | Fnil -> () + | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl + +let rec collect_expr (Expr(ed, ty)) = + match ed with + | Econst_int n -> () + | Econst_float f -> () + | Evar id -> () + | Eunop(op, e1) -> collect_expr e1 + | Ederef e -> collect_expr e + | Eaddrof e -> collect_expr e + | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2 + | Ecast(ty, e1) -> collect_type ty; collect_expr e1 + | Eindex(e1, e2) -> collect_expr e1; collect_expr e2 + | Ecall(e1, el) -> collect_expr e1; collect_expr_list el + | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2 + | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2 + | Esizeof ty -> collect_type ty + | Efield(e1, id) -> collect_expr e1 + +and collect_expr_list = function + | Enil -> () + | Econs(hd, tl) -> collect_expr hd; collect_expr_list tl + +let rec collect_stmt = function + | Sskip -> () + | Sexpr e -> collect_expr e + | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 + | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 + | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 + | Swhile(e, s) -> collect_expr e; collect_stmt s + | Sdowhile(e, s) -> collect_stmt s; collect_expr e + | Sfor(s_init, e, s_iter, s_body) -> + collect_stmt s_init; collect_expr e; + collect_stmt s_iter; collect_stmt s_body + | Sbreak -> () + | Scontinue -> () + | Sswitch(e, cases) -> collect_expr e; collect_cases cases + | Sreturn None -> () + | Sreturn (Some e) -> collect_expr e + +and collect_cases = function + | LSdefault s -> collect_stmt s + | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem + +let collect_function f = + collect_type f.fn_return; + coqlist_iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params; + coqlist_iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars; + collect_stmt f.fn_body + +let collect_fundef (Coq_pair(id, fd)) = + match fd with + | External(_, args, res) -> collect_type_list args; collect_type res + | Internal f -> collect_function f + +let collect_globvar (Coq_pair(Coq_pair(id, init), ty)) = + collect_type ty + +let collect_program p = + coqlist_iter collect_globvar p.prog_vars; + coqlist_iter collect_fundef p.prog_funct + +let print_struct_or_union p ((kind, fld), name) = + fprintf p "@[<v 2>%s %s{@ " + (match kind with Struct -> "struct" | Union -> "union") + name; + let rec print_fields = function + | Fnil -> () + | Fcons(id, ty, rem) -> + fprintf p "%s; @ " (name_cdecl (extern_atom id) ty); + print_fields rem in + print_fields fld; + fprintf p "@;<0 -2>}@]@ " + +let print_program p prog = + struct_union_names := []; + struct_union_name_counter := 0; + collect_program prog; + fprintf p "@[<v 0>"; + List.iter (print_struct_or_union p) !struct_union_names; + fprintf p "@ "; + coqlist_iter (print_globvar p) prog.prog_vars; + fprintf p "@ "; + coqlist_iter (print_fundef p) prog.prog_funct; + fprintf p "@]@." + + diff --git a/cil-1.3.5.tar.gz b/cil-1.3.5.tar.gz Binary files differnew file mode 100644 index 0000000..2c19144 --- /dev/null +++ b/cil-1.3.5.tar.gz diff --git a/cil.patch/astslicer.ml.patch b/cil.patch/astslicer.ml.patch new file mode 100644 index 0000000..e8d0195 --- /dev/null +++ b/cil.patch/astslicer.ml.patch @@ -0,0 +1,40 @@ +*** ../cil/src/ext/astslicer.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/ext/astslicer.ml 2006-06-20 17:24:22.000000000 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + (* + * + * Copyright (c) 2001-2002, +*************** +*** 97,103 **** +--- 99,110 ---- + Printf.fprintf out ")\n" ; + incr i + | Switch(_,b,_,_) ++ (* + | Loop(b,_,_,_) ++ *) ++ | While(_,b,_) ++ | DoWhile(_,b,_) ++ | For(_,_,_,b,_) + | Block(b) -> + emit base i st_ht s ; + decr i ; +*************** +*** 371,377 **** +--- 378,389 ---- + doBlock b2 base'' i'' inside ; + incr i + | Switch(_,b,_,_) ++ (* + | Loop(b,_,_,_) ++ *) ++ | While(_,b,_) ++ | DoWhile(_,b,_) ++ | For(_,_,_,b,_) + | Block(b) -> + let inside = check base i default in + mark ws s inside ; diff --git a/cil.patch/cabs2cil.ml.patch b/cil.patch/cabs2cil.ml.patch new file mode 100644 index 0000000..12a81ca --- /dev/null +++ b/cil.patch/cabs2cil.ml.patch @@ -0,0 +1,325 @@ +*** ../cil/src/frontc/cabs2cil.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/frontc/cabs2cil.ml 2006-07-25 10:45:51.136500945 +0200 +*************** +*** 1,3 **** +--- 1,7 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ (* MODIF: Return statement no longer added when the body of the function ++ falls-through. *) ++ + (* + * + * Copyright (c) 2001-2002, +*************** +*** 816,828 **** + (fun s -> + if s.labels != [] then + raise (Failure "cannot duplicate: has labels"); + (match s.skind with +! If _ | Switch _ | Loop _ | Block _ -> + raise (Failure "cannot duplicate: complex stmt") + | Instr il -> + pCount := !pCount + List.length il + | _ -> incr pCount); + if !pCount > 5 then raise (Failure ("cannot duplicate: too many instr")); + (* We can just copy it because there is nothing to share here. + * Except maybe for the ref cell in Goto but it is Ok to share + * that, I think *) +--- 820,835 ---- + (fun s -> + if s.labels != [] then + raise (Failure "cannot duplicate: has labels"); ++ (* + (match s.skind with +! If _ | Switch _ | (*Loop _*) +! While _ | DoWhile _ | For _ | Block _ -> + raise (Failure "cannot duplicate: complex stmt") + | Instr il -> + pCount := !pCount + List.length il + | _ -> incr pCount); + if !pCount > 5 then raise (Failure ("cannot duplicate: too many instr")); ++ *) + (* We can just copy it because there is nothing to share here. + * Except maybe for the ref cell in Goto but it is Ok to share + * that, I think *) +*************** +*** 838,843 **** +--- 845,851 ---- + let canDrop (c: chunk) = + List.for_all canDropStatement c.stmts + ++ (* + let loopChunk (body: chunk) : chunk = + (* Make the statement *) + let loop = mkStmt (Loop (c2block body, !currentLoc, None, None)) in +*************** +*** 845,850 **** +--- 853,885 ---- + postins = []; + cases = body.cases; + } ++ *) ++ ++ let whileChunk (e: exp) (body: chunk) : chunk = ++ let loop = mkStmt (While (e, c2block body, !currentLoc)) in ++ ++ { stmts = [ loop ]; ++ postins = []; ++ cases = body.cases; ++ } ++ ++ let doWhileChunk (e: exp) (body: chunk) : chunk = ++ let loop = mkStmt (DoWhile (e, c2block body, !currentLoc)) in ++ ++ { stmts = [ loop ]; ++ postins = []; ++ cases = body.cases; ++ } ++ ++ let forChunk (bInit: chunk) (e: exp) (bIter: chunk) ++ (body: chunk) : chunk = ++ let loop = mkStmt (For (c2block bInit, e, c2block bIter, ++ c2block body, !currentLoc)) in ++ ++ { stmts = [ loop ]; ++ postins = []; ++ cases = body.cases; ++ } + + let breakChunk (l: location) : chunk = + { stmts = [ mkStmt (Break l) ]; +*************** +*** 959,964 **** +--- 994,1000 ---- + + + (************ Labels ***********) ++ (* + (* Since we turn dowhile and for loops into while we need to take care in + * processing the continue statement. For each loop that we enter we place a + * marker in a list saying what kinds of loop it is. When we see a continue +*************** +*** 971,980 **** +--- 1007,1035 ---- + + let startLoop iswhile = + continues := (if iswhile then While else NotWhile (ref "")) :: !continues ++ *) ++ ++ (* We need to take care while processing the continue statement... ++ * For each loop that we enter we place a marker in a list saying what ++ * chunk of code we must duplicate before each continue statement ++ * in order to preserve the semantics. *) ++ type loopMarker = ++ DuplicateBeforeContinue of chunk ++ ++ let continues : loopMarker list ref = ref [] ++ ++ let startLoop lstate = ++ continues := lstate :: !continues ++ ++ let continueDuplicateChunk (l: location) : chunk = ++ match !continues with ++ | [] -> E.s (error "continue not in a loop") ++ | DuplicateBeforeContinue c :: _ -> c @@ continueChunk l + + (* Sometimes we need to create new label names *) + let newLabelName (base: string) = fst (newAlphaName false "label" base) + ++ (* + let continueOrLabelChunk (l: location) : chunk = + match !continues with + [] -> E.s (error "continue not in a loop") +*************** +*** 990,995 **** +--- 1045,1051 ---- + [] -> E.s (error "labContinue not in a loop") + | While :: rest -> c + | NotWhile lr :: rest -> if !lr = "" then c else consLabel !lr c !currentLoc false ++ *) + + let exitLoop () = + match !continues with +*************** +*** 5465,5473 **** +--- 5521,5534 ---- + * then the switch falls through. *) + blockFallsThrough b || blockCanBreak b + end ++ (* + | Loop (b, _, _, _) -> + (* A loop falls through if it can break. *) + blockCanBreak b ++ *) ++ | While (_, b, _) -> blockCanBreak b ++ | DoWhile (_, b, _) -> blockCanBreak b ++ | For (_, _, _, b, _) -> blockCanBreak b + | Block b -> blockFallsThrough b + | TryFinally (b, h, _) -> blockFallsThrough h + | TryExcept (b, _, h, _) -> true (* Conservative *) +*************** +*** 5512,5518 **** + | Break _ -> true + | If (_, b1, b2, _) -> + blockCanBreak b1 || blockCanBreak b2 +! | Switch _ | Loop _ -> + (* switches and loops catch any breaks in their bodies *) + false + | Block b -> blockCanBreak b +--- 5573,5579 ---- + | Break _ -> true + | If (_, b1, b2, _) -> + blockCanBreak b1 || blockCanBreak b2 +! | Switch _ | (*Loop _*) While _ | DoWhile _ | For _ -> + (* switches and loops catch any breaks in their bodies *) + false + | Block b -> blockCanBreak b +*************** +*** 5522,5527 **** +--- 5583,5589 ---- + List.exists stmtCanBreak b.bstmts + in + if blockFallsThrough !currentFunctionFDEC.sbody then begin ++ (* + let retval = + match unrollType !currentReturnType with + TVoid _ -> None +*************** +*** 5537,5542 **** +--- 5599,5605 ---- + !currentFunctionFDEC.sbody.bstmts <- + !currentFunctionFDEC.sbody.bstmts + @ [mkStmt (Return(retval, endloc))] ++ *) + end; + + (* ignore (E.log "The env after finishing the body of %s:\n%t\n" +*************** +*** 5738,5743 **** +--- 5801,5807 ---- + doCondition false e st' sf' + + | A.WHILE(e,s,loc) -> ++ (* + startLoop true; + let s' = doStatement s in + exitLoop (); +*************** +*** 5746,5753 **** +--- 5810,5836 ---- + loopChunk ((doCondition false e skipChunk + (breakChunk loc')) + @@ s') ++ *) ++ (** We need to convert A.WHILE(e,s) where e may have side effects ++ into Cil.While(e',s') where e' is side-effect free. *) ++ ++ (* Let e == (sCond , eCond) with sCond a sequence of statements ++ and eCond a side-effect free expression. *) ++ let (sCond, eCond, _) = doExp false e (AExp None) in ++ ++ (* Then doStatement(A.WHILE((sCond , eCond), s)) ++ = sCond ; Cil.While(eCond, (doStatement(s) ; sCond)) ++ where doStatement(A.CONTINUE) = (sCond ; Cil.Continue). *) ++ ++ startLoop (DuplicateBeforeContinue sCond); ++ let s' = doStatement s in ++ exitLoop (); ++ let loc' = convLoc loc in ++ currentLoc := loc'; ++ sCond @@ (whileChunk eCond (s' @@ sCond)) + + | A.DOWHILE(e,s,loc) -> ++ (* + startLoop false; + let s' = doStatement s in + let loc' = convLoc loc in +*************** +*** 5757,5764 **** + in + exitLoop (); + loopChunk (s' @@ s'') + +! | A.FOR(fc1,e2,e3,s,loc) -> begin + let loc' = convLoc loc in + currentLoc := loc'; + enterScope (); (* Just in case we have a declaration *) +--- 5840,5866 ---- + in + exitLoop (); + loopChunk (s' @@ s'') ++ *) ++ (** We need to convert A.DOWHILE(e,s) where e may have side effects ++ into Cil.DoWhile(e',s') where e' is side-effect free. *) ++ ++ (* Let e == (sCond , eCond) with sCond a sequence of statements ++ and eCond a side-effect free expression. *) ++ let (sCond, eCond, _) = doExp false e (AExp None) in ++ ++ (* Then doStatement(A.DOWHILE((sCond , eCond), s)) ++ = Cil.DoWhile(eCond, (doStatement(s) ; sCond)) ++ where doStatement(A.CONTINUE) = (sCond ; Cil.Continue). *) ++ ++ startLoop (DuplicateBeforeContinue sCond); ++ let s' = doStatement s in ++ exitLoop (); ++ let loc' = convLoc loc in ++ currentLoc := loc'; ++ doWhileChunk eCond (s' @@ sCond) + +! | A.FOR(fc1,e2,e3,s,loc) -> +! (*begin + let loc' = convLoc loc in + currentLoc := loc'; + enterScope (); (* Just in case we have a declaration *) +*************** +*** 5784,5789 **** +--- 5886,5920 ---- + exitScope (); + res + end ++ *) ++ (** We need to convert A.FOR(e1,e2,e3,s) where e1, e2 and e3 may ++ have side effects into Cil.For(bInit,e2',bIter,s') where e2' ++ is side-effect free. **) ++ ++ (* Let e1 == bInit be a block of statements ++ Let e2 == (bCond , eCond) with bCond a block of statements ++ and eCond a side-effect free expression ++ Let e3 == bIter be a sequence of statements. *) ++ let (bInit, _, _) = match fc1 with ++ | FC_EXP e1 -> doExp false e1 ADrop ++ | FC_DECL d1 -> (doDecl false d1, zero, voidType) in ++ let (bCond, eCond, _) = doExp false e2 (AExp None) in ++ let eCond' = match eCond with ++ | Const(CStr "exp_nothing") -> Cil.one ++ | _ -> eCond in ++ let (bIter, _, _) = doExp false e3 ADrop in ++ ++ (* Then doStatement(A.FOR(bInit, (bCond , eCond), bIter, s)) ++ = Cil.For({bInit; bCond}, eCond', bIter, {doStatement(s); bCond}) ++ where doStatement(A.CONTINUE) = (bCond ; Cil.Continue). *) ++ ++ startLoop (DuplicateBeforeContinue bCond); ++ let s' = doStatement s in ++ exitLoop (); ++ let loc' = convLoc loc in ++ currentLoc := loc'; ++ (forChunk (bInit @@ bCond) eCond' bIter (s' @@ bCond)) ++ + | A.BREAK loc -> + let loc' = convLoc loc in + currentLoc := loc'; +*************** +*** 5792,5798 **** +--- 5923,5932 ---- + | A.CONTINUE loc -> + let loc' = convLoc loc in + currentLoc := loc'; ++ (* + continueOrLabelChunk loc' ++ *) ++ continueDuplicateChunk loc' + + | A.RETURN (A.NOTHING, loc) -> + let loc' = convLoc loc in diff --git a/cil.patch/cfg.ml.patch b/cil.patch/cfg.ml.patch new file mode 100644 index 0000000..9629d46 --- /dev/null +++ b/cil.patch/cfg.ml.patch @@ -0,0 +1,55 @@ +*** ../cil/src/ext/cfg.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/ext/cfg.ml 2006-06-20 17:42:04.000000000 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + (* + * + * Copyright (c) 2001-2003, +*************** +*** 156,162 **** +--- 158,169 ---- + then + addOptionSucc next; + cfgBlock blk next next cont ++ (* + | Loop(blk,_,_,_) -> ++ *) ++ | While(_,blk,_) ++ | DoWhile(_,blk,_) ++ | For(_,_,_,blk,_) -> + addBlockSucc blk; + cfgBlock blk (Some s) next (Some s) + (* Since all loops have terminating condition true, we don't put +*************** +*** 184,190 **** +--- 191,202 ---- + | Block b -> fasBlock todo b + | If (_, tb, fb, _) -> (fasBlock todo tb; fasBlock todo fb) + | Switch (_, b, _, _) -> fasBlock todo b ++ (* + | Loop (b, _, _, _) -> fasBlock todo b ++ *) ++ | While (_, b, _) -> fasBlock todo b ++ | DoWhile (_, b, _) -> fasBlock todo b ++ | For (_, _, _, b, _) -> fasBlock todo b + | (Return _ | Break _ | Continue _ | Goto _ | Instr _) -> () + | TryExcept _ | TryFinally _ -> E.s (E.unimp "try/except/finally") + end +*************** +*** 201,207 **** +--- 213,224 ---- + begin + match s.skind with + | If (e, _, _, _) -> "if" (*sprint ~width:999 (dprintf "if %a" d_exp e)*) ++ (* + | Loop _ -> "loop" ++ *) ++ | While _ -> "while" ++ | DoWhile _ -> "dowhile" ++ | For _ -> "for" + | Break _ -> "break" + | Continue _ -> "continue" + | Goto _ -> "goto" diff --git a/cil.patch/check.ml.patch b/cil.patch/check.ml.patch new file mode 100644 index 0000000..7fe183f --- /dev/null +++ b/cil.patch/check.ml.patch @@ -0,0 +1,56 @@ +*** ../cil/src/check.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/check.ml 2006-06-21 11:13:35.000000000 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + (* + * + * Copyright (c) 2001-2002, +*************** +*** 661,667 **** + (fun _ -> + (* Print context only for certain small statements *) + match s.skind with +! Loop _ | If _ | Switch _ -> nil + | _ -> dprintf "checkStmt: %a" d_stmt s) + (fun _ -> + (* Check the labels *) +--- 663,669 ---- + (fun _ -> + (* Print context only for certain small statements *) + match s.skind with +! (*Loop _*) While _ | DoWhile _ | For _ | If _ | Switch _ -> nil + | _ -> dprintf "checkStmt: %a" d_stmt s) + (fun _ -> + (* Check the labels *) +*************** +*** 704,710 **** +--- 706,731 ---- + | None, _ -> ignore (warn "Invalid return value") + | Some re', rt' -> checkExpType false re' rt' + end ++ (* + | Loop (b, l, _, _) -> checkBlock b ++ *) ++ | While (e, b, l) -> ++ currentLoc := l; ++ let te = checkExp false e in ++ checkBooleanType te; ++ checkBlock b; ++ | DoWhile (e, b, l) -> ++ currentLoc := l; ++ let te = checkExp false e in ++ checkBooleanType te; ++ checkBlock b; ++ | For (bInit, e, bIter, b, l) -> ++ currentLoc := l; ++ checkBlock bInit; ++ let te = checkExp false e in ++ checkBooleanType te; ++ checkBlock bIter; ++ checkBlock b; + | Block b -> checkBlock b + | If (e, bt, bf, l) -> + currentLoc := l; diff --git a/cil.patch/cil.ml.patch b/cil.patch/cil.ml.patch new file mode 100644 index 0000000..a49b73d --- /dev/null +++ b/cil.patch/cil.ml.patch @@ -0,0 +1,381 @@ +*** ../cil/src/cil.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/cil.ml 2006-07-25 10:57:30.686790845 +0200 +*************** +*** 1,3 **** +--- 1,6 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ (* MODIF: useLogicalOperators flag set to true by default. *) ++ + (* + * + * Copyright (c) 2001-2003, +*************** +*** 63,69 **** + * print output for the MS VC + * compiler. Default is GCC *) + +! let useLogicalOperators = ref false + + + module M = Machdep +--- 66,72 ---- + * print output for the MS VC + * compiler. Default is GCC *) + +! let useLogicalOperators = ref (*false*) true + + + module M = Machdep +*************** +*** 684,692 **** + | Goto of stmt ref * location (** A goto statement. Appears from + actual goto's in the code. *) + | Break of location (** A break to the end of the nearest +! enclosing Loop or Switch *) + | Continue of location (** A continue to the start of the +! nearest enclosing [Loop] *) + | If of exp * block * block * location (** A conditional. + Two successors, the "then" and + the "else" branches. Both +--- 687,695 ---- + | Goto of stmt ref * location (** A goto statement. Appears from + actual goto's in the code. *) + | Break of location (** A break to the end of the nearest +! enclosing loop or Switch *) + | Continue of location (** A continue to the start of the +! nearest enclosing loop *) + | If of exp * block * block * location (** A conditional. + Two successors, the "then" and + the "else" branches. Both +*************** +*** 701,706 **** +--- 704,710 ---- + you can get from the labels of the + statement *) + ++ (* + | Loop of block * location * (stmt option) * (stmt option) + (** A [while(1)] loop. The + * termination test is implemented +*************** +*** 713,718 **** +--- 717,726 ---- + * and the second will point to + * the stmt containing the break + * label for this loop. *) ++ *) ++ | While of exp * block * location (** A while loop. *) ++ | DoWhile of exp * block * location (** A do...while loop. *) ++ | For of block * exp * block * block * location (** A for loop. *) + + | Block of block (** Just a block of statements. Use it + as a way to keep some attributes +*************** +*** 1040,1046 **** +--- 1048,1059 ---- + | Continue(loc) -> loc + | If(_, _, _, loc) -> loc + | Switch (_, _, _, loc) -> loc ++ (* + | Loop (_, loc, _, _) -> loc ++ *) ++ | While (_, _, loc) -> loc ++ | DoWhile (_, _, loc) -> loc ++ | For (_, _, _, _, loc) -> loc + | Block b -> if b.bstmts == [] then lu + else get_stmtLoc ((List.hd b.bstmts).skind) + | TryFinally (_, _, l) -> l +*************** +*** 1524,1533 **** +--- 1537,1549 ---- + + let mkWhile ~(guard:exp) ~(body: stmt list) : stmt list = + (* Do it like this so that the pretty printer recognizes it *) ++ (* + [ mkStmt (Loop (mkBlock (mkStmt (If(guard, + mkBlock [ mkEmptyStmt () ], + mkBlock [ mkStmt (Break lu)], lu)) :: + body), lu, None, None)) ] ++ *) ++ [ mkStmt (While (guard, mkBlock body, lu)) ] + + + +*************** +*** 3448,3453 **** +--- 3464,3471 ---- + ++ self#pExp () e + ++ text ") " + ++ self#pBlock () b) ++ ++ (* + | Loop(b, l, _, _) -> begin + (* Maybe the first thing is a conditional. Turn it into a WHILE *) + try +*************** +*** 3484,3489 **** +--- 3502,3540 ---- + ++ text "ile (1) " + ++ self#pBlock () b) + end ++ *) ++ ++ | While (e, b, l) -> ++ self#pLineDirective l ++ ++ (align ++ ++ text "while (" ++ ++ self#pExp () e ++ ++ text ") " ++ ++ self#pBlock () b) ++ ++ | DoWhile (e, b, l) -> ++ self#pLineDirective l ++ ++ (align ++ ++ text "do " ++ ++ self#pBlock () b ++ ++ text " while (" ++ ++ self#pExp () e ++ ++ text ");") ++ ++ | For (bInit, e, bIter, b, l) -> ++ ignore (E.warn ++ "in for loops, the 1st and 3rd expressions are not printed"); ++ self#pLineDirective l ++ ++ (align ++ ++ text "for (" ++ ++ text "/* ??? */" (* self#pBlock () bInit *) ++ ++ text "; " ++ ++ self#pExp () e ++ ++ text "; " ++ ++ text "/* ??? */" (* self#pBlock() bIter *) ++ ++ text ") " ++ ++ self#pBlock () b) ++ + | Block b -> align ++ self#pBlock () b + + | TryFinally (b, h, l) -> +*************** +*** 4705,4713 **** +--- 4756,4781 ---- + | Return (Some e, l) -> + let e' = fExp e in + if e' != e then Return (Some e', l) else s.skind ++ (* + | Loop (b, l, s1, s2) -> + let b' = fBlock b in + if b' != b then Loop (b', l, s1, s2) else s.skind ++ *) ++ | While (e, b, l) -> ++ let e' = fExp e in ++ let b' = fBlock b in ++ if e' != e || b' != b then While (e', b', l) else s.skind ++ | DoWhile (e, b, l) -> ++ let b' = fBlock b in ++ let e' = fExp e in ++ if e' != e || b' != b then DoWhile (e', b', l) else s.skind ++ | For (bInit, e, bIter, b, l) -> ++ let bInit' = fBlock bInit in ++ let e' = fExp e in ++ let bIter' = fBlock bIter in ++ let b' = fBlock b in ++ if bInit' != bInit || e' != e || bIter' != bIter || b' != b then ++ For (bInit', e', bIter', b', l) else s.skind + | If(e, s1, s2, l) -> + let e' = fExp e in + (*if e queued any instructions, pop them here and remember them so that +*************** +*** 5180,5186 **** +--- 5248,5262 ---- + peepHole1 doone tb.bstmts; + peepHole1 doone eb.bstmts + | Switch (e, b, _, _) -> peepHole1 doone b.bstmts ++ (* + | Loop (b, l, _, _) -> peepHole1 doone b.bstmts ++ *) ++ | While (_, b, _) -> peepHole1 doone b.bstmts ++ | DoWhile (_, b, _) -> peepHole1 doone b.bstmts ++ | For (bInit, _, bIter, b, _) -> ++ peepHole1 doone bInit.bstmts; ++ peepHole1 doone bIter.bstmts; ++ peepHole1 doone b.bstmts + | Block b -> peepHole1 doone b.bstmts + | TryFinally (b, h, l) -> + peepHole1 doone b.bstmts; +*************** +*** 5214,5220 **** +--- 5290,5304 ---- + peepHole2 dotwo tb.bstmts; + peepHole2 dotwo eb.bstmts + | Switch (e, b, _, _) -> peepHole2 dotwo b.bstmts ++ (* + | Loop (b, l, _, _) -> peepHole2 dotwo b.bstmts ++ *) ++ | While (_, b, _) -> peepHole2 dotwo b.bstmts ++ | DoWhile (_, b, _) -> peepHole2 dotwo b.bstmts ++ | For (bInit, _, bIter, b, _) -> ++ peepHole2 dotwo bInit.bstmts; ++ peepHole2 dotwo bIter.bstmts; ++ peepHole2 dotwo b.bstmts + | Block b -> peepHole2 dotwo b.bstmts + | TryFinally (b, h, l) -> peepHole2 dotwo b.bstmts; + peepHole2 dotwo h.bstmts +*************** +*** 5887,5892 **** +--- 5971,5977 ---- + [] -> trylink s fallthrough + | hd :: tl -> (link s hd ; succpred_block b2 fallthrough )) + ++ (* + | Loop(b,l,_,_) -> + begin match b.bstmts with + [] -> failwith "computeCFGInfo: empty loop" +*************** +*** 5894,5899 **** +--- 5979,6011 ---- + link s hd ; + succpred_block b (Some(hd)) + end ++ *) ++ ++ | While (e, b, l) -> begin match b.bstmts with ++ | [] -> failwith "computeCFGInfo: empty loop" ++ | hd :: tl -> link s hd ; ++ succpred_block b (Some(hd)) ++ end ++ ++ | DoWhile (e, b, l) ->begin match b.bstmts with ++ | [] -> failwith "computeCFGInfo: empty loop" ++ | hd :: tl -> link s hd ; ++ succpred_block b (Some(hd)) ++ end ++ ++ | For (bInit, e, bIter, b, l) -> ++ (match bInit.bstmts with ++ | [] -> failwith "computeCFGInfo: empty loop" ++ | hd :: tl -> link s hd ; ++ succpred_block bInit (Some(hd))) ; ++ (match bIter.bstmts with ++ | [] -> failwith "computeCFGInfo: empty loop" ++ | hd :: tl -> link s hd ; ++ succpred_block bIter (Some(hd))) ; ++ (match b.bstmts with ++ | [] -> failwith "computeCFGInfo: empty loop" ++ | hd :: tl -> link s hd ; ++ succpred_block b (Some(hd))) ; + + | Block(b) -> begin match b.bstmts with + [] -> trylink s fallthrough +*************** +*** 5985,5991 **** + let i = get_switch_count () in + let break_stmt = mkStmt (Instr []) in + break_stmt.labels <- +! [Label((Printf.sprintf "switch_%d_break" i),l,false)] ; + let break_block = mkBlock [ break_stmt ] in + let body_block = b in + let body_if_stmtkind = (If(zero,body_block,break_block,l)) in +--- 6097,6103 ---- + let i = get_switch_count () in + let break_stmt = mkStmt (Instr []) in + break_stmt.labels <- +! [Label((Printf.sprintf "switch_%d_break" i),l,false)] ; + let break_block = mkBlock [ break_stmt ] in + let body_block = b in + let body_if_stmtkind = (If(zero,body_block,break_block,l)) in +*************** +*** 6026,6039 **** + s.skind <- handle_choices (List.sort compare_choices sl) ; + xform_switch_block b (fun () -> ref break_stmt) cont_dest i + end + | Loop(b,l,_,_) -> + let i = get_switch_count () in + let break_stmt = mkStmt (Instr []) in + break_stmt.labels <- +! [Label((Printf.sprintf "while_%d_break" i),l,false)] ; + let cont_stmt = mkStmt (Instr []) in + cont_stmt.labels <- +! [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; + b.bstmts <- cont_stmt :: b.bstmts ; + let this_stmt = mkStmt + (Loop(b,l,Some(cont_stmt),Some(break_stmt))) in +--- 6138,6152 ---- + s.skind <- handle_choices (List.sort compare_choices sl) ; + xform_switch_block b (fun () -> ref break_stmt) cont_dest i + end ++ (* + | Loop(b,l,_,_) -> + let i = get_switch_count () in + let break_stmt = mkStmt (Instr []) in + break_stmt.labels <- +! [Label((Printf.sprintf "while_%d_break" i),l,false)] ; + let cont_stmt = mkStmt (Instr []) in + cont_stmt.labels <- +! [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; + b.bstmts <- cont_stmt :: b.bstmts ; + let this_stmt = mkStmt + (Loop(b,l,Some(cont_stmt),Some(break_stmt))) in +*************** +*** 6043,6048 **** +--- 6156,6217 ---- + break_stmt.succs <- s.succs ; + let new_block = mkBlock [ this_stmt ; break_stmt ] in + s.skind <- Block new_block ++ *) ++ | While (e, b, l) -> ++ let i = get_switch_count () in ++ let break_stmt = mkStmt (Instr []) in ++ break_stmt.labels <- ++ [Label((Printf.sprintf "while_%d_break" i),l,false)] ; ++ let cont_stmt = mkStmt (Instr []) in ++ cont_stmt.labels <- ++ [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; ++ b.bstmts <- cont_stmt :: b.bstmts ; ++ let this_stmt = mkStmt ++ (While(e,b,l)) in ++ let break_dest () = ref break_stmt in ++ let cont_dest () = ref cont_stmt in ++ xform_switch_block b break_dest cont_dest label_index ; ++ break_stmt.succs <- s.succs ; ++ let new_block = mkBlock [ this_stmt ; break_stmt ] in ++ s.skind <- Block new_block ++ ++ | DoWhile (e, b, l) -> ++ let i = get_switch_count () in ++ let break_stmt = mkStmt (Instr []) in ++ break_stmt.labels <- ++ [Label((Printf.sprintf "while_%d_break" i),l,false)] ; ++ let cont_stmt = mkStmt (Instr []) in ++ cont_stmt.labels <- ++ [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; ++ b.bstmts <- cont_stmt :: b.bstmts ; ++ let this_stmt = mkStmt ++ (DoWhile(e,b,l)) in ++ let break_dest () = ref break_stmt in ++ let cont_dest () = ref cont_stmt in ++ xform_switch_block b break_dest cont_dest label_index ; ++ break_stmt.succs <- s.succs ; ++ let new_block = mkBlock [ this_stmt ; break_stmt ] in ++ s.skind <- Block new_block ++ ++ | For (bInit, e, bIter , b, l) -> ++ let i = get_switch_count () in ++ let break_stmt = mkStmt (Instr []) in ++ break_stmt.labels <- ++ [Label((Printf.sprintf "while_%d_break" i),l,false)] ; ++ let cont_stmt = mkStmt (Instr []) in ++ cont_stmt.labels <- ++ [Label((Printf.sprintf "while_%d_continue" i),l,false)] ; ++ b.bstmts <- cont_stmt :: b.bstmts ; ++ let this_stmt = mkStmt ++ (For(bInit,e,bIter,b,l)) in ++ let break_dest () = ref break_stmt in ++ let cont_dest () = ref cont_stmt in ++ xform_switch_block b break_dest cont_dest label_index ; ++ break_stmt.succs <- s.succs ; ++ let new_block = mkBlock [ this_stmt ; break_stmt ] in ++ s.skind <- Block new_block ++ ++ + | Block(b) -> xform_switch_block b break_dest cont_dest label_index + + | TryExcept _ | TryFinally _ -> diff --git a/cil.patch/cil.mli.patch b/cil.patch/cil.mli.patch new file mode 100644 index 0000000..d0e0363 --- /dev/null +++ b/cil.patch/cil.mli.patch @@ -0,0 +1,59 @@ +*** ../cil/src/cil.mli 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/cil.mli 2006-06-21 10:56:23.555126082 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + (* + * + * Copyright (c) 2001-2002, +*************** +*** 918,927 **** + * statement. The target statement MUST have at least a label. *) + + | Break of location +! (** A break to the end of the nearest enclosing Loop or Switch *) + + | Continue of location +! (** A continue to the start of the nearest enclosing [Loop] *) + | If of exp * block * block * location + (** A conditional. Two successors, the "then" and the "else" branches. + * Both branches fall-through to the successor of the If statement. *) +--- 920,929 ---- + * statement. The target statement MUST have at least a label. *) + + | Break of location +! (** A break to the end of the nearest enclosing loop or Switch *) + + | Continue of location +! (** A continue to the start of the nearest enclosing loop *) + | If of exp * block * block * location + (** A conditional. Two successors, the "then" and the "else" branches. + * Both branches fall-through to the successor of the If statement. *) +*************** +*** 932,943 **** +--- 934,956 ---- + * among its labels what cases it implements. The statements that + * implement the cases are somewhere within the provided [block]. *) + ++ (* + | Loop of block * location * (stmt option) * (stmt option) + (** A [while(1)] loop. The termination test is implemented in the body of + * a loop using a [Break] statement. If prepareCFG has been called, + * the first stmt option will point to the stmt containing the continue + * label for this loop and the second will point to the stmt containing + * the break label for this loop. *) ++ *) ++ ++ | While of exp * block * location ++ (** A [while] loop. *) ++ ++ | DoWhile of exp * block * location ++ (** A [do...while] loop. *) ++ ++ | For of block * exp * block * block * location ++ (** A [for] loop. *) + + | Block of block + (** Just a block of statements. Use it as a way to keep some block diff --git a/cil.patch/dataflow.ml.patch b/cil.patch/dataflow.ml.patch new file mode 100644 index 0000000..87b00de --- /dev/null +++ b/cil.patch/dataflow.ml.patch @@ -0,0 +1,27 @@ +*** ../cil/src/ext/dataflow.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/ext/dataflow.ml 2006-06-20 17:28:35.000000000 +0200 +*************** +*** 1,3 **** +--- 1,4 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) + + module IH = Inthash + module E = Errormsg +*************** +*** 219,225 **** + + | Goto _ | Break _ | Continue _ | If _ + | TryExcept _ | TryFinally _ +! | Switch _ | Loop _ | Return _ | Block _ -> curr + in + currentLoc := get_stmtLoc s.skind; + +--- 220,227 ---- + + | Goto _ | Break _ | Continue _ | If _ + | TryExcept _ | TryFinally _ +! | Switch _ | (*Loop _*) While _ | DoWhile _ | For _ +! | Return _ | Block _ -> curr + in + currentLoc := get_stmtLoc s.skind; + diff --git a/cil.patch/dataslicing.ml.patch b/cil.patch/dataslicing.ml.patch new file mode 100644 index 0000000..cebf2e3 --- /dev/null +++ b/cil.patch/dataslicing.ml.patch @@ -0,0 +1,28 @@ +*** ../cil/src/ext/dataslicing.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/ext/dataslicing.ml 2006-06-21 11:14:58.866051623 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + (* + * + * Copyright (c) 2004, +*************** +*** 357,365 **** +--- 359,373 ---- + | 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") + diff --git a/cil.patch/formatparse.mly.patch b/cil.patch/formatparse.mly.patch new file mode 100644 index 0000000..09e161b --- /dev/null +++ b/cil.patch/formatparse.mly.patch @@ -0,0 +1,40 @@ +*** ../cil/src/formatparse.mly 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/formatparse.mly 2006-06-20 16:22:57.000000000 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ /* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. */ ++ + /*(* Parser for constructing CIL from format strings *) + (* + * +*************** +*** 1352,1357 **** +--- 1354,1360 ---- + mkCast e !upointType + else e + in ++ (* + mkStmt + (Loop (mkBlock [ mkStmt + (If(e, +*************** +*** 1360,1366 **** + (Break loc) ], + loc)); + $5 mkTemp loc args ], +! loc, None, None))) + } + | instr_list { (fun mkTemp loc args -> + mkStmt (Instr ($1 loc args))) +--- 1363,1372 ---- + (Break loc) ], + loc)); + $5 mkTemp loc args ], +! loc, None, None)) +! *) +! mkStmt +! (While (e, mkBlock [ $5 mkTemp loc args ], loc))) + } + | instr_list { (fun mkTemp loc args -> + mkStmt (Instr ($1 loc args))) diff --git a/cil.patch/mergecil.ml.patch b/cil.patch/mergecil.ml.patch new file mode 100644 index 0000000..cc976ec --- /dev/null +++ b/cil.patch/mergecil.ml.patch @@ -0,0 +1,25 @@ +*** ../cil/src/mergecil.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/mergecil.ml 2006-06-20 17:20:05.000000000 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + (* + * + * Copyright (c) 2001-2002, +*************** +*** 1151,1157 **** +--- 1153,1164 ---- + + 41*(stmtListSum b2.bstmts) + | Switch(_,b,_,_) -> 43 + 47*(stmtListSum b.bstmts) + (* don't look at stmt list b/c is not part of tree *) ++ (* + | Loop(b,_,_,_) -> 49 + 53*(stmtListSum b.bstmts) ++ *) ++ | While(_,b,_) -> 49 + 53*(stmtListSum b.bstmts) ++ | DoWhile(_,b,_) -> 49 + 53*(stmtListSum b.bstmts) ++ | For(_,_,_,b,_) -> 49 + 53*(stmtListSum b.bstmts) + | Block(b) -> 59 + 61*(stmtListSum b.bstmts) + | TryExcept (b, (il, e), h, _) -> + 67 + 83*(stmtListSum b.bstmts) + 97*(stmtListSum h.bstmts) diff --git a/cil.patch/oneret.ml.patch b/cil.patch/oneret.ml.patch new file mode 100644 index 0000000..d4c13d5 --- /dev/null +++ b/cil.patch/oneret.ml.patch @@ -0,0 +1,38 @@ +*** ../cil/src/ext/oneret.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/ext/oneret.ml 2006-06-21 11:15:54.000000000 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + (* + * + * Copyright (c) 2001-2002, +*************** +*** 133,142 **** +--- 135,159 ---- + currentLoc := l; + s.skind <- If(eb, scanBlock false t, scanBlock false e, l); + s :: scanStmts mainbody rests ++ (* + | ({skind=Loop(b,l,lb1,lb2)} as s) :: rests -> + currentLoc := l; + s.skind <- Loop(scanBlock false b, l,lb1,lb2); + s :: scanStmts mainbody rests ++ *) ++ | ({skind=While(e,b,l)} as s) :: rests -> ++ currentLoc := l; ++ s.skind <- While(e, scanBlock false b, l); ++ s :: scanStmts mainbody rests ++ | ({skind=DoWhile(e,b,l)} as s) :: rests -> ++ currentLoc := l; ++ s.skind <- DoWhile(e, scanBlock false b, l); ++ s :: scanStmts mainbody rests ++ | ({skind=For(bInit,e,bIter,b,l)} as s) :: rests -> ++ currentLoc := l; ++ s.skind <- For(scanBlock false bInit, e, scanBlock false bIter, ++ scanBlock false b, l); ++ s :: scanStmts mainbody rests + | ({skind=Switch(e, b, cases, l)} as s) :: rests -> + currentLoc := l; + s.skind <- Switch(e, scanBlock false b, cases, l); diff --git a/cil.patch/ptranal.ml.patch b/cil.patch/ptranal.ml.patch new file mode 100644 index 0000000..8b5cf9f --- /dev/null +++ b/cil.patch/ptranal.ml.patch @@ -0,0 +1,28 @@ +*** ../cil/src/ext/pta/ptranal.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/ext/pta/ptranal.ml 2006-06-21 11:55:25.414890423 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + (* + * + * Copyright (c) 2001-2002, +*************** +*** 312,318 **** +--- 314,328 ---- + | Switch (e, b, sl, l) -> + analyze_block b; + List.iter analyze_stmt sl ++ (* + | Loop (b, l, _, _) -> analyze_block b ++ *) ++ | While (_, b, _) -> analyze_block b ++ | DoWhile (_, b, _) -> analyze_block b ++ | For (bInit, _, bIter, b, _) -> ++ analyze_block bInit; ++ analyze_block bIter; ++ analyze_block b + | Block b -> analyze_block b + | TryFinally (b, h, _) -> + analyze_block b; diff --git a/cil.patch/usedef.ml.patch b/cil.patch/usedef.ml.patch new file mode 100644 index 0000000..d075316 --- /dev/null +++ b/cil.patch/usedef.ml.patch @@ -0,0 +1,38 @@ +*** ../cil/src/ext/usedef.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/ext/usedef.ml 2006-06-20 17:36:16.000000000 +0200 +*************** +*** 1,3 **** +--- 1,5 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ + + open Cil + open Pretty +*************** +*** 130,136 **** +--- 132,141 ---- + | Return (Some e, _) -> ve e + | If (e, _, _, _) -> ve e + | Break _ | Goto _ | Continue _ -> () ++ (* + | Loop (_, _, _, _) -> () ++ *) ++ | While _ | DoWhile _ | For _ -> () + | Switch (e, _, _, _) -> ve e + | Instr il -> + List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il +*************** +*** 165,171 **** +--- 170,181 ---- + let u'', d'' = handle_block fb in + (VS.union (VS.union u u') u'', VS.union (VS.union d d') d'') + | Break _ | Goto _ | Continue _ -> !varUsed, !varDefs ++ (* + | Loop (b, _, _, _) -> handle_block b ++ *) ++ | While (_, b, _) -> handle_block b ++ | DoWhile (_, b, _) -> handle_block b ++ | For (_, _, _, b, _) -> handle_block b + | Switch (e, b, _, _) -> + let _ = ve e in + let u, d = !varUsed, !varDefs in diff --git a/extraction/.depend b/extraction/.depend index e18eef8..aa7e42a 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -8,6 +8,10 @@ BinInt.cmi ../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CList.cmx BinPos.cmx \ BinInt.cmx +../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ + CList.cmi BinInt.cmi AST.cmi +../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ + CList.cmx BinInt.cmx AST.cmx ../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \ ../caml/CMlexer.cmi ../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \ @@ -30,10 +34,20 @@ ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx ../caml/Coloringaux.cmi ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx -../caml/Main2.cmo: ../caml/PrintPPC.cmi Main.cmi Datatypes.cmi \ - ../caml/CMtypecheck.cmi ../caml/CMparser.cmi ../caml/CMlexer.cmi -../caml/Main2.cmx: ../caml/PrintPPC.cmx Main.cmx Datatypes.cmx \ - ../caml/CMtypecheck.cmx ../caml/CMparser.cmx ../caml/CMlexer.cmx +../caml/Main2.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \ + Datatypes.cmi Csyntax.cmi ../caml/Cil2Csyntax.cmo ../caml/CMtypecheck.cmi \ + ../caml/CMparser.cmi ../caml/CMlexer.cmi +../caml/Main2.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \ + Datatypes.cmx Csyntax.cmx ../caml/Cil2Csyntax.cmx ../caml/CMtypecheck.cmx \ + ../caml/CMparser.cmx ../caml/CMlexer.cmx +../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \ + ../caml/Camlcoq.cmo CList.cmi AST.cmi +../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \ + ../caml/Camlcoq.cmx CList.cmx AST.cmx +../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ + CList.cmi AST.cmi +../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ + CList.cmx AST.cmx ../caml/PrintPPC.cmo: PPC.cmi Datatypes.cmi ../caml/Camlcoq.cmo CList.cmi \ AST.cmi ../caml/PrintPPC.cmi ../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \ @@ -76,11 +90,11 @@ CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ Csharpminor.cmi: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi -cshmgen.cmi: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi csyntax.cmi \ +Cshmgen.cmi: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi Csyntax.cmi \ Csharpminor.cmi CList.cmi AST.cmi -csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \ +Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \ Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi csyntax.cmi Coqlib.cmi \ +Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \ CList.cmi AST.cmi Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi \ @@ -113,7 +127,7 @@ Mach.cmi: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi \ Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Main.cmi: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ - Linearize.cmi Datatypes.cmi ctyping.cmi csyntax.cmi cshmgen.cmi \ + Linearize.cmi Datatypes.cmi Ctyping.cmi Csyntax.cmi Cshmgen.cmi \ Constprop.cmi Cminorgen.cmi Cminor.cmi CSE.cmi Allocation.cmi AST.cmi Maps.cmi: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \ BinInt.cmi @@ -227,18 +241,18 @@ Csharpminor.cmo: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ Csharpminor.cmx: Zmax.cmx Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx \ Globalenvs.cmx Floats.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx \ AST.cmx Csharpminor.cmi -cshmgen.cmo: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi csyntax.cmi \ - Csharpminor.cmi CList.cmi AST.cmi cshmgen.cmi -cshmgen.cmx: Peano.cmx Integers.cmx Floats.cmx Datatypes.cmx csyntax.cmx \ - Csharpminor.cmx CList.cmx AST.cmx cshmgen.cmi -csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \ - Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi csyntax.cmi -csyntax.cmx: Zmax.cmx Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx \ - Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx csyntax.cmi -ctyping.cmo: Specif.cmi Maps.cmi Datatypes.cmi csyntax.cmi Coqlib.cmi \ - CList.cmi AST.cmi ctyping.cmi -ctyping.cmx: Specif.cmx Maps.cmx Datatypes.cmx csyntax.cmx Coqlib.cmx \ - CList.cmx AST.cmx ctyping.cmi +Cshmgen.cmo: Peano.cmi Integers.cmi Floats.cmi Datatypes.cmi Csyntax.cmi \ + Csharpminor.cmi CList.cmi AST.cmi Cshmgen.cmi +Cshmgen.cmx: Peano.cmx Integers.cmx Floats.cmx Datatypes.cmx Csyntax.cmx \ + Csharpminor.cmx CList.cmx AST.cmx Cshmgen.cmi +Csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \ + Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Csyntax.cmi +Csyntax.cmx: Zmax.cmx Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx \ + Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Csyntax.cmi +Ctyping.cmo: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \ + CList.cmi AST.cmi Ctyping.cmi +Ctyping.cmx: Specif.cmx Maps.cmx Datatypes.cmx Csyntax.cmx Coqlib.cmx \ + CList.cmx AST.cmx Ctyping.cmi Datatypes.cmo: Datatypes.cmi Datatypes.cmx: Datatypes.cmi Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \ @@ -312,11 +326,11 @@ Mach.cmx: Zmax.cmx Zdiv.cmx Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx \ Locations.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx Coqlib.cmx \ CList.cmx BinPos.cmx BinInt.cmx AST.cmx Mach.cmi Main.cmo: Tunneling.cmi Stacking.cmi RTLgen.cmi PPCgen.cmi PPC.cmi \ - Linearize.cmi Datatypes.cmi ctyping.cmi csyntax.cmi cshmgen.cmi \ + Linearize.cmi Datatypes.cmi Ctyping.cmi Csyntax.cmi Cshmgen.cmi \ Constprop.cmi Cminorgen.cmi Cminor.cmi CSE.cmi Allocation.cmi AST.cmi \ Main.cmi Main.cmx: Tunneling.cmx Stacking.cmx RTLgen.cmx PPCgen.cmx PPC.cmx \ - Linearize.cmx Datatypes.cmx ctyping.cmx csyntax.cmx cshmgen.cmx \ + Linearize.cmx Datatypes.cmx Ctyping.cmx Csyntax.cmx Cshmgen.cmx \ Constprop.cmx Cminorgen.cmx Cminor.cmx CSE.cmx Allocation.cmx AST.cmx \ Main.cmi Maps.cmo: Specif.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinNat.cmi \ diff --git a/extraction/Makefile b/extraction/Makefile index 72bf244..e4dcdbe 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -6,10 +6,9 @@ FILES=\ Coqlib.ml Maps.ml Sets.ml AST.ml Iteration.ml Integers.ml \ ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.ml Values.ml \ Mem.ml Globalenvs.ml \ - csyntax.ml ctyping.ml \ - cshmgen.ml \ + Csyntax.ml Ctyping.ml Csharpminor.ml Cshmgen.ml \ Op.ml Cminor.ml Cmconstr.ml \ - Csharpminor.ml Cminorgen.ml \ + Cminorgen.ml \ Registers.ml RTL.ml \ ../caml/RTLgenaux.ml RTLgen.ml \ Locations.ml Conventions.ml \ @@ -23,27 +22,30 @@ FILES=\ Mach.ml Stacking.ml \ PPC.ml PPCgen.ml \ Main.ml \ + ../caml/Cil2Csyntax.ml \ ../caml/CMparser.ml ../caml/CMlexer.ml ../caml/CMtypecheck.ml \ - ../caml/PrintPPC.ml ../caml/Main2.ml + ../caml/PrintCsyntax.ml ../caml/PrintPPC.ml \ + ../caml/Main2.ml EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES)) GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli) -CAMLINCL=-I ../caml +CAMLINCL=-I ../caml -I ../cil/obj/x86_LINUX OCAMLC=ocamlc -g $(CAMLINCL) OCAMLOPT=ocamlopt $(CAMLINCL) OCAMLDEP=ocamldep $(CAMLINCL) +OCAMLLIBS=unix.cma str.cma cil.cma COQINCL=-I ../lib -I ../common -I ../backend -I ../cfrontend COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source ../ccomp: $(FILES:.ml=.cmo) - $(OCAMLC) -o ../ccomp $(FILES:.ml=.cmo) + $(OCAMLC) -o ../ccomp $(OCAMLLIBS) $(FILES:.ml=.cmo) clean:: rm -f ../ccomp ../ccomp.opt: $(FILES:.ml=.cmx) - $(OCAMLOPT) -o ../ccomp.opt $(FILES:.ml=.cmx) + $(OCAMLOPT) -o ../ccomp.opt $(OCAMLLIBS:.cma=.cmxa) $(FILES:.ml=.cmx) clean:: rm -f ../ccomp.opt diff --git a/test/c/fft.c b/test/c/fft.c index 6f24af5..9edf427 100644 --- a/test/c/fft.c +++ b/test/c/fft.c @@ -9,11 +9,6 @@ #define PI 3.14159265358979323846 #endif -extern double cos_static(double), sin_static(double); - -#define cos cos_static -#define sin sin_static - /********************************************************/ /* A Duhamel-Hollman split-radix dif fft */ /* Ref: Electronics Letters, Jan. 5, 1984 */ @@ -23,9 +18,9 @@ extern double cos_static(double), sin_static(double); int dfft(double x[], double y[], int np) { -double *px,*py; -int i,j,k,m,n,i0,i1,i2,i3,is,id,n1,n2,n4; -double a,e,a3,cc1,ss1,cc3,ss3,r1,r2,s1,s2,s3,xt,tpi; + double *px,*py; + int i,j,k,m,n,i0,i1,i2,i3,is,id,n1,n2,n4; + double a,e,a3,cc1,ss1,cc3,ss3,r1,r2,s1,s2,s3,xt,tpi; px = x - 1; py = y - 1; @@ -34,33 +29,29 @@ double a,e,a3,cc1,ss1,cc3,ss3,r1,r2,s1,s2,s3,xt,tpi; while (i < np) { - i = i+i; - m = m+1; + i = i+i; + m = m+1; } n = i; - if (n != np) - { - for (i = np+1; i <= n; i++) - { - *(px + i) = 0.0; - *(py + i) = 0.0; - } - /*printf("nuse %d point fft",n); */ + if (n != np) { + for (i = np+1; i <= n; i++) { + px[i] = 0.0; + py[i] = 0.0; + } + /*printf("nuse %d point fft",n); */ } n2 = n+n; tpi = 2.0 * PI; - for (k = 1; k <= m-1; k++ ) - { + for (k = 1; k <= m-1; k++ ) { n2 = n2 / 2; n4 = n2 / 4; e = tpi / (double)n2; a = 0.0; - - for (j = 1; j<= n4 ; j++) - { + + for (j = 1; j<= n4 ; j++) { a3 = 3.0 * a; cc1 = cos(a); ss1 = sin(a); @@ -71,85 +62,78 @@ double a,e,a3,cc1,ss1,cc3,ss3,r1,r2,s1,s2,s3,xt,tpi; is = j; id = 2 * n2; - while ( is < n ) - { - for (i0 = is; i0 <= n-1; i0 = i0 + id) - { - i1 = i0 + n4; - i2 = i1 + n4; - i3 = i2 + n4; - r1 = *(px+i0) - *(px+i2); - *(px+i0) = *(px+i0) + *(px+i2); - r2 = *(px+i1) - *(px+i3); - *(px+i1) = *(px+i1) + *(px+i3); - s1 = *(py+i0) - *(py+i2); - *(py+i0) = *(py+i0) + *(py+i2); - s2 = *(py+i1) - *(py+i3); - *(py+i1) = *(py+i1) + *(py+i3); - s3 = r1 - s2; r1 = r1 + s2; - s2 = r2 - s1; r2 = r2 + s1; - *(px+i2) = r1*cc1 - s2*ss1; - *(py+i2) = -s2*cc1 - r1*ss1; - *(px+i3) = s3*cc3 + r2*ss3; - *(py+i3) = r2*cc3 - s3*ss3; - } - is = 2 * id - n2 + j; - id = 4 * id; - } + while ( is < n ) { + for (i0 = is; i0 <= n-1; i0 = i0 + id) { + i1 = i0 + n4; + i2 = i1 + n4; + i3 = i2 + n4; + r1 = px[i0] - px[i2]; + px[i0] = px[i0] + px[i2]; + r2 = px[i1] - px[i3]; + px[i1] = px[i1] + px[i3]; + s1 = py[i0] - py[i2]; + py[i0] = py[i0] + py[i2]; + s2 = py[i1] - py[i3]; + py[i1] = py[i1] + py[i3]; + s3 = r1 - s2; r1 = r1 + s2; + s2 = r2 - s1; r2 = r2 + s1; + px[i2] = r1*cc1 - s2*ss1; + py[i2] = -s2*cc1 - r1*ss1; + px[i3] = s3*cc3 + r2*ss3; + py[i3] = r2*cc3 - s3*ss3; + } + is = 2 * id - n2 + j; + id = 4 * id; + } } } - + /************************************/ /* Last stage, length=2 butterfly */ /************************************/ is = 1; id = 4; - while ( is < n) - { - for (i0 = is; i0 <= n; i0 = i0 + id) - { + while ( is < n) { + for (i0 = is; i0 <= n; i0 = i0 + id) { i1 = i0 + 1; - r1 = *(px+i0); - *(px+i0) = r1 + *(px+i1); - *(px+i1) = r1 - *(px+i1); - r1 = *(py+i0); - *(py+i0) = r1 + *(py+i1); - *(py+i1) = r1 - *(py+i1); - } - is = 2*id - 1; - id = 4 * id; + r1 = px[i0]; + px[i0] = r1 + px[i1]; + px[i1] = r1 - px[i1]; + r1 = py[i0]; + py[i0] = r1 + py[i1]; + py[i1] = r1 - py[i1]; + } + is = 2*id - 1; + id = 4 * id; } - + /*************************/ /* Bit reverse counter */ /*************************/ j = 1; n1 = n - 1; - for (i = 1; i <= n1; i++) - { - if (i < j) - { - xt = *(px+j); - *(px+j) = *(px+i); - *(px+i) = xt; - xt = *(py+j); - *(py+j) = *(py+i); - *(py+i) = xt; + for (i = 1; i <= n1; i++) { + if (i < j) { + xt = px[j]; + px[j] = px[i]; + px[i] = xt; + xt = py[j]; + py[j] = py[i]; + py[i] = xt; } k = n / 2; - while (k < j) - { - j = j - k; - k = k / 2; + while (k < j) { + j = j - k; + k = k / 2; } j = j + k; } /* - for (i = 1; i<=16; i++) printf("%d %g %gn",i,*(px+i),(py+i)); + for (i = 1; i<=16; i++) printf("%d %g %gn",i,px[i],py[i]); */ return(n); |