Commit 891377ce authored by xleroy's avatar xleroy
Browse files

Switching to the new C parser/elaborator/simplifier

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 018edf2d
......@@ -25,9 +25,12 @@ option) any later version:
cfrontend/PrintCsyntax.ml lib/Integers.v
cfrontend/Csem.v lib/Maps.v
cfrontend/Csyntax.v lib/Parmov.v
common/AST.v runtime/calloc.c
common/Errors.v runtime/stdio.c
common/Events.v runtime/stdio.h
common/AST.v lib/Camlcoq.ml
common/Errors.v
common/Events.v
all files in the runtime/ directory
all files in the cparser/ directory
(except those listed below which are under a BSD license)
A copy of the GNU General Public License version 2 is included below.
......@@ -37,12 +40,14 @@ files are free software and can be used both in commercial and
non-commercial contexts, subject to the terms of the GNU General
Public License.
This distribution includes a modified copy of the CIL library.
The CIL library is Copyright 2001-2005 George C. Necula, Scott McPeak,
Wes Weimer and Ben Liblit. The modifications are Copyright 2006,
2007, 2008, 2009 Institut National de Recherche en Informatique et en
Automatique. The CIL library and the modifications are distributed
under the terms of the BSD license, included below.
Finally, the following files are taken from the CIL library:
cparser/Cabs.ml
cparser/Lexer.mli
cparser/Lexer.mll
cparser/Parser.mly
These files are Copyright 2001-2005 George C. Necula, Scott McPeak,
Wes Weimer and Ben Liblit, and are distributed under the terms of the
BSD license, included below.
----------------------------------------------------------------------
......
......@@ -25,10 +25,7 @@ OCAMLBUILD=ocamlbuild
OCB_OPTIONS=\
-no-hygiene \
-no-links \
-I extraction $(INCLUDES) \
-cflags -I,`pwd`/cil/obj/$(ARCHOS) \
-lflags -I,`pwd`/cil/obj/$(ARCHOS) \
-libs unix,str,cil
-I extraction $(INCLUDES)
VPATH=$(DIRS)
GPATH=$(DIRS)
......@@ -89,9 +86,6 @@ extraction:
$(COQEXEC) extraction/extraction.v
cd extraction && ./fixextract
cil:
$(MAKE) -j1 -C cil
ccomp: driver/Configuration.ml
$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
&& rm -f ccomp && ln -s _build/driver/Driver.native ccomp
......@@ -111,7 +105,6 @@ runtime:
all:
$(MAKE) proof
$(MAKE) cil
$(MAKE) extraction
$(MAKE) ccomp
$(MAKE) runtime
......@@ -178,7 +171,6 @@ clean:
distclean:
$(MAKE) clean
rm -rf cil
rm -f Makefile.config
include .depend
......
<cparser/*.cmx>: for-pack(Cparser)
<driver/Driver.*{byte,native}>: use_unix,use_str,use_Cparser
......@@ -99,8 +99,10 @@ let dense_enough (numcases: int) (minkey: int64) (maxkey: int64) =
let compile_switch default table =
let (tbl, keys) = normalize_table table in
let minkey = uint64_of_coqint (IntSet.min_elt keys)
and maxkey = uint64_of_coqint (IntSet.max_elt keys) in
if dense_enough (List.length tbl) minkey maxkey
then compile_switch_as_jumptable default tbl minkey maxkey
else compile_switch_as_tree default tbl
if IntSet.is_empty keys then CTaction default else begin
let minkey = uint64_of_coqint (IntSet.min_elt keys)
and maxkey = uint64_of_coqint (IntSet.max_elt keys) in
if dense_enough (List.length tbl) minkey maxkey
then compile_switch_as_jumptable default tbl minkey maxkey
else compile_switch_as_tree default tbl
end
This diff is collapsed.
cparser/C
cparser/Errors
cparser/Cabs
cparser/Cabshelper
cparser/Parse_aux
cparser/Parser
cparser/Lexer
cparser/Machine
cparser/Env
cparser/Cprint
cparser/Cutil
cparser/Ceval
cparser/Cleanup
cparser/Builtins
cparser/Elab
cparser/Rename
cparser/Transform
cparser/Unblock
cparser/SimplExpr
cparser/AddCasts
cparser/StructByValue
cparser/StructAssign
cparser/Bitfields
cparser/Parse
AddCasts.cmi: C.cmi
Bitfields.cmi: C.cmi
Builtins.cmi: Env.cmi C.cmi
Ceval.cmi: Env.cmi C.cmi
Cleanup.cmi: C.cmi
C.cmi:
Cprint.cmi: C.cmi
Cutil.cmi: Env.cmi C.cmi
Elab.cmi: C.cmi
Env.cmi: C.cmi
Errors.cmi:
Lexer.cmi: Parser.cmi
Machine.cmi:
Parse_aux.cmi:
Parse.cmi: C.cmi
Parser.cmi: Cabs.cmo
Rename.cmi: C.cmi
SimplExpr.cmi: C.cmi
StructAssign.cmi: C.cmi
StructByValue.cmi: C.cmi
Transform.cmi: Env.cmi C.cmi
Unblock.cmi: C.cmi
AddCasts.cmo: Transform.cmi Cutil.cmi C.cmi AddCasts.cmi
AddCasts.cmx: Transform.cmx Cutil.cmx C.cmi AddCasts.cmi
Bitfields.cmo: Transform.cmi Machine.cmi Cutil.cmi C.cmi Bitfields.cmi
Bitfields.cmx: Transform.cmx Machine.cmx Cutil.cmx C.cmi Bitfields.cmi
Builtins.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi
Builtins.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmi
Cabshelper.cmo: Cabs.cmo
Cabshelper.cmx: Cabs.cmx
Cabs.cmo:
Cabs.cmx:
Ceval.cmo: Machine.cmi Cutil.cmi C.cmi Ceval.cmi
Ceval.cmx: Machine.cmx Cutil.cmx C.cmi Ceval.cmi
Cleanup.cmo: Cutil.cmi C.cmi Cleanup.cmi
Cleanup.cmx: Cutil.cmx C.cmi Cleanup.cmi
Cprint.cmo: C.cmi Cprint.cmi
Cprint.cmx: C.cmi Cprint.cmi
Cutil.cmo: Machine.cmi Errors.cmi Env.cmi Cprint.cmi C.cmi Cutil.cmi
Cutil.cmx: Machine.cmx Errors.cmx Env.cmx Cprint.cmx C.cmi Cutil.cmi
Elab.cmo: Parser.cmi Machine.cmi Lexer.cmi Errors.cmi Env.cmi Cutil.cmi \
Cprint.cmi Cleanup.cmi Ceval.cmi Cabshelper.cmo Cabs.cmo C.cmi \
Builtins.cmi Elab.cmi
Elab.cmx: Parser.cmx Machine.cmx Lexer.cmx Errors.cmx Env.cmx Cutil.cmx \
Cprint.cmx Cleanup.cmx Ceval.cmx Cabshelper.cmx Cabs.cmx C.cmi \
Builtins.cmx Elab.cmi
Env.cmo: C.cmi Env.cmi
Env.cmx: C.cmi Env.cmi
Errors.cmo: Errors.cmi
Errors.cmx: Errors.cmi
Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi
Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi
Machine.cmo: Machine.cmi
Machine.cmx: Machine.cmi
Main.cmo: Parse.cmi Cprint.cmi
Main.cmx: Parse.cmx Cprint.cmx
Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi
Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi
Parse.cmo: Unblock.cmi StructByValue.cmi StructAssign.cmi SimplExpr.cmi \
Rename.cmi Errors.cmi Elab.cmi Bitfields.cmi AddCasts.cmi Parse.cmi
Parse.cmx: Unblock.cmx StructByValue.cmx StructAssign.cmx SimplExpr.cmx \
Rename.cmx Errors.cmx Elab.cmx Bitfields.cmx AddCasts.cmx Parse.cmi
Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi
Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi
Rename.cmo: Errors.cmi Cutil.cmi C.cmi Builtins.cmi Rename.cmi
Rename.cmx: Errors.cmx Cutil.cmx C.cmi Builtins.cmx Rename.cmi
Scoping.cmo:
Scoping.cmx:
SimplExpr.cmo: Transform.cmi Cutil.cmi C.cmi SimplExpr.cmi
SimplExpr.cmx: Transform.cmx Cutil.cmx C.cmi SimplExpr.cmi
SimplifyStrict.cmo: Env.cmi Cutil.cmi C.cmi
SimplifyStrict.cmx: Env.cmx Cutil.cmx C.cmi
StructAssign.cmo: Transform.cmi Errors.cmi Env.cmi Cutil.cmi C.cmi \
StructAssign.cmi
StructAssign.cmx: Transform.cmx Errors.cmx Env.cmx Cutil.cmx C.cmi \
StructAssign.cmi
StructByValue.cmo: Transform.cmi Env.cmi Cutil.cmi C.cmi StructByValue.cmi
StructByValue.cmx: Transform.cmx Env.cmx Cutil.cmx C.cmi StructByValue.cmi
Transform.cmo: Env.cmi Cutil.cmi C.cmi Builtins.cmi Transform.cmi
Transform.cmx: Env.cmx Cutil.cmx C.cmi Builtins.cmx Transform.cmi
Unblock.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi Unblock.cmi
Unblock.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi Unblock.cmi
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Materialize implicit casts *)
(* Assumes: simplified code
Produces: simplified code
Preserves: unblocked code *)
open C
open Cutil
open Transform
(* We have the option of materializing all casts or leave "widening"
casts implicit. Widening casts are:
- from a small integer type to a larger integer type,
- from a small float type to a larger float type,
- from a pointer type to void *.
*)
let omit_widening_casts = ref false
let widening_cast env tfrom tto =
begin match unroll env tfrom, unroll env tto with
| TInt(k1, _), TInt(k2, _) ->
let r1 = integer_rank k1 and r2 = integer_rank k2 in
r1 < r2 || (r1 = r2 && is_signed_ikind k1 = is_signed_ikind k2)
| TFloat(k1, _), TFloat(k2, _) ->
float_rank k1 <= float_rank k2
| TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2
| _, _ -> false
end
let cast_not_needed env tfrom tto =
let tfrom = pointer_decay env tfrom
and tto = pointer_decay env tto in
compatible_types env tfrom tto
|| (!omit_widening_casts && widening_cast env tfrom tto)
let cast env e tto =
if cast_not_needed env e.etyp tto
then e
else {edesc = ECast(tto, e); etyp = tto}
(* Note: this pass applies only to simplified expressions
because casts cannot be materialized in op= expressions... *)
let rec add_expr env e =
match e.edesc with
| EConst _ -> e
| EVar _ -> e
| ESizeof _ -> e
| EUnop(op, e1) ->
let e1' = add_expr env e1 in
let desc =
match op with
| Ominus | Oplus | Onot ->
EUnop(op, cast env e1' e.etyp)
| Olognot | Oderef | Oaddrof
| Odot _ | Oarrow _ ->
EUnop(op, e1')
| Opreincr | Opredecr | Opostincr | Opostdecr ->
assert false (* not simplified *)
in { edesc = desc; etyp = e.etyp }
| EBinop(op, e1, e2, ty) ->
let e1' = add_expr env e1 in
let e2' = add_expr env e2 in
let desc =
match op with
| Oadd ->
if is_pointer_type env ty
then EBinop(Oadd, e1', e2', ty)
else EBinop(Oadd, cast env e1' ty, cast env e2' ty, ty)
| Osub ->
if is_pointer_type env ty
then EBinop(Osub, e1', e2', ty)
else EBinop(Osub, cast env e1' ty, cast env e2' ty, ty)
| Omul|Odiv|Omod|Oand|Oor|Oxor|Oeq|One|Olt|Ogt|Ole|Oge ->
EBinop(op, cast env e1' ty, cast env e2' ty, ty)
| Oshl|Oshr ->
EBinop(op, cast env e1' ty, e2', ty)
| Oindex | Ologand | Ologor | Ocomma ->
EBinop(op, e1', e2', ty)
| Oassign
| Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
| Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
assert false (* not simplified *)
in { edesc = desc; etyp = e.etyp }
| EConditional(e1, e2, e3) ->
{ edesc =
EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
etyp = e.etyp }
| ECast(ty, e1) ->
{ edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
| ECall(e1, el) ->
assert false (* not simplified *)
(* Arguments to a prototyped function *)
let rec add_proto env args params =
match args, params with
| [], _ -> []
| _::_, [] -> add_noproto env args
| arg1 :: argl, (_, ty_p) :: paraml ->
cast env (add_expr env arg1) ty_p ::
add_proto env argl paraml
(* Arguments to a non-prototyped function *)
and add_noproto env args =
match args with
| [] -> []
| arg1 :: argl ->
cast env (add_expr env arg1) (default_argument_conversion env arg1.etyp) ::
add_noproto env argl
(* Arguments to function calls in general *)
let add_arguments env ty_fun args =
let ty_args =
match unroll env ty_fun with
| TFun(res, args, vararg, a) -> args
| TPtr(ty, a) ->
begin match unroll env ty with
| TFun(res, args, vararg, a) -> args
| _ -> assert false
end
| _ -> assert false in
match ty_args with
| None -> add_noproto env args
| Some targs -> add_proto env args targs
(* Toplevel expressions (appearing in Sdo statements) *)
let add_topexpr env loc e =
match e.edesc with
| EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
let ecall =
{edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
etyp = ty} in
if cast_not_needed env ty lhs.etyp then
sassign loc (add_expr env lhs) ecall
else begin
let tmp = new_temp (erase_attributes_type env ty) in
sseq loc (sassign loc tmp ecall)
(sassign loc (add_expr env lhs) (cast env tmp lhs.etyp))
end
| EBinop(Oassign, lhs, rhs, _) ->
sassign loc (add_expr env lhs) (cast env (add_expr env rhs) lhs.etyp)
| ECall(e1, el) ->
let ecall =
{edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
etyp = e.etyp} in
{sdesc = Sdo ecall; sloc = loc}
| _ ->
assert false
(* Initializers *)
let rec add_init env tto = function
| Init_single e ->
Init_single (cast env (add_expr env e) tto)
| Init_array il ->
let ty_elt =
match unroll env tto with
| TArray(ty, _, _) -> ty | _ -> assert false in
Init_array (List.map (add_init env ty_elt) il)
| Init_struct(id, fil) ->
Init_struct (id, List.map
(fun (fld, i) -> (fld, add_init env fld.fld_typ i))
fil)
| Init_union(id, fld, i) ->
Init_union(id, fld, add_init env fld.fld_typ i)
(* Declarations *)
let add_decl env (sto, id, ty, optinit) =
(sto, id, ty,
begin match optinit with
| None -> None
| Some init -> Some(add_init env ty init)
end)
(* Statements *)
let rec add_stmt env s =
match s.sdesc with
| Sskip -> s
| Sdo e -> add_topexpr env s.sloc e
| Sseq(s1, s2) ->
{sdesc = Sseq(add_stmt env s1, add_stmt env s2); sloc = s.sloc }
| Sif(e, s1, s2) ->
{sdesc = Sif(add_expr env e, add_stmt env s1, add_stmt env s2);
sloc = s.sloc}
| Swhile(e, s1) ->
{sdesc = Swhile(add_expr env e, add_stmt env s1);
sloc = s.sloc}
| Sdowhile(s1, e) ->
{sdesc = Sdowhile(add_stmt env s1, add_expr env e);
sloc = s.sloc}
| Sfor(s1, e, s2, s3) ->
{sdesc = Sfor(add_stmt env s1, add_expr env e, add_stmt env s2,
add_stmt env s3);
sloc = s.sloc}
| Sbreak -> s
| Scontinue -> s
| Sswitch(e, s1) ->
{sdesc = Sswitch(add_expr env e, add_stmt env s1); sloc = s.sloc}
| Slabeled(lbl, s) ->
{sdesc = Slabeled(lbl, add_stmt env s); sloc = s.sloc}
| Sgoto lbl -> s
| Sreturn None -> s
| Sreturn (Some e) ->
{sdesc = Sreturn(Some(add_expr env e)); sloc = s.sloc}
| Sblock sl ->
{sdesc = Sblock(List.map (add_stmt env) sl); sloc = s.sloc}
| Sdecl d ->
{sdesc = Sdecl(add_decl env d); sloc = s.sloc}
let add_fundef env f =
reset_temps();
let body' = add_stmt env f.fd_body in
let temps = get_temps () in
(* fd_locals have no initializers, so no need to transform them *)
{ f with fd_locals = f.fd_locals @ temps; fd_body = body' }
let program ?(all = false) p =
omit_widening_casts := not all;
Transform.program ~decl:add_decl ~fundef:add_fundef p
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
val program: ?all: bool -> C.program -> C.program
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Elimination of bit fields in structs *)
(* Assumes: unblocked, simplified code.
Preserves: unblocked, simplified code. *)
open Printf
open Machine
open C
open Cutil
open Transform
(* Info associated to each bitfield *)
type bitfield_info =
{ bf_carrier: string; (* name of underlying regular field *)
bf_carrier_typ: typ; (* type of underlying regular field *)
bf_pos: int; (* start bit *)
bf_size: int; (* size in bit *)
bf_signed: bool } (* signed or unsigned *)
(* invariants:
0 <= pos < bitsizeof(int)
0 < sz <= bitsizeof(int)
0 < pos + sz <= bitsizeof(int)
*)
(* Mapping (struct identifier, bitfield name) -> bitfield info *)
let bitfield_table =
(Hashtbl.create 57: (ident * string, bitfield_info) Hashtbl.t)
(* Packing algorithm -- keep consistent with [Cutil.pack_bitfield]! *)
let unsigned_ikind_for_carrier nbits =
if nbits <= 8 then IUChar else
if nbits <= 8 * !config.sizeof_short then IUShort else
if nbits <= 8 * !config.sizeof_int then IUInt else
if nbits <= 8 * !config.sizeof_long then IULong else
if nbits <= 8 * !config.sizeof_longlong then IULongLong else
assert false
let pack_bitfields env id ml =
let rec pack accu pos = function
| [] ->
(pos, accu, [])
| m :: ms as ml ->
match m.fld_bitfield with
| None -> (pos, accu, ml)
| Some n ->
if n = 0 then
(pos, accu, ms) (* bit width 0 means end of pack *)
else if pos + n >= 8 * !config.sizeof_int then
(pos, accu, ml) (* doesn't fit in current word *)
else begin
let signed =
match unroll env m.fld_typ with
| TInt(ik, _) -> is_signed_ikind ik
| _ -> assert false (* should never happen, checked in Elab *) in
pack ((m.fld_name, pos, n, signed) :: accu) (pos + n) ms
end
in pack [] 0 ml
let rec transf_members env id count = function
| [] -> []
| m :: ms as ml ->
if m.fld_bitfield = None then
m :: transf_members env id count ms
else begin
let (nbits, bitfields, ml') = pack_bitfields env id ml in
let carrier = sprintf "__bf%d" count in
let carrier_typ = TInt(unsigned_ikind_for_carrier nbits, []) in
List.iter
(fun (name, pos, sz, signed) ->
Hashtbl.add bitfield_table
(id, name)
{bf_carrier = carrier; bf_carrier_typ = carrier_typ;
bf_pos = pos; bf_size = sz; bf_signed = signed})
bitfields;
{ fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
:: transf_members env id (count + 1) ml'
end
let transf_composite env su id ml =
match su with
| Struct -> transf_members env id 1 ml
| Union -> ml
(* Bitfield manipulation expressions *)
let left_shift_count bf =
intconst
(Int64.of_int (8 * !config.sizeof_int - (bf.bf_pos + bf.bf_size)))
IInt
let right_shift_count bf =
intconst
(Int64.of_int (8 * !config.sizeof_int - bf.bf_size))
IInt
let insertion_mask bf =
let m =
Int64.shift_left
(Int64.pred (Int64.shift_left 1L bf.bf_size))
bf.bf_pos in
(* Give the mask an hexadecimal string representation, nicer to read *)
{edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])}
(* Extract the value of a bitfield *)
(* Reference C code:
unsigned int bitfield_unsigned_extract(unsigned int x, int ofs, int sz)
{
return (x << (BITSIZE_UINT - (ofs + sz))) >> (BITSIZE_UINT - sz);
}
signed int bitfield_signed_extract(unsigned int x, int ofs, int sz)
{
return ((signed int) (x << (BITSIZE_UINT - (ofs + sz))))
>> (BITSIZE_UINT - sz);
}
*)
let bitfield_extract bf carrier =
let e1 =
{edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, []));
etyp = carrier.etyp} in
let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
let e2 =
{edesc = ECast(ty, e1); etyp = ty} in
{edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
etyp = e2.etyp}
(* Assign a bitfield within a carrier *)