diff options
| -rw-r--r-- | .depend | 5 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 109 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 72 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 1814 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 17 | ||||
| -rw-r--r-- | common/Determinism.v | 109 | ||||
| -rw-r--r-- | common/Globalenvs.v | 208 | ||||
| -rw-r--r-- | cparser/StructAssign.ml | 50 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Compiler.v | 9 | ||||
| -rw-r--r-- | driver/Driver.ml | 152 | ||||
| -rw-r--r-- | driver/Interp.ml | 408 | ||||
| -rw-r--r-- | extraction/extraction.v | 1 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 109 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 122 | ||||
| -rw-r--r-- | test/regression/expr1.c | 2 | ||||
| -rw-r--r-- | test/regression/initializers.c | 2 | ||||
| -rw-r--r-- | test/regression/volatile2.c | 2 |
19 files changed, 2741 insertions, 455 deletions
@@ -90,9 +90,10 @@ $(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqli cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo +cfrontend/Cexec.vo cfrontend/Cexec.glob: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo -cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo +cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Clight.vo cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo @@ -101,5 +102,5 @@ cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo -driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo +driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo @@ -71,7 +71,7 @@ BACKEND=\ # C front-end modules (in cfrontend/) -CFRONTEND=Csyntax.v Csem.v Cstrategy.v \ +CFRONTEND=Csyntax.v Csem.v Cstrategy.v Cexec.v \ Initializers.v Initializersproof.v \ SimplExpr.v SimplExprspec.v SimplExprproof.v \ Clight.v Cshmgen.v Cshmgenproof.v \ @@ -114,7 +114,7 @@ ccomp.byte: driver/Configuration.ml runtime: $(MAKE) -C runtime -.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte runtime +.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte cinterp cinterp.byte runtime all: $(MAKE) proof diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index cc42f3c..44a7571 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -269,9 +269,7 @@ let print_annot_val oc txt args res = (* The ARM has strict alignment constraints. *) -let print_builtin_memcpy oc sz al args = - let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in +let print_builtin_memcpy_small oc sz al src dst = let rec copy ofs sz ninstr = if sz >= 4 && al >= 4 then begin fprintf oc " ldr %a, [%a, #%d]\n" ireg IR14 ireg src ofs; @@ -287,10 +285,50 @@ let print_builtin_memcpy oc sz al args = copy (ofs + 1) (sz - 1) (ninstr + 2) end else ninstr in - fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n" + copy 0 sz 0 + +let print_builtin_memcpy_big oc sz al src dst = + assert (sz >= al); + assert (sz mod al = 0); + let (load, store, chunksize) = + if al >= 4 then ("ldr", "str", 4) + else if al = 2 then ("ldrh", "strh", 2) + else ("ldrb", "strb", 1) in + let tmp = + if src <> IR0 && dst <> IR0 then IR0 + else if src <> IR1 && dst <> IR1 then IR1 + else IR2 in + fprintf oc " stmfd sp!, {%a,%a,%a}\n" ireg tmp ireg src ireg dst; + begin match Asmgen.decompose_int + (coqint_of_camlint (Int32.of_int (sz / chunksize))) with + | [] -> assert false + | hd::tl -> + fprintf oc " mov %a, #%a\n" ireg IR14 coqint hd; + List.iter + (fun n -> + fprintf oc " orr %a, %a, #%a\n" ireg IR14 ireg IR14 coqint n) + tl + end; + let lbl = new_label() in + fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg tmp ireg src chunksize; + fprintf oc " subs %a, %a, #1\n" ireg IR14 ireg IR14; + fprintf oc " %s %a, [%a], #%d\n" store ireg tmp ireg dst chunksize; + fprintf oc " bne .L%d\n" lbl; + fprintf oc " ldmfd sp!, {%a,%a,%a}\n" ireg tmp ireg src ireg dst; + 9 + +let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in + fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" comment sz al; - let n = copy 0 sz 0 in - fprintf oc "%s end builtin __builtin_memcpy\n" comment; n + let n = + if sz <= 64 + then print_builtin_memcpy_small oc sz al src dst + else print_builtin_memcpy_big oc sz al src dst in + fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n + +(* Handling of volatile reads and writes *) let print_builtin_vload oc chunk args res = fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; @@ -351,46 +389,6 @@ let print_builtin_inline oc name args res = fprintf oc "%s end %s\n" comment name; n -(* Handling of other builtins *) - -let re_builtin_function = Str.regexp "__builtin_" - -let is_builtin_function s = - Str.string_match re_builtin_function (extern_atom s) 0 - -let print_memcpy oc load store sz log2sz = - let lbl1 = new_label() in - let lbl2 = new_label() in - if sz = 1 - then fprintf oc " cmp %a, #0\n" ireg IR2 - else fprintf oc " movs %a, %a, lsr #%d\n" ireg IR2 ireg IR2 log2sz; - fprintf oc " beq .L%d\n" lbl1; - fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl2 load ireg IR3 ireg IR1 sz; - fprintf oc " subs %a, %a, #1\n" ireg IR2 ireg IR2; - fprintf oc " %s %a, [%a], #%d\n" store ireg IR3 ireg IR0 sz; - fprintf oc " bne .L%d\n" lbl2; - fprintf oc ".L%d:\n" lbl1; - 7 - -let print_builtin_function oc s = - fprintf oc "%s begin %s\n" comment (extern_atom s); - (* int args: IR0-IR3 float args: FR0, FR1 - int res: IR0 float res: FR0 *) - let n = match extern_atom s with - (* Block copy *) - | "__builtin_memcpy" -> - print_memcpy oc "ldrb" "strb" 1 0 - | "__builtin_memcpy_al2" -> - print_memcpy oc "ldrh" "strh" 2 1 - | "__builtin_memcpy_al4" | "__builtin_memcpy_al8" -> - print_memcpy oc "ldr" "str" 4 2 - (* Catch-all *) - | s -> - invalid_arg ("unrecognized builtin function " ^ s) - in - fprintf oc "%s end %s\n" comment (extern_atom s); - n - (* Printing of instructions *) let shift_op oc = function @@ -424,21 +422,11 @@ let print_instruction oc = function | Pbc(bit, lbl) -> fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1 | Pbsymb id -> - if not (is_builtin_function id) then begin - fprintf oc " b %a\n" print_symb id; 1 - end else begin - let n = print_builtin_function oc id in - fprintf oc " mov pc, r14\n"; - n + 1 - end + fprintf oc " b %a\n" print_symb id; 1 | Pbreg r -> fprintf oc " mov pc, %a\n" ireg r; 1 | Pblsymb id -> - if not (is_builtin_function id) then begin - fprintf oc " bl %a\n" print_symb id; 1 - end else begin - print_builtin_function oc id - end + fprintf oc " bl %a\n" print_symb id; 1 | Pblreg r -> fprintf oc " mov lr, pc\n"; fprintf oc " mov pc, %a\n" ireg r; 2 @@ -658,9 +646,8 @@ let print_fundef oc (Coq_pair(name, defn)) = match defn with | Internal code -> print_function oc name code - | External ef -> - if need_stub ef && not(is_builtin_function name) - then print_external_function oc name (ef_sig ef) + | External ef + if need_stub ef then print_external_function oc name (ef_sig ef) (* Data *) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 225905a..f8905a6 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -72,28 +72,11 @@ let builtins_generic = { "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); (* Block copy *) - "__builtin_memcpy", - (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, [])], - false); - "__builtin_memcpy_al2", - (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, [])], - false); - "__builtin_memcpy_al4", - (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, [])], - false); - "__builtin_memcpy_al8", + "__builtin_memcpy_aligned", (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, []); TInt(Cutil.size_t_ikind, [])], false); (* Annotations *) @@ -216,14 +199,10 @@ let register_annotation_val txt targ = (** ** Handling of inlined memcpy functions *) -let register_inlined_memcpy basename sz = +let register_inlined_memcpy sz al = let al = - match basename with - | "__builtin_memcpy_al2" -> 2l - | "__builtin_memcpy_al4" -> 4l - | "__builtin_memcpy_al8" -> 8l - | _ -> 1l in - let name = Printf.sprintf "%s_sz%ld" basename sz in + if al <= 4l then al else 4l in (* max alignment supported by CompCert *) + let name = Printf.sprintf "__builtin_memcpy_sz%ld_al%ld" sz al in let targs = Tcons(Tpointer Tvoid, Tcons(Tpointer Tvoid, Tnil)) and tres = Tvoid and ef = EF_memcpy(coqint_of_camlint sz, coqint_of_camlint al) in @@ -231,24 +210,21 @@ let register_inlined_memcpy basename sz = Evalof(Evar(intern_string name, Tfunction(targs, tres)), Tfunction(targs, tres)) -let memcpy_inline_threshold = ref 64l - -let make_builtin_memcpy name fn args = +let make_builtin_memcpy args = match args with - | Econs(dst, Econs(src, Econs(sz, Enil))) -> + | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) -> let sz1 = match Initializers.constval sz with - | CompcertErrors.OK(Vint n) -> Some (camlint_of_coqint n) - | _ -> None in - begin match sz1 with - | Some sz2 when sz2 <= !memcpy_inline_threshold -> - let fn = register_inlined_memcpy name sz2 in - Ecall(fn, Econs(dst, Econs(src, Enil)), Tvoid) - | _ -> - Ecall(fn, args, Tvoid) - end + | CompcertErrors.OK(Vint n) -> camlint_of_coqint n + | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; 0l in + let al1 = + match Initializers.constval al with + | CompcertErrors.OK(Vint n) -> camlint_of_coqint n + | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; 0l in + let fn = register_inlined_memcpy sz1 al1 in + Ecall(fn, Econs(dst, Econs(src, Enil)), Tvoid) | _ -> - Ecall(fn, args, Tvoid) + assert false (** ** Translation functions *) @@ -570,12 +546,8 @@ let rec convertExpr env e = ezero end - | C.ECall({edesc = C.EVar {name = ("__builtin_memcpy" - |"__builtin_memcpy_al2" - |"__builtin_memcpy_al4" - |"__builtin_memcpy_al8" as name)}} as fn, - args) -> - make_builtin_memcpy name (convertExpr env fn) (convertExprList env args) + | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) -> + make_builtin_memcpy (convertExprList env args) | C.ECall(fn, args) -> match projFunType env fn.etyp with @@ -764,11 +736,6 @@ let convertFundef env fd = (** External function declaration *) -let noninlined_builtin_functions = [ - "__builtin_memcpy"; "__builtin_memcpy_al2"; - "__builtin_memcpy_al4"; "__builtin_memcpy_al8" -] - let convertFundecl env (sto, id, ty, optinit) = let (args, res) = match convertTyp env ty with @@ -777,8 +744,9 @@ let convertFundecl env (sto, id, ty, optinit) = let id' = intern_string id.name in let sg = signature_of_type args res in let ef = + if id.name = "malloc" then EF_malloc else + if id.name = "free" then EF_free else if List.mem_assoc id.name builtins.functions - && not (List.mem id.name noninlined_builtin_functions) then EF_builtin(id', sg) else EF_external(id', sg) in Datatypes.Coq_pair(id', External(ef, args, res)) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v new file mode 100644 index 0000000..3dd34c1 --- /dev/null +++ b/cfrontend/Cexec.v @@ -0,0 +1,1814 @@ +Require Import Axioms. +Require Import Coqlib. +Require Import Errors. +Require Import Maps. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import AST. +Require Import Memory. +Require Import Events. +Require Import Globalenvs. +Require Import Determinism. +Require Import Csyntax. +Require Import Csem. +Require Cstrategy. + +(** Animating the CompCert C semantics *) + +Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} +with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2} +with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}. +Proof. + assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality. + assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality. + assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality. + generalize ident_eq zeq. intros E1 E2. + decide equality. + decide equality. + generalize ident_eq. intros E1. + decide equality. +Defined. + +Opaque type_eq. + +(** Error monad with options or lists *) + +Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end) + (at level 200, X ident, A at level 100, B at level 200) + : option_monad_scope. + +Notation " 'check' A ; B" := (if A then B else None) + (at level 200, A at level 100, B at level 200) + : option_monad_scope. + +Notation "'do' X <- A ; B" := (match A with Some X => B | None => nil end) + (at level 200, X ident, A at level 100, B at level 200) + : list_monad_scope. + +Notation " 'check' A ; B" := (if A then B else nil) + (at level 200, A at level 100, B at level 200) + : list_monad_scope. + +Definition is_val (a: expr) : option (val * type) := + match a with + | Eval v ty => Some(v, ty) + | _ => None + end. + +Lemma is_val_inv: + forall a v ty, is_val a = Some(v, ty) -> a = Eval v ty. +Proof. + intros until ty. destruct a; simpl; congruence. +Qed. + +Definition is_loc (a: expr) : option (block * int * type) := + match a with + | Eloc b ofs ty => Some(b, ofs, ty) + | _ => None + end. + +Lemma is_loc_inv: + forall a b ofs ty, is_loc a = Some(b, ofs, ty) -> a = Eloc b ofs ty. +Proof. + intros until ty. destruct a; simpl; congruence. +Qed. + +Local Open Scope option_monad_scope. + +Fixpoint is_val_list (al: exprlist) : option (list (val * type)) := + match al with + | Enil => Some nil + | Econs a1 al => do vt1 <- is_val a1; do vtl <- is_val_list al; Some(vt1::vtl) + end. + +Definition is_skip (s: statement) : {s = Sskip} + {s <> Sskip}. +Proof. + destruct s; (left; congruence) || (right; congruence). +Qed. + +(** * Reduction of expressions *) + +Section EXEC. + +Variable ge: genv. + +Inductive reduction: Type := + | Lred (l': expr) (m': mem) + | Rred (r': expr) (m': mem) + | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem). + +Section EXPRS. + +Variable e: env. + +Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) := + match vtl, tl with + | nil, Tnil => Some nil + | (v1,t1)::vtl, Tcons t1' tl => + do v <- sem_cast v1 t1 t1'; do vl <- sem_cast_arguments vtl tl; Some(v::vl) + | _, _ => None + end. + +(** The result of stepping an expression can be +- [None] denoting that the expression is stuck; +- [Some nil] meaning that the expression is fully reduced + (it's [Eval] for a r-value and [Eloc] for a l-value); +- [Some ll] meaning that the expression can reduce to any of + the elements of [ll]. Each element is a pair of a context + and a reduction inside this context (see type [reduction] above). +*) + +Definition reducts (A: Type): Type := option (list ((expr -> A) * reduction)). + +Definition topred (r: reduction) : reducts expr := + Some (((fun (x: expr) => x), r) :: nil). + +Definition incontext {A B: Type} (ctx: A -> B) (r: reducts A) : reducts B := + match r with + | None => None + | Some l => Some (map (fun z => ((fun (x: expr) => ctx(fst z x)), snd z)) l) + end. + +Definition incontext2 {A1 A2 B: Type} + (ctx1: A1 -> B) (r1: reducts A1) + (ctx2: A2 -> B) (r2: reducts A2) : reducts B := + match r1, r2 with + | None, _ => None + | _, None => None + | Some l1, Some l2 => + Some (map (fun z => ((fun (x: expr) => ctx1(fst z x)), snd z)) l1 + ++ map (fun z => ((fun (x: expr) => ctx2(fst z x)), snd z)) l2) + end. + +Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := + match k, a with + | LV, Eloc b ofs ty => + Some nil + | LV, Evar x ty => + match e!x with + | Some(b, ty') => + check type_eq ty ty'; + topred (Lred (Eloc b Int.zero ty) m) + | None => + do b <- Genv.find_symbol ge x; + do ty' <- type_of_global ge b; + check type_eq ty ty'; + topred (Lred (Eloc b Int.zero ty) m) + end + | LV, Ederef r ty => + match is_val r with + | Some(Vptr b ofs, ty') => + topred (Lred (Eloc b ofs ty) m) + | Some _ => + None + | None => + incontext (fun x => Ederef x ty) (step_expr RV r m) + end + | LV, Efield l f ty => + match is_loc l with + | Some(b, ofs, ty') => + match ty' with + | Tstruct id fList => + match field_offset f fList with + | Error _ => None + | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m) + end + | Tunion id fList => + topred (Lred (Eloc b ofs ty) m) + | _ => None + end + | None => + incontext (fun x => Efield x f ty) (step_expr LV l m) + end + | RV, Eval v ty => + Some nil + | RV, Evalof l ty => + match is_loc l with + | Some(b, ofs, ty') => + check type_eq ty ty'; + do v <- load_value_of_type ty m b ofs; + topred (Rred (Eval v ty) m) + | None => + incontext (fun x => Evalof x ty) (step_expr LV l m) + end + | RV, Eaddrof l ty => + match is_loc l with + | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m) + | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m) + end + | RV, Eunop op r1 ty => + match is_val r1 with + | Some(v1, ty1) => + do v <- sem_unary_operation op v1 ty1; + topred (Rred (Eval v ty) m) + | None => + incontext (fun x => Eunop op x ty) (step_expr RV r1 m) + end + | RV, Ebinop op r1 r2 ty => + match is_val r1, is_val r2 with + | Some(v1, ty1), Some(v2, ty2) => + do v <- sem_binary_operation op v1 ty1 v2 ty2 m; + topred (Rred (Eval v ty) m) + | _, _ => + incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m) + (fun x => Ebinop op r1 x ty) (step_expr RV r2 m) + end + | RV, Ecast r1 ty => + match is_val r1 with + | Some(v1, ty1) => + do v <- sem_cast v1 ty1 ty; + topred (Rred (Eval v ty) m) + | None => + incontext (fun x => Ecast x ty) (step_expr RV r1 m) + end + | RV, Econdition r1 r2 r3 ty => + match is_val r1 with + | Some(v1, ty1) => + do b <- bool_val v1 ty1; + topred (Rred (Eparen (if b then r2 else r3) ty) m) + | None => + incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) + end + | RV, Esizeof ty' ty => + topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m) + | RV, Eassign l1 r2 ty => + match is_loc l1, is_val r2 with + | Some(b, ofs, ty1), Some(v2, ty2) => + check type_eq ty1 ty; + do v <- sem_cast v2 ty2 ty1; + do m' <- store_value_of_type ty1 m b ofs v; + topred (Rred (Eval v ty) m') + | _, _ => + incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m) + (fun x => Eassign l1 x ty) (step_expr RV r2 m) + end + | RV, Eassignop op l1 r2 tyres ty => + match is_loc l1, is_val r2 with + | Some(b, ofs, ty1), Some(v2, ty2) => + check type_eq ty1 ty; + do v1 <- load_value_of_type ty1 m b ofs; + do v <- sem_binary_operation op v1 ty1 v2 ty2 m; + do v' <- sem_cast v tyres ty1; + do m' <- store_value_of_type ty1 m b ofs v'; + topred (Rred (Eval v' ty) m') + | _, _ => + incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m) + (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m) + end + | RV, Epostincr id l ty => + match is_loc l with + | Some(b, ofs, ty1) => + check type_eq ty1 ty; + do v1 <- load_value_of_type ty m b ofs; + do v2 <- sem_incrdecr id v1 ty; + do v3 <- sem_cast v2 (typeconv ty) ty; + do m' <- store_value_of_type ty m b ofs v3; + topred (Rred (Eval v1 ty) m') + | None => + incontext (fun x => Epostincr id x ty) (step_expr LV l m) + end + | RV, Ecomma r1 r2 ty => + match is_val r1 with + | Some _ => + check type_eq (typeof r2) ty; + topred (Rred r2 m) + | None => + incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m) + end + | RV, Eparen r1 ty => + match is_val r1 with + | Some (v1, ty1) => + do v <- sem_cast v1 ty1 ty; + topred (Rred (Eval v ty) m) + | None => + incontext (fun x => Eparen x ty) (step_expr RV r1 m) + end + | RV, Ecall r1 rargs ty => + match is_val r1, is_val_list rargs with + | Some(vf, tyf), Some vtl => + match classify_fun tyf with + | fun_case_f tyargs tyres => + do fd <- Genv.find_funct ge vf; + do vargs <- sem_cast_arguments vtl tyargs; + check type_eq (type_of_fundef fd) (Tfunction tyargs tyres); + topred (Callred fd vargs ty m) + | _ => None + end + | _, _ => + incontext2 (fun x => Ecall x rargs ty) (step_expr RV r1 m) + (fun x => Ecall r1 x ty) (step_exprlist rargs m) + end + | _, _ => None + end + +with step_exprlist (rl: exprlist) (m: mem): reducts exprlist := + match rl with + | Enil => + Some nil + | Econs r1 rs => + incontext2 (fun x => Econs x rs) (step_expr RV r1 m) + (fun x => Econs r1 x) (step_exprlist rs m) + end. + +(** Soundness: if [step_expr] returns [Some ll], then every element + of [ll] is a reduct. *) + +Lemma context_compose: + forall k2 k3 C2, context k2 k3 C2 -> + forall k1 C1, context k1 k2 C1 -> + context k1 k3 (fun x => C2(C1 x)) +with contextlist_compose: + forall k2 C2, contextlist k2 C2 -> + forall k1 C1, context k1 k2 C1 -> + contextlist k1 (fun x => C2(C1 x)). +Proof. + induction 1; intros; try (constructor; eauto). + replace (fun x => C1 x) with C1. auto. apply extensionality; auto. + induction 1; intros; constructor; eauto. +Qed. + +Hint Constructors context contextlist. +Hint Resolve context_compose contextlist_compose. + +Definition reduction_ok (a: expr) (m: mem) (rd: reduction) : Prop := + match rd with + | Lred l' m' => lred ge e a m l' m' + | Rred r' m' => rred a m r' m' + | Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m + end. + +Definition reduction_kind (rd: reduction): kind := + match rd with + | Lred l' m' => LV + | Rred r' m' => RV + | Callred fd args tyres m' => RV + end. + +Ltac monadInv := + match goal with + | [ H: match ?x with Some _ => _ | None => None end = Some ?y |- _ ] => + destruct x as []_eqn; [monadInv|discriminate] + | [ H: match ?x with left _ => _ | right _ => None end = Some ?y |- _ ] => + destruct x; [monadInv|discriminate] + | _ => idtac + end. + +Lemma sem_cast_arguments_sound: + forall rargs vtl tyargs vargs, + is_val_list rargs = Some vtl -> + sem_cast_arguments vtl tyargs = Some vargs -> + cast_arguments rargs tyargs vargs. +Proof. + induction rargs; simpl; intros. + inv H. destruct tyargs; simpl in H0; inv H0. constructor. + monadInv. inv H. simpl in H0. destruct p as [v1 t1]. destruct tyargs; try congruence. monadInv. + inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto. +Qed. + +Definition reducts_ok (k: kind) (a: expr) (m: mem) (res: reducts expr) : Prop := + match res with + | None => True + | Some nil => match k with LV => is_loc a <> None | RV => is_val a <> None end + | Some ll => + forall C rd, + In (C, rd) ll -> + context (reduction_kind rd) k C /\ exists a', a = C a' /\ reduction_ok a' m rd + end. + +Definition list_reducts_ok (al: exprlist) (m: mem) (res: reducts exprlist) : Prop := + match res with + | None => True + | Some nil => is_val_list al <> None + | Some ll => + forall C rd, + In (C, rd) ll -> + contextlist (reduction_kind rd) C /\ exists a', al = C a' /\ reduction_ok a' m rd + end. + +Lemma topred_ok: + forall k a m rd, + reduction_ok a m rd -> + k = reduction_kind rd -> + reducts_ok k a m (topred rd). +Proof. + intros. unfold topred; red. simpl; intros. destruct H1; try contradiction. + inv H1. split. auto. exists a; auto. +Qed. + +Lemma incontext_ok: + forall k a m C res k' a', + reducts_ok k' a' m res -> + a = C a' -> + context k' k C -> + match k' with LV => is_loc a' = None | RV => is_val a' = None end -> + reducts_ok k a m (incontext C res). +Proof. + unfold reducts_ok; intros. destruct res; simpl. destruct l. +(* res = Some nil *) + destruct k'; congruence. +(* res = Some nonempty-list *) + simpl map at 1. hnf. intros. + exploit list_in_map_inv; eauto. intros [[C1 rd1] [P Q]]. inv P. + exploit H; eauto. intros [U [a'' [V W]]]. + split. eapply context_compose; eauto. exists a''; split; auto. congruence. +(* res = None *) + auto. +Qed. + +Remark incontext2_inv: + forall {A1 A2 B: Type} (C1: A1 -> B) res1 (C2: A2 -> B) res2, + match incontext2 C1 res1 C2 res2 with + | None => res1 = None \/ res2 = None + | Some nil => res1 = Some nil /\ res2 = Some nil + | Some ll => + exists ll1, exists ll2, + res1 = Some ll1 /\ res2 = Some ll2 /\ + forall C rd, In (C, rd) ll -> + (exists C', C = (fun x => C1(C' x)) /\ In (C', rd) ll1) + \/ (exists C', C = (fun x => C2(C' x)) /\ In (C', rd) ll2) + end. +Proof. + intros. unfold incontext2. destruct res1 as [ll1|]; auto. destruct res2 as [ll2|]; auto. + set (ll := map + (fun z : (expr -> A1) * reduction => + (fun x : expr => C1 (fst z x), snd z)) ll1 ++ + map + (fun z : (expr -> A2) * reduction => + (fun x : expr => C2 (fst z x), snd z)) ll2). + destruct ll as []_eqn. + destruct (app_eq_nil _ _ Heql). + split. destruct ll1; auto || discriminate. destruct ll2; auto || discriminate. + rewrite <- Heql. exists ll1; exists ll2. split. auto. split. auto. + unfold ll; intros. + rewrite in_app in H. destruct H. + exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. + left; exists C'; auto. + exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P. + right; exists C'; auto. +Qed. + +Lemma incontext2_ok: + forall k a m k1 a1 res1 k2 a2 res2 C1 C2, + reducts_ok k1 a1 m res1 -> + reducts_ok k2 a2 m res2 -> + a = C1 a1 -> a = C2 a2 -> + context k1 k C1 -> context k2 k C2 -> + match k1 with LV => is_loc a1 = None | RV => is_val a1 = None end + \/ match k2 with LV => is_loc a2 = None | RV => is_val a2 = None end -> + reducts_ok k a m (incontext2 C1 res1 C2 res2). +Proof. + unfold reducts_ok; intros. + generalize (incontext2_inv C1 res1 C2 res2). + destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto. + destruct ll. + intros [EQ1 EQ2]. subst. destruct H5. destruct k1; congruence. destruct k2; congruence. + intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. + exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst. + destruct ll1; try contradiction. exploit H; eauto. + intros [U [a' [V W]]]. split. eauto. exists a'; split. congruence. auto. + destruct ll2; try contradiction. exploit H0; eauto. + intros [U [a' [V W]]]. split. eauto. exists a'; split. congruence. auto. +Qed. + +Lemma incontext2_list_ok: + forall a1 a2 ty m res1 res2, + reducts_ok RV a1 m res1 -> + list_reducts_ok a2 m res2 -> + is_val a1 = None \/ is_val_list a2 = None -> + reducts_ok RV (Ecall a1 a2 ty) m + (incontext2 (fun x => Ecall x a2 ty) res1 + (fun x => Ecall a1 x ty) res2). +Proof. + unfold reducts_ok, list_reducts_ok; intros. + set (C1 := fun x => Ecall x a2 ty). set (C2 := fun x => Ecall a1 x ty). + generalize (incontext2_inv C1 res1 C2 res2). + destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto. + destruct ll. + intros [EQ1 EQ2]. subst. intuition congruence. + intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. + exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst. + destruct ll1; try contradiction. exploit H; eauto. + intros [U [a' [V W]]]. split. unfold C1. auto. exists a'; split. unfold C1; congruence. auto. + destruct ll2; try contradiction. exploit H0; eauto. + intros [U [a' [V W]]]. split. unfold C2. auto. exists a'; split. unfold C2; congruence. auto. +Qed. + +Lemma incontext2_list_ok': + forall a1 a2 m res1 res2, + reducts_ok RV a1 m res1 -> + list_reducts_ok a2 m res2 -> + list_reducts_ok (Econs a1 a2) m + (incontext2 (fun x => Econs x a2) res1 + (fun x => Econs a1 x) res2). +Proof. + unfold reducts_ok, list_reducts_ok; intros. + set (C1 := fun x => Econs x a2). set (C2 := fun x => Econs a1 x). + generalize (incontext2_inv C1 res1 C2 res2). + destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto. + destruct ll. + intros [EQ1 EQ2]. subst. + simpl. destruct (is_val a1); try congruence. destruct (is_val_list a2); congruence. + intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. + exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst. + destruct ll1; try contradiction. exploit H; eauto. + intros [U [a' [V W]]]. split. unfold C1. auto. exists a'; split. unfold C1; congruence. auto. + destruct ll2; try contradiction. exploit H0; eauto. + intros [U [a' [V W]]]. split. unfold C2. auto. exists a'; split. unfold C2; congruence. auto. +Qed. + +Ltac mysimpl := + match goal with + | [ |- reducts_ok _ _ _ (match ?x with Some _ => _ | None => None end) ] => + destruct x as []_eqn; [mysimpl|exact I] + | [ |- reducts_ok _ _ _ (match ?x with left _ => _ | right _ => None end) ] => + destruct x as []_eqn; [subst;mysimpl|exact I] + | _ => + idtac + end. + +Theorem step_expr_sound: + forall a k m, reducts_ok k a m (step_expr k a m) +with step_exprlist_sound: + forall al m, list_reducts_ok al m (step_exprlist al m). +Proof with try (exact I). + induction a; destruct k; intros; simpl... +(* Eval *) + congruence. +(* Evar *) + destruct (e!x) as [[b ty'] | ]_eqn; mysimpl. + apply topred_ok; auto. apply red_var_local; auto. + apply topred_ok; auto. apply red_var_global; auto. +(* Efield *) + destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. + destruct ty'... + (* top struct *) + destruct (field_offset f f0) as [delta|]_eqn... + rewrite (is_loc_inv _ _ _ _ Heqo). apply topred_ok; auto. apply red_field_struct; auto. + (* top union *) + rewrite (is_loc_inv _ _ _ _ Heqo). apply topred_ok; auto. apply red_field_union; auto. + (* in depth *) + eapply incontext_ok; eauto. +(* Evalof *) + destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. rewrite (is_loc_inv _ _ _ _ Heqo). apply red_rvalof; auto. + (* depth *) + eapply incontext_ok; eauto. +(* Ederef *) + destruct (is_val a) as [[v ty'] | ]_eqn. + (* top *) + destruct v... mysimpl. apply topred_ok; auto. rewrite (is_val_inv _ _ _ Heqo). apply red_deref; auto. + (* depth *) + eapply incontext_ok; eauto. +(* Eaddrof *) + destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. + (* top *) + apply topred_ok; auto. rewrite (is_loc_inv _ _ _ _ Heqo). apply red_addrof; auto. + (* depth *) + eapply incontext_ok; eauto. +(* unop *) + destruct (is_val a) as [[v ty'] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. rewrite (is_val_inv _ _ _ Heqo). apply red_unop; auto. + (* depth *) + eapply incontext_ok; eauto. +(* binop *) + destruct (is_val a1) as [[v1 ty1] | ]_eqn. + destruct (is_val a2) as [[v2 ty2] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. + rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). apply red_binop; auto. + (* depth *) + eapply incontext2_ok; eauto. + eapply incontext2_ok; eauto. +(* cast *) + destruct (is_val a) as [[v ty'] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. + rewrite (is_val_inv _ _ _ Heqo). apply red_cast; auto. + (* depth *) + eapply incontext_ok; eauto. +(* condition *) + destruct (is_val a1) as [[v ty'] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. + rewrite (is_val_inv _ _ _ Heqo). eapply red_condition; eauto. + (* depth *) + eapply incontext_ok; eauto. +(* sizeof *) + apply topred_ok; auto. apply red_sizeof. +(* assign *) + destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. + destruct (is_val a2) as [[v2 ty2] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. + rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). apply red_assign; auto. + (* depth *) + eapply incontext2_ok; eauto. + eapply incontext2_ok; eauto. +(* assignop *) + destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn. + destruct (is_val a2) as [[v2 ty2] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. + rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). eapply red_assignop; eauto. + (* depth *) + eapply incontext2_ok; eauto. + eapply incontext2_ok; eauto. +(* postincr *) + destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. + rewrite (is_loc_inv _ _ _ _ Heqo). eapply red_postincr; eauto. + (* depth *) + eapply incontext_ok; eauto. +(* comma *) + destruct (is_val a1) as [[v ty'] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. + rewrite (is_val_inv _ _ _ Heqo). apply red_comma; auto. + (* depth *) + eapply incontext_ok; eauto. +(* call *) + destruct (is_val a) as [[vf tyf] | ]_eqn. + destruct (is_val_list rargs) as [vtl | ]_eqn. + (* top *) + destruct (classify_fun tyf) as [tyargs tyres|]_eqn... + mysimpl. apply topred_ok; auto. + rewrite (is_val_inv _ _ _ Heqo). red. split; auto. eapply red_Ecall; eauto. + eapply sem_cast_arguments_sound; eauto. + (* depth *) + eapply incontext2_list_ok; eauto. + eapply incontext2_list_ok; eauto. +(* loc *) + congruence. +(* paren *) + destruct (is_val a) as [[v ty'] | ]_eqn. + (* top *) + mysimpl. apply topred_ok; auto. + rewrite (is_val_inv _ _ _ Heqo). apply red_paren; auto. + (* depth *) + eapply incontext_ok; eauto. + + induction al; simpl; intros. +(* nil *) + congruence. +(* cons *) + eapply incontext2_list_ok'; eauto. +Qed. + + +Lemma step_exprlist_val_list: + forall m al, is_val_list al <> None -> step_exprlist al m = Some nil. +Proof. + induction al; simpl; intros. + auto. + destruct (is_val r1) as [[v1 ty1]|]_eqn; try congruence. + destruct (is_val_list al) as []_eqn; try congruence. + rewrite (is_val_inv _ _ _ Heqo). + rewrite IHal. auto. congruence. +Qed. + +(** Completeness, part 1: if [step_expr] returns [Some ll], + then [ll] contains all possible reducts. *) + +Lemma lred_topred: + forall l1 m1 l2 m2, + lred ge e l1 m1 l2 m2 -> + step_expr LV l1 m1 = topred (Lred l2 m2). +Proof. + induction 1; simpl. +(* var local *) + rewrite H. rewrite dec_eq_true; auto. +(* var global *) + rewrite H; rewrite H0; rewrite H1. rewrite dec_eq_true; auto. +(* deref *) + auto. +(* field struct *) + rewrite H; auto. +(* field union *) + auto. +Qed. + +Lemma rred_topred: + forall r1 m1 r2 m2, + rred r1 m1 r2 m2 -> + step_expr RV r1 m1 = topred (Rred r2 m2). +Proof. + induction 1; simpl. +(* valof *) + rewrite dec_eq_true; auto. rewrite H; auto. +(* addrof *) + auto. +(* unop *) + rewrite H; auto. +(* binop *) + rewrite H; auto. +(* cast *) + rewrite H; auto. +(* condition *) + rewrite H; auto. +(* sizeof *) + auto. +(* assign *) + rewrite dec_eq_true; auto. rewrite H; rewrite H0; auto. +(* assignop *) + rewrite dec_eq_true; auto. rewrite H; rewrite H0; rewrite H1; rewrite H2; auto. +(* postincr *) + rewrite dec_eq_true; auto. rewrite H; rewrite H0; rewrite H1; rewrite H2; auto. +(* comma *) + rewrite H; rewrite dec_eq_true; auto. +(* paren *) + rewrite H; auto. +Qed. + +Lemma sem_cast_arguments_complete: + forall al tyl vl, + cast_arguments al tyl vl -> + exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl. +Proof. + induction 1. + exists (@nil (val * type)); auto. + destruct IHcast_arguments as [vtl [A B]]. + exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto. +Qed. + +Lemma callred_topred: + forall a fd args ty m, + callred ge a fd args ty -> + step_expr RV a m = topred (Callred fd args ty m). +Proof. + induction 1; simpl. + rewrite H2. exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. + rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. auto. +Qed. + +Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop := + match res1, res2 with + | Some ll1, Some ll2 => + forall C1 rd, In (C1, rd) ll1 -> In ((fun x => C(C1 x)), rd) ll2 + | None, Some ll2 => False + | _, None => True + end. + +Lemma reducts_incl_trans: + forall (A1 A2: Type) (C: A1 -> A2) res1 res2, reducts_incl C res1 res2 -> + forall (A3: Type) (C': A2 -> A3) res3, + reducts_incl C' res2 res3 -> + reducts_incl (fun x => C'(C x)) res1 res3. +Proof. + unfold reducts_incl; intros. destruct res1; destruct res2; destruct res3; auto. contradiction. +Qed. + +Lemma reducts_incl_nil: + forall (A B: Type) (C: A -> B) res, + reducts_incl C (Some nil) res. +Proof. + intros; red. destruct res; auto. intros; contradiction. +Qed. + +Lemma reducts_incl_val: + forall (A: Type) a m v ty (C: expr -> A) res, + is_val a = Some(v, ty) -> reducts_incl C (step_expr RV a m) res. +Proof. + intros. rewrite (is_val_inv _ _ _ H). apply reducts_incl_nil. +Qed. + +Lemma reducts_incl_loc: + forall (A: Type) a m b ofs ty (C: expr -> A) res, + is_loc a = Some(b, ofs, ty) -> reducts_incl C (step_expr LV a m) res. +Proof. + intros. rewrite (is_loc_inv _ _ _ _ H). apply reducts_incl_nil. +Qed. + +Lemma reducts_incl_listval: + forall (A: Type) a m vtl (C: exprlist -> A) res, + is_val_list a = Some vtl -> reducts_incl C (step_exprlist a m) res. +Proof. + intros. rewrite step_exprlist_val_list. apply reducts_incl_nil. congruence. +Qed. + +Lemma reducts_incl_incontext: + forall (A B: Type) (C: A -> B) res, + reducts_incl C res (incontext C res). +Proof. + intros; unfold reducts_incl. destruct res; simpl; auto. + intros. set (f := fun z : (expr -> A) * reduction => (fun x : expr => C (fst z x), snd z)). + change (In (f (C1, rd)) (map f l)). apply in_map. auto. +Qed. + +Lemma reducts_incl_incontext2_left: + forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2, + reducts_incl C1 res1 (incontext2 C1 res1 C2 res2). +Proof. + intros. destruct res1; simpl; auto. destruct res2; auto. + intros. rewrite in_app_iff. left. + set (f := fun z : (expr -> A1) * reduction => (fun x : expr => C1 (fst z x), snd z)). + change (In (f (C0, rd)) (map f l)). apply in_map; auto. +Qed. + +Lemma reducts_incl_incontext2_right: + forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2, + reducts_incl C2 res2 (incontext2 C1 res1 C2 res2). +Proof. + intros. destruct res1; destruct res2; simpl; auto. + intros. rewrite in_app_iff. right. + set (f := fun z : (expr -> A2) * reduction => (fun x : expr => C2 (fst z x), snd z)). + change (In (f (C0, rd)) (map f l0)). apply in_map; auto. +Qed. + +Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval + reducts_incl_incontext reducts_incl_incontext2_left reducts_incl_incontext2_right. + +Lemma step_expr_context: + forall from to C, context from to C -> + forall a m, reducts_incl C (step_expr from a m) (step_expr to (C a) m) +with step_exprlist_context: + forall from C, contextlist from C -> + forall a m, reducts_incl C (step_expr from a m) (step_exprlist (C a) m). +Proof. + induction 1; simpl; intros. +(* top *) + red. destruct (step_expr k a m); auto. intros. + replace (fun x => C1 x) with C1; auto. apply extensionality; auto. +(* deref *) + eapply reducts_incl_trans with (C' := fun x => Ederef x ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* field *) + eapply reducts_incl_trans with (C' := fun x => Efield x f ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* valof *) + eapply reducts_incl_trans with (C' := fun x => Evalof x ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* addrof *) + eapply reducts_incl_trans with (C' := fun x => Eaddrof x ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* unop *) + eapply reducts_incl_trans with (C' := fun x => Eunop op x ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* binop left *) + eapply reducts_incl_trans with (C' := fun x => Ebinop op x e2 ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* binop right *) + eapply reducts_incl_trans with (C' := fun x => Ebinop op e1 x ty); eauto. + destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. + destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. +(* cast *) + eapply reducts_incl_trans with (C' := fun x => Ecast x ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* condition *) + eapply reducts_incl_trans with (C' := fun x => Econdition x r2 r3 ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* assign left *) + eapply reducts_incl_trans with (C' := fun x => Eassign x e2 ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* assign right *) + eapply reducts_incl_trans with (C' := fun x => Eassign e1 x ty); eauto. + destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto. + destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. +(* assignop left *) + eapply reducts_incl_trans with (C' := fun x => Eassignop op x e2 tyres ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* assignop right *) + eapply reducts_incl_trans with (C' := fun x => Eassignop op e1 x tyres ty); eauto. + destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto. + destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto. +(* postincr *) + eapply reducts_incl_trans with (C' := fun x => Epostincr id x ty); eauto. + destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto. +(* call left *) + eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* call right *) + eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. + destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto. + destruct (is_val_list (C a)) as [vl|]_eqn; eauto. +(* comma *) + eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. +(* paren *) + eapply reducts_incl_trans with (C' := fun x => Eparen x ty); eauto. + destruct (is_val (C a)) as [[v ty']|]_eqn; eauto. + + induction 1; simpl; intros. +(* cons left *) + eapply reducts_incl_trans with (C' := fun x => Econs x el). + apply step_expr_context; eauto. eauto. +(* binop right *) + eapply reducts_incl_trans with (C' := fun x => Econs e1 x). + apply step_exprlist_context; eauto. eauto. +Qed. + +(** Completeness, part 2: given a safe expression, [step_expr] does not return [None]. *) + +Lemma topred_none: + forall rd, topred rd <> None. +Proof. + intros; unfold topred; congruence. +Qed. + +Lemma incontext_none: + forall (A B: Type) (C: A -> B) rds, + rds <> None -> incontext C rds <> None. +Proof. + unfold incontext; intros. destruct rds; congruence. +Qed. + +Lemma incontext2_none: + forall (A1 A2 B: Type) (C1: A1 -> B) rds1 (C2: A2 -> B) rds2, + rds1 <> None -> rds2 <> None -> incontext2 C1 rds1 C2 rds2 <> None. +Proof. + unfold incontext2; intros. destruct rds1; destruct rds2; congruence. +Qed. + +Lemma safe_expr_kind: + forall k C a m, + context k RV C -> + not_stuck ge e (C a) m -> + k = Cstrategy.expr_kind a. +Proof. + intros. + symmetry. eapply Cstrategy.not_imm_stuck_kind; eauto. +Qed. + +Lemma safe_inversion: + forall k C a m, + context k RV C -> + not_stuck ge e (C a) m -> + match a with + | Eloc _ _ _ => True + | Eval _ _ => True + | _ => Cstrategy.invert_expr_prop ge e a m + end. +Proof. + intros. eapply Cstrategy.not_imm_stuck_inv; eauto. +Qed. + +Lemma is_val_list_all_values: + forall al vtl, is_val_list al = Some vtl -> Cstrategy.exprlist_all_values al. +Proof. + induction al; simpl; intros. auto. + destruct (is_val r1) as [[v ty]|]_eqn; try discriminate. + destruct (is_val_list al) as [vtl'|]_eqn; try discriminate. + rewrite (is_val_inv _ _ _ Heqo). eauto. +Qed. + +Theorem step_expr_defined: + forall a k m C, + context k RV C -> + not_stuck ge e (C a) m -> + step_expr k a m <> None +with step_exprlist_defined: + forall al m C, + Cstrategy.contextlist' C -> + not_stuck ge e (C al) m -> + step_exprlist al m <> None. +Proof. + induction a; intros k m C CTX NS; + rewrite (safe_expr_kind _ _ _ _ CTX NS); + rewrite (safe_expr_kind _ _ _ _ CTX NS) in CTX; + simpl in *; + generalize (safe_inversion _ _ _ _ CTX NS); intro INV. +(* val *) + congruence. +(* var *) + red in INV. destruct INV as [b [P | [P [Q R]]]]. + rewrite P; rewrite dec_eq_true. apply topred_none. + rewrite P; rewrite Q; rewrite R; rewrite dec_eq_true. apply topred_none. +(* field *) + destruct (is_loc a) as [[[b ofs] ty']|]_eqn. + rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. + destruct ty'; try contradiction. destruct INV as [delta EQ]. rewrite EQ. apply topred_none. + apply topred_none. + apply incontext_none. apply IHa with (C := fun x => C(Efield x f ty)); eauto. +(* valof *) + destruct (is_loc a) as [[[b ofs] ty']|]_eqn. + rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. destruct INV as [EQ [v LD]]. subst. + rewrite dec_eq_true; rewrite LD; apply topred_none. + apply incontext_none. apply IHa with (C := fun x => C(Evalof x ty)); eauto. +(* deref *) + destruct (is_val a) as [[v ty']|]_eqn. + rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [b [ofs EQ]]. subst. + apply topred_none. + apply incontext_none. apply IHa with (C := fun x => C(Ederef x ty)); eauto. +(* addrof *) + destruct (is_loc a) as [[[b ofs] ty']|]_eqn. + apply topred_none. + apply incontext_none. apply IHa with (C := fun x => C(Eaddrof x ty)); eauto. +(* unop *) + destruct (is_val a) as [[v1 ty1]|]_eqn. + rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ]. + rewrite EQ; apply topred_none. + apply incontext_none. apply IHa with (C := fun x => C(Eunop op x ty)); eauto. +(* binop *) + destruct (is_val a1) as [[v1 ty1]|]_eqn. + destruct (is_val a2) as [[v2 ty2]|]_eqn. + rewrite (is_val_inv _ _ _ Heqo) in INV. + rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. destruct INV as [v EQ]. + rewrite EQ; apply topred_none. + apply incontext2_none. apply IHa1 with (C := fun x => C(Ebinop op x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Ebinop op a1 x ty)); eauto. + apply incontext2_none. apply IHa1 with (C := fun x => C(Ebinop op x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Ebinop op a1 x ty)); eauto. +(* cast *) + destruct (is_val a) as [[v1 ty1]|]_eqn. + rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ]. + rewrite EQ; apply topred_none. + apply incontext_none. apply IHa with (C := fun x => C(Ecast x ty)); eauto. +(* condition *) + destruct (is_val a1) as [[v1 ty1]|]_eqn. + rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ]. + rewrite EQ; apply topred_none. + apply incontext_none. apply IHa1 with (C := fun x => C(Econdition x a2 a3 ty)); eauto. +(* sizeof *) + apply topred_none. +(* assign *) + destruct (is_loc a1) as [[[b ofs] ty1]|]_eqn. + destruct (is_val a2) as [[v2 ty2]|]_eqn. + rewrite (is_loc_inv _ _ _ _ Heqo) in INV. + rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. + destruct INV as [v [m' [P [Q R]]]]. + subst. rewrite dec_eq_true; rewrite Q; rewrite R; apply topred_none. + apply incontext2_none. apply IHa1 with (C := fun x => C(Eassign x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Eassign a1 x ty)); eauto. + apply incontext2_none. apply IHa1 with (C := fun x => C(Eassign x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Eassign a1 x ty)); eauto. +(* assignop *) + destruct (is_loc a1) as [[[b ofs] ty1]|]_eqn. + destruct (is_val a2) as [[v2 ty2]|]_eqn. + rewrite (is_loc_inv _ _ _ _ Heqo) in INV. + rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. + destruct INV as [v1 [v [v' [m' [P [Q [R [S T]]]]]]]]. + subst. rewrite dec_eq_true; rewrite Q; rewrite R; rewrite S; rewrite T; apply topred_none. + apply incontext2_none. apply IHa1 with (C := fun x => C(Eassignop op x a2 tyres ty)); eauto. apply IHa2 with (C := fun x => C(Eassignop op a1 x tyres ty)); eauto. + apply incontext2_none. apply IHa1 with (C := fun x => C(Eassignop op x a2 tyres ty)); eauto. apply IHa2 with (C := fun x => C(Eassignop op a1 x tyres ty)); eauto. +(* postincr *) + destruct (is_loc a) as [[[b ofs] ty1]|]_eqn. + rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. + destruct INV as [v1 [v2 [v3 [m' [P [Q [R [S T]]]]]]]]. + subst. rewrite dec_eq_true; rewrite Q; rewrite R; rewrite S; rewrite T; apply topred_none. + apply incontext_none. apply IHa with (C := fun x => C(Epostincr id x ty)); eauto. +(* comma *) + destruct (is_val a1) as [[v1 ty1]|]_eqn. + rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. rewrite INV. + rewrite dec_eq_true; apply topred_none. + apply incontext_none. apply IHa1 with (C := fun x => C(Ecomma x a2 ty)); eauto. +(* call *) + destruct (is_val a) as [[vf tyf]|]_eqn. + destruct (is_val_list rargs) as [vtl|]_eqn. + rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. + destruct INV as [tyargs [tyres [fd [vl [P [Q [R S]]]]]]]. + eapply is_val_list_all_values; eauto. + rewrite P; rewrite Q. + exploit sem_cast_arguments_complete; eauto. intros [vtl' [U V]]. + assert (vtl' = vtl) by congruence. subst. rewrite V. rewrite S. rewrite dec_eq_true. + apply topred_none. + apply incontext2_none. apply IHa with (C := fun x => C(Ecall x rargs ty)); eauto. + apply step_exprlist_defined with (C := fun x => C(Ecall a x ty)); auto. + apply Cstrategy.contextlist'_intro with (rl0 := Enil). auto. + apply incontext2_none. apply IHa with (C := fun x => C(Ecall x rargs ty)); eauto. + apply step_exprlist_defined with (C := fun x => C(Ecall a x ty)); auto. + apply Cstrategy.contextlist'_intro with (rl0 := Enil). auto. +(* loc *) + congruence. +(* paren *) + destruct (is_val a) as [[v1 ty1]|]_eqn. + rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ]. + rewrite EQ; apply topred_none. + apply incontext_none. apply IHa with (C := fun x => C(Eparen x ty)); eauto. + + induction al; intros; simpl. +(* nil *) + congruence. +(* cons *) + apply incontext2_none. + apply step_expr_defined with (C := fun x => C(Econs x al)); eauto. + apply Cstrategy.contextlist'_head; auto. + apply IHal with (C := fun x => C(Econs r1 x)); auto. + apply Cstrategy.contextlist'_tail; auto. +Qed. + +(** Connections between [not_stuck] and [step_expr]. *) + +Lemma step_expr_not_imm_stuck: + forall k a m, + step_expr k a m <> None -> + not_imm_stuck ge e k a m. +Proof. + intros. generalize (step_expr_sound a k m). unfold reducts_ok. + destruct (step_expr k a m) as [ll|]. destruct ll. +(* value or location *) + destruct k; destruct a; simpl; intros; try congruence. + apply not_stuck_loc. + apply Csem.not_stuck_val. +(* reducible *) + intros R. destruct p as [C1 rd1]. destruct (R C1 rd1) as [P [a' [U V]]]; auto with coqlib. + subst a. red in V. destruct rd1. + eapply not_stuck_lred; eauto. + eapply not_stuck_rred; eauto. + destruct V. subst m'. eapply not_stuck_callred; eauto. +(* stuck *) + congruence. +Qed. + +Lemma step_expr_not_stuck: + forall a m, + step_expr RV a m <> None -> + not_stuck ge e a m. +Proof. + intros; red; intros. subst a. + apply step_expr_not_imm_stuck. + generalize (step_expr_context _ _ C H0 e' m). unfold reducts_incl. + destruct (step_expr k e' m). congruence. + destruct (step_expr RV (C e') m). tauto. congruence. +Qed. + +Lemma not_stuck_step_expr: + forall a m, + not_stuck ge e a m -> + step_expr RV a m <> None. +Proof. + intros. apply step_expr_defined with (C := fun x => x); auto. +Qed. + +End EXPRS. + +(** * External functions and events. *) + +Section EVENTS. + +Variable F V: Type. +Variable genv: Genv.t F V. + +Definition eventval_of_val (v: val) (t: typ) : option eventval := + match v, t with + | Vint i, AST.Tint => Some (EVint i) + | Vfloat f, AST.Tfloat => Some (EVfloat f) + | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol genv b; Some (EVptr_global id ofs) + | _, _ => None + end. + +Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) := + match vl, tl with + | nil, nil => Some nil + | v1::vl, t1::tl => + do ev1 <- eventval_of_val v1 t1; + do evl <- list_eventval_of_val vl tl; + Some (ev1 :: evl) + | _, _ => None + end. + +Definition val_of_eventval (ev: eventval) (t: typ) : option val := + match ev, t with + | EVint i, AST.Tint => Some (Vint i) + | EVfloat f, AST.Tfloat => Some (Vfloat f) + | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol genv id; Some (Vptr b ofs) + | _, _ => None + end. + +Lemma eventval_of_val_sound: + forall v t ev, eventval_of_val v t = Some ev -> eventval_match genv ev t v. +Proof. + intros. destruct v; destruct t; simpl in H; inv H. + constructor. + constructor. + destruct (Genv.invert_symbol genv b) as [id|]_eqn; inv H1. + constructor. apply Genv.invert_find_symbol; auto. +Qed. + +Lemma eventval_of_val_complete: + forall ev t v, eventval_match genv ev t v -> eventval_of_val v t = Some ev. +Proof. + induction 1; simpl; auto. + rewrite (Genv.find_invert_symbol _ _ H). auto. +Qed. + +Lemma list_eventval_of_val_sound: + forall vl tl evl, list_eventval_of_val vl tl = Some evl -> eventval_list_match genv evl tl vl. +Proof with try discriminate. + induction vl; destruct tl; simpl; intros; inv H. + constructor. + destruct (eventval_of_val a t) as [ev1|]_eqn... + destruct (list_eventval_of_val vl tl) as [evl'|]_eqn... + inv H1. constructor. apply eventval_of_val_sound; auto. eauto. +Qed. + +Lemma list_eventval_of_val_complete: + forall evl tl vl, eventval_list_match genv evl tl vl -> list_eventval_of_val vl tl = Some evl. +Proof. + induction 1; simpl. auto. + rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto. +Qed. + +Lemma val_of_eventval_sound: + forall ev t v, val_of_eventval ev t = Some v -> eventval_match genv ev t v. +Proof. + intros. destruct ev; destruct t; simpl in H; inv H. + constructor. + constructor. + destruct (Genv.find_symbol genv i) as [b|]_eqn; inv H1. + constructor. auto. +Qed. + +Lemma val_of_eventval_complete: + forall ev t v, eventval_match genv ev t v -> val_of_eventval ev t = Some v. +Proof. + induction 1; simpl; auto. rewrite H; auto. +Qed. + +(** System calls and library functions *) + +Definition do_ef_external (name: ident) (sg: signature) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + do args <- list_eventval_of_val vargs (sig_args sg); + match nextworld_io w name args with + | None => None + | Some(res, w') => + do vres <- val_of_eventval res (proj_sig_res sg); + Some(w', Event_syscall name args res :: E0, vres, m) + end. + +Definition do_ef_volatile_load (chunk: memory_chunk) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vptr b ofs :: nil => + if block_is_volatile genv b then + do id <- Genv.invert_symbol genv b; + match nextworld_vload w chunk id ofs with + | None => None + | Some(res, w') => + do vres <- val_of_eventval res (type_of_chunk chunk); + Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres, m) + end + else + do v <- Mem.load chunk m b (Int.unsigned ofs); + Some(w, E0, v, m) + | _ => None + end. + +Definition do_ef_volatile_store (chunk: memory_chunk) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vptr b ofs :: v :: nil => + if block_is_volatile genv b then + do id <- Genv.invert_symbol genv b; + do ev <- eventval_of_val v (type_of_chunk chunk); + do w' <- nextworld_vstore w chunk id ofs ev; + Some(w', Event_vstore chunk id ofs ev :: nil, Vundef, m) + else + do m' <- Mem.store chunk m b (Int.unsigned ofs) v; + Some(w, E0, Vundef, m') + | _ => None + end. + +Definition do_ef_malloc + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vint n :: nil => + let (m', b) := Mem.alloc m (-4) (Int.unsigned n) in + do m'' <- Mem.store Mint32 m' b (-4) (Vint n); + Some(w, E0, Vptr b Int.zero, m'') + | _ => None + end. + +Definition do_ef_free + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vptr b lo :: nil => + do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4); + match vsz with + | Vint sz => + check (zlt 0 (Int.unsigned sz)); + do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz); + Some(w, E0, Vundef, m') + | _ => None + end + | _ => None + end. + +Definition memcpy_args_ok + (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop := + (al = 1 \/ al = 2 \/ al = 4) + /\ sz > 0 + /\ (al | sz) /\ (al | osrc) /\ (al | odst) + /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc). + +Remark memcpy_check_args: + forall sz al bdst odst bsrc osrc, + {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}. +Proof with try (right; intuition omega). + intros. + assert (X: {al = 1 \/ al = 2 \/ al = 4} + {~(al = 1 \/ al = 2 \/ al = 4)}). + destruct (zeq al 1); auto. destruct (zeq al 2); auto. destruct (zeq al 4); auto... + unfold memcpy_args_ok. destruct X... + assert (al > 0) by (intuition omega). + destruct (zlt 0 sz)... + destruct (Zdivide_dec al sz); auto... + destruct (Zdivide_dec al osrc); auto... + destruct (Zdivide_dec al odst); auto... + assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc} + +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}). + destruct (eq_block bsrc bdst); auto. + destruct (zeq osrc odst); auto. + destruct (zle (osrc + sz) odst); auto. + destruct (zle (odst + sz) osrc); auto. + right; intuition omega. + destruct Y... left; intuition omega. +Qed. + +Definition do_ef_memcpy (sz al: Z) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vptr bdst odst :: Vptr bsrc osrc :: nil => + if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then + do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz; + do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes; + Some(w, E0, Vundef, m') + else None + | _ => None + end. + +Definition do_ef_annot (text: ident) (targs: list typ) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + do args <- list_eventval_of_val vargs targs; + Some(w, Event_annot text args :: E0, Vundef, m). + +Definition do_ef_annot_val (text: ident) (targ: typ) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | varg :: nil => + do arg <- eventval_of_val varg targ; + Some(w, Event_annot text (arg :: nil) :: E0, varg, m) + | _ => None + end. + +Definition do_external (ef: external_function): + world -> list val -> mem -> option (world * trace * val * mem) := + match ef with + | EF_external name sg => do_ef_external name sg + | EF_builtin name sg => do_ef_external name sg + | EF_vload chunk => do_ef_volatile_load chunk + | EF_vstore chunk => do_ef_volatile_store chunk + | EF_malloc => do_ef_malloc + | EF_free => do_ef_free + | EF_memcpy sz al => do_ef_memcpy sz al + | EF_annot text targs => do_ef_annot text targs + | EF_annot_val text targ => do_ef_annot_val text targ + end. + +Ltac mydestr := + match goal with + | [ |- None = Some _ -> _ ] => intro X; discriminate + | [ |- Some _ = Some _ -> _ ] => intro X; inv X + | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr + | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr + | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr + | _ => idtac + end. + +Lemma do_ef_external_sound: + forall ef w vargs m w' t vres m', + do_external ef w vargs m = Some(w', t, vres, m') -> + external_call ef genv vargs m t vres m' /\ possible_trace w t w'. +Proof with try congruence. + intros until m'. + assert (IO: forall name sg, + do_ef_external name sg w vargs m = Some(w', t, vres, m') -> + extcall_io_sem name sg genv vargs m t vres m' /\ possible_trace w t w'). + intros until sg. unfold do_ef_external. mydestr. destruct p as [res w'']; mydestr. + split. econstructor. apply list_eventval_of_val_sound; auto. + apply val_of_eventval_sound; auto. + econstructor. constructor; eauto. constructor. + + destruct ef; simpl. +(* EF_external *) + auto. +(* EF_builtin *) + auto. +(* EF_vload *) + unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... + mydestr. destruct p as [res w'']; mydestr. + split. constructor. apply Genv.invert_find_symbol; auto. auto. + apply val_of_eventval_sound; auto. + econstructor. constructor; eauto. constructor. + split. constructor; auto. constructor. +(* EF_vstore *) + unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... + mydestr. + split. constructor. apply Genv.invert_find_symbol; auto. auto. + apply eventval_of_val_sound; auto. + econstructor. constructor; eauto. constructor. + split. constructor; auto. constructor. +(* EF_malloc *) + unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs... + destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr. + split. econstructor; eauto. constructor. +(* EF_free *) + unfold do_ef_free. destruct vargs... destruct v... destruct vargs... + mydestr. destruct v... mydestr. + split. econstructor; eauto. omega. constructor. +(* EF_memcpy *) + unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... + destruct v... destruct vargs... mydestr. red in m0. + split. econstructor; eauto; tauto. constructor. +(* EF_annot *) + unfold do_ef_annot. mydestr. + split. constructor. apply list_eventval_of_val_sound; auto. + econstructor. constructor; eauto. constructor. +(* EF_annot_val *) + unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. + split. constructor. apply eventval_of_val_sound; auto. + econstructor. constructor; eauto. constructor. +Qed. + +Lemma do_ef_external_complete: + forall ef w vargs m w' t vres m', + external_call ef genv vargs m t vres m' -> possible_trace w t w' -> + do_external ef w vargs m = Some(w', t, vres, m'). +Proof. + intros. + assert (IO: forall name sg, + extcall_io_sem name sg genv vargs m t vres m' -> + do_ef_external name sg w vargs m = Some (w', t, vres, m')). + intros. inv H1. inv H0. inv H8. inv H6. + unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. + rewrite (val_of_eventval_complete _ _ _ H3). auto. + + destruct ef; simpl in *. +(* EF_external *) + auto. +(* EF_builtin *) + auto. +(* EF_vload *) + inv H; unfold do_ef_volatile_load. + inv H0. inv H8. inv H6. + rewrite H2. rewrite (Genv.find_invert_symbol _ _ H1). rewrite H9. + rewrite (val_of_eventval_complete _ _ _ H3). auto. + inv H0. rewrite H1. rewrite H2. auto. +(* EF_vstore *) + inv H; unfold do_ef_volatile_store. + inv H0. inv H8. inv H6. + rewrite H2. rewrite (Genv.find_invert_symbol _ _ H1). + rewrite (eventval_of_val_complete _ _ _ H3). rewrite H9. auto. + inv H0. rewrite H1. rewrite H2. auto. +(* EF_malloc *) + inv H; unfold do_ef_malloc. + inv H0. rewrite H1. rewrite H2. auto. +(* EF_free *) + inv H; unfold do_ef_free. + inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega. +(* EF_memcpy *) + inv H; unfold do_ef_memcpy. + inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto. + red. tauto. +(* EF_annot *) + inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. + rewrite (list_eventval_of_val_complete _ _ _ H1). auto. +(* EF_annot_val *) + inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. + rewrite (eventval_of_val_complete _ _ _ H1). auto. +Qed. + +End EVENTS. + +(** * Transitions over states. *) + +Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l} : env * mem := + match l with + | nil => (e,m) + | (id, ty) :: l' => + let (m1,b1) := Mem.alloc m 0 (sizeof ty) in + do_alloc_variables (PTree.set id (b1, ty) e) m1 l' +end. + +Lemma do_alloc_variables_sound: + forall l e m, alloc_variables e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)). +Proof. + induction l; intros; simpl. + constructor. + destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1]_eqn; simpl. + econstructor; eauto. +Qed. + +Lemma do_alloc_variables_complete: + forall e1 m1 l e2 m2, alloc_variables e1 m1 l e2 m2 -> + do_alloc_variables e1 m1 l = (e2, m2). +Proof. + induction 1; simpl. + auto. + rewrite H; rewrite IHalloc_variables; auto. +Qed. + +Function sem_bind_parameters (e: env) (m: mem) (l: list (ident * type)) (lv: list val) + {struct l} : option mem := + match l, lv with + | nil, nil => Some m + | (id, ty) :: params, v1::lv => + match PTree.get id e with + | Some (b, ty') => + check (type_eq ty ty'); + do m1 <- store_value_of_type ty m b Int.zero v1; + sem_bind_parameters e m1 params lv + | None => None + end + | _, _ => None +end. + +Lemma sem_bind_parameters_sound : forall e m l lv m', + sem_bind_parameters e m l lv = Some m' -> + bind_parameters e m l lv m'. +Proof. + intros; functional induction (sem_bind_parameters e m l lv); try discriminate. + inversion H; constructor; auto. + econstructor; eauto. +Qed. + +Lemma sem_bind_parameters_complete : forall e m l lv m', + bind_parameters e m l lv m' -> + sem_bind_parameters e m l lv = Some m'. +Proof. + induction 1; simpl; auto. + rewrite H. rewrite dec_eq_true. + destruct (store_value_of_type ty m b Int.zero v1); try discriminate. + inv H0; auto. +Qed. + +Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) := + match snd C_rd with + | Lred a m => (E0, ExprState f (fst C_rd a) k e m) + | Rred a m => (E0, ExprState f (fst C_rd a) k e m) + | Callred fd vargs ty m => (E0, Callstate fd vargs (Kcall f e (fst C_rd) ty k) m) + end. + +Local Open Scope list_monad_scope. + +Definition ret (S: state) : list (trace * state) := (E0, S) :: nil. + +Definition do_step (w: world) (s: state) : list (trace * state) := + match s with + + | ExprState f a k e m => + match is_val a with + | Some(v, ty) => + match k with + | Kdo k => ret (State f Sskip k e m ) + | Kifthenelse s1 s2 k => + do b <- bool_val v ty; ret (State f (if b then s1 else s2) k e m) + | Kwhile1 x s k => + do b <- bool_val v ty; + if b then ret (State f s (Kwhile2 x s k) e m) else ret (State f Sskip k e m) + | Kdowhile2 x s k => + do b <- bool_val v ty; + if b then ret (State f (Sdowhile x s) k e m) else ret (State f Sskip k e m) + | Kfor2 a2 a3 s k => + do b <- bool_val v ty; + if b then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m) + | Kreturn k => + do v' <- sem_cast v ty f.(fn_return); + do m' <- Mem.free_list m (blocks_of_env e); + ret (Returnstate v' (call_cont k) m') + | Kswitch1 sl k => + match v with + | Vint n => ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) + | _ => nil + end + | _ => nil + end + + | None => + match step_expr e RV a m with + | None => nil + | Some ll => map (expr_final_state f k e) ll + end + end + + | State f (Sdo x) k e m => ret(ExprState f x (Kdo k) e m) + + | State f (Ssequence s1 s2) k e m => ret(State f s1 (Kseq s2 k) e m) + | State f Sskip (Kseq s k) e m => ret (State f s k e m) + | State f Scontinue (Kseq s k) e m => ret (State f Scontinue k e m) + | State f Sbreak (Kseq s k) e m => ret (State f Sbreak k e m) + + | State f (Sifthenelse a s1 s2) k e m => ret (ExprState f a (Kifthenelse s1 s2 k) e m) + + | State f (Swhile x s) k e m => ret (ExprState f x (Kwhile1 x s k) e m) + | State f (Sskip|Scontinue) (Kwhile2 x s k) e m => ret (State f (Swhile x s) k e m) + | State f Sbreak (Kwhile2 x s k) e m => ret (State f Sskip k e m) + + | State f (Sdowhile a s) k e m => ret (State f s (Kdowhile1 a s k) e m) + | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m => ret (ExprState f x (Kdowhile2 x s k) e m) + | State f Sbreak (Kdowhile1 x s k) e m => ret (State f Sskip k e m) + + | State f (Sfor a1 a2 a3 s) k e m => + if is_skip a1 + then ret (ExprState f a2 (Kfor2 a2 a3 s k) e m) + else ret (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) + | State f Sskip (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m) + | State f Scontinue (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m) + | State f Sbreak (Kfor3 a2 a3 s k) e m => ret (State f Sskip k e m) + | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m) + + | State f (Sreturn None) k e m => + do m' <- Mem.free_list m (blocks_of_env e); + ret (Returnstate Vundef (call_cont k) m') + | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m) + | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => + check (type_eq f.(fn_return) Tvoid); + do m' <- Mem.free_list m (blocks_of_env e); + ret (Returnstate Vundef k m') + + | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m) + | State f (Sskip|Sbreak) (Kswitch2 k) e m => ret (State f Sskip k e m) + | State f Scontinue (Kswitch2 k) e m => ret (State f Scontinue k e m) + + | State f (Slabel lbl s) k e m => ret (State f s k e m) + | State f (Sgoto lbl) k e m => + match find_label lbl f.(fn_body) (call_cont k) with + | Some(s', k') => ret (State f s' k' e m) + | None => nil + end + + | Callstate (Internal f) vargs k m => + check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f))); + let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in + do m2 <- sem_bind_parameters e m1 f.(fn_params) vargs; + ret (State f f.(fn_body) k e m2) + | Callstate (External ef _ _) vargs k m => + match do_external _ _ ge ef w vargs m with + | None => nil + | Some(w',t,v,m') => (t, Returnstate v k m') :: nil + end + + | Returnstate v (Kcall f e C ty k) m => ret (ExprState f (C (Eval v ty)) k e m) + + | _ => nil + end. + +(* +Definition at_external (S: state): option (external_function * list val * mem) := + match S with + | Callstate (External ef _ _) vargs k m => Some (ef, vargs, m) + | _ => None + end. + +Definition after_external (S: state) (v: val) (m: mem): option state := + match S with + | Callstate _ _ k _ => Some (Returnstate v k m) + | _ => None + end. +*) + +Ltac myinv := + match goal with + | [ |- In _ nil -> _ ] => intro X; elim X + | [ |- In _ (ret _) -> _ ] => + intro X; elim X; clear X; + [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] + | [ |- In _ (_ :: nil) -> _ ] => + intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv] + | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x as []_eqn; myinv + | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x as []_eqn; myinv + | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv + | _ => idtac + end. + +Hint Extern 3 => exact I. + +Lemma do_step_sound: + forall w S t S', In (t, S') (do_step w S) -> Csem.step ge S t S'. +Proof with try (right; econstructor; eauto; fail). + intros until S'. destruct S; simpl. +(* State *) + destruct s; myinv... + (* skip *) + destruct k; myinv... + (* break *) + destruct k; myinv... + (* continue *) + destruct k; myinv... + (* goto *) + destruct p as [s' k']. myinv... +(* ExprState *) + destruct (is_val r) as [[v ty]|]_eqn. + (* expression is a value *) + rewrite (is_val_inv _ _ _ Heqo). + destruct k; myinv... + destruct v; myinv... + (* expression reduces *) + destruct (step_expr e RV r m) as [ll|]_eqn; try contradiction. intros. + exploit list_in_map_inv; eauto. intros [[C rd] [A B]]. + generalize (step_expr_sound e r RV m). unfold reducts_ok. rewrite Heqr0. + destruct ll; try contradiction. intros SOUND. + exploit SOUND; eauto. intros [CTX [a [EQ RD]]]. subst r. + unfold expr_final_state in A. simpl in A. left. + destruct rd; inv A; simpl in RD. + apply step_lred. auto. apply step_expr_not_stuck; congruence. auto. + apply step_rred. auto. apply step_expr_not_stuck; congruence. auto. + destruct RD; subst m'. apply Csem.step_call. auto. apply step_expr_not_stuck; congruence. auto. +(* callstate *) + destruct fd; myinv. + (* internal *) + destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1]_eqn. + myinv. right; apply step_internal_function with m1. auto. + change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp. + apply do_alloc_variables_sound. apply sem_bind_parameters_sound; auto. + (* external *) + destruct p as [[[w' tr] v] m']. myinv. right; constructor. + eapply do_ef_external_sound; eauto. +(* returnstate *) + destruct k; myinv... +Qed. + +Remark estep_not_val: + forall f a k e m t S, estep ge (ExprState f a k e m) t S -> is_val a = None. +Proof. + intros. + assert (forall b from to C, context from to C -> (C = fun x => x) \/ is_val (C b) = None). + induction 1; simpl; auto. + inv H. + destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto. + destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto. + destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto. +Qed. + +Lemma do_step_complete: + forall w S t S' w', possible_trace w t w' -> Csem.step ge S t S' -> In (t, S') (do_step w S). +Proof with (unfold ret; auto with coqlib). + intros until w'; intro PT; intros. + destruct H. + (* Expression step *) + inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL. +(* lred *) + unfold do_step; rewrite NOTVAL. + destruct (step_expr e RV (C a) m) as [ll|]_eqn. + change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Lred a' m')). + apply in_map. + generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl. + rewrite Heqr. destruct (step_expr e LV a m) as [ll'|]_eqn; try tauto. + intro. replace C with (fun x => C x). apply H3. + rewrite (lred_topred _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib. + apply extensionality; auto. + exploit not_stuck_step_expr; eauto. +(* rred *) + unfold do_step; rewrite NOTVAL. + destruct (step_expr e RV (C a) m) as [ll|]_eqn. + change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m')). + apply in_map. + generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl. + rewrite Heqr. destruct (step_expr e RV a m) as [ll'|]_eqn; try tauto. + intro. replace C with (fun x => C x). apply H3. + rewrite (rred_topred _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib. + apply extensionality; auto. + exploit not_stuck_step_expr; eauto. +(* callred *) + unfold do_step; rewrite NOTVAL. + destruct (step_expr e RV (C a) m) as [ll|]_eqn. + change (E0, Callstate fd vargs (Kcall f e C ty k) m) with (expr_final_state f k e (C, Callred fd vargs ty m)). + apply in_map. + generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl. + rewrite Heqr. destruct (step_expr e RV a m) as [ll'|]_eqn; try tauto. + intro. replace C with (fun x => C x). apply H3. + rewrite (callred_topred _ _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib. + apply extensionality; auto. + exploit not_stuck_step_expr; eauto. + + (* Statement step *) + inv H; simpl... + rewrite H0... + rewrite H0... + rewrite H0... + destruct H0; subst s0... + destruct H0; subst s0... + rewrite H0... + rewrite H0... + rewrite pred_dec_false... + rewrite pred_dec_true... + rewrite H0... + rewrite H0... + destruct H0; subst x... + rewrite H0... + rewrite H0; rewrite H1... + rewrite pred_dec_true; auto. rewrite H2. red in H0. destruct k; try contradiction... + destruct H0; subst x... + rewrite H0... + + (* Call step *) + rewrite pred_dec_true; auto. rewrite (do_alloc_variables_complete _ _ _ _ _ H1). + rewrite (sem_bind_parameters_complete _ _ _ _ _ H2)... + exploit do_ef_external_complete; eauto. intro EQ; rewrite EQ. auto with coqlib. +Qed. + +End EXEC. + +Local Open Scope option_monad_scope. + +Definition do_initial_state (p: program): option (genv * state) := + let ge := Genv.globalenv p in + do m0 <- Genv.init_mem p; + do b <- Genv.find_symbol ge p.(prog_main); + do f <- Genv.find_funct_ptr ge b; + check (type_eq (type_of_fundef f) (Tfunction Tnil (Tint I32 Signed))); + Some (ge, Callstate f nil Kstop m0). + +Definition at_final_state (S: state): option int := + match S with + | Returnstate (Vint r) Kstop m => Some r + | _ => None + end. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 61599cf..6358786 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -129,7 +129,7 @@ let name_type ty = name_cdecl "" ty type associativity = LtoR | RtoL | NA let rec precedence = function - | Eloc _ -> assert false + | Eloc _ -> (16, NA) | Evar _ -> (16, NA) | Ederef _ -> (15, RtoL) | Efield _ -> (16, LtoR) @@ -153,7 +153,7 @@ let rec precedence = function | Eassign _ -> (2, RtoL) | Eassignop _ -> (2, RtoL) | Ecomma _ -> (1, LtoR) - | Eparen _ -> assert false + | Eparen _ -> (14, RtoL) (* Expressions *) @@ -168,7 +168,7 @@ let rec expr p (prec, e) = else fprintf p "@[<hov 2>"; begin match e with | Eloc _ -> - assert false + fprintf p "<loc>" | Evar(id, _) -> fprintf p "%s" (extern_atom id) | Ederef(a1, _) -> @@ -181,8 +181,10 @@ let rec expr p (prec, e) = fprintf p "%ld" (camlint_of_coqint n) | Eval(Vfloat f, _) -> fprintf p "%F" f - | Eval(_, _) -> - assert false + | Eval(Vptr _, _) -> + fprintf p "<ptr>" + | Eval(Vundef, _) -> + fprintf p "<undef>" | Esizeof(ty, _) -> fprintf p "sizeof(%s)" (name_type ty) | Eunop(op, a1, _) -> @@ -207,8 +209,8 @@ let rec expr p (prec, e) = fprintf p "%a,@ %a" expr (prec1, a1) expr (prec2, a2) | Ecall(a1, al, _) -> fprintf p "%a@[<hov 1>(%a)@]" expr (prec', a1) exprlist (true, al) - | Eparen _ -> - assert false + | Eparen(a1, ty) -> + fprintf p "(%s) %a" (name_type ty) expr (prec', a1) end; if prec' < prec then fprintf p ")@]" else fprintf p "@]" @@ -221,6 +223,7 @@ and exprlist p (first, rl) = exprlist p (false, rl) let print_expr p e = expr p (0, e) +let print_exprlist p el = exprlist p (true, el) (* Statements *) diff --git a/common/Determinism.v b/common/Determinism.v index 16e8890..29cc695 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -222,13 +222,13 @@ Qed. Record sem_deterministic (L: semantics) := mk_deterministic { det_step: forall s0 t1 s1 t2 s2, - L (genv L) s0 t1 s1 -> L (genv L) s0 t2 s2 -> s1 = s2 /\ t1 = t2; + Step L s0 t1 s1 -> Step L s0 t2 s2 -> s1 = s2 /\ t1 = t2; det_initial_state: forall s1 s2, initial_state L s1 -> initial_state L s2 -> s1 = s2; det_final_state: forall s r1 r2, final_state L s r1 -> final_state L s r2 -> r1 = r2; det_final_nostep: forall s r, - final_state L s r -> nostep L (genv L) s + final_state L s r -> Nostep L s }. Section DETERM_SEM. @@ -238,18 +238,18 @@ Hypothesis DET: sem_deterministic L. Ltac use_step_deterministic := match goal with - | [ S1: step L (genv L) _ ?t1 _, S2: step L (genv L) _ ?t2 _ |- _ ] => + | [ S1: Step L _ ?t1 _, S2: Step L _ ?t2 _ |- _ ] => destruct (det_step L DET _ _ _ _ _ S1 S2) as [EQ1 EQ2]; subst end. (** Determinism for finite transition sequences. *) Lemma star_step_diamond: - forall s0 t1 s1, star L (genv L) s0 t1 s1 -> - forall t2 s2, star L (genv L) s0 t2 s2 -> + forall s0 t1 s1, Star L s0 t1 s1 -> + forall t2 s2, Star L s0 t2 s2 -> exists t, - (star L (genv L) s1 t s2 /\ t2 = t1 ** t) - \/ (star L (genv L) s2 t s1 /\ t1 = t2 ** t). + (Star L s1 t s2 /\ t2 = t1 ** t) + \/ (Star L s2 t s1 /\ t1 = t2 ** t). Proof. induction 1; intros. exists t2; auto. @@ -262,7 +262,7 @@ Qed. Ltac use_star_step_diamond := match goal with - | [ S1: star (step L) (genv L) _ ?t1 _, S2: star (step L) (genv L) _ ?t2 _ |- _ ] => + | [ S1: Star L _ ?t1 _, S2: Star L _ ?t2 _ |- _ ] => let t := fresh "t" in let P := fresh "P" in let EQ := fresh "EQ" in destruct (star_step_diamond _ _ _ S1 _ _ S2) as [t [ [P EQ] | [P EQ] ]]; subst @@ -270,16 +270,16 @@ Ltac use_star_step_diamond := Ltac use_nostep := match goal with - | [ S: step L (genv L) ?s _ _, NO: nostep (step L) (genv L) ?s |- _ ] => elim (NO _ _ S) + | [ S: Step L ?s _ _, NO: Nostep L ?s |- _ ] => elim (NO _ _ S) end. Lemma star_step_triangle: forall s0 t1 s1 t2 s2, - star L (genv L) s0 t1 s1 -> - star L (genv L) s0 t2 s2 -> - nostep L (genv L) s2 -> + Star L s0 t1 s1 -> + Star L s0 t2 s2 -> + Nostep L s2 -> exists t, - star L (genv L) s1 t s2 /\ t2 = t1 ** t. + Star L s1 t s2 /\ t2 = t1 ** t. Proof. intros. use_star_step_diamond. exists t; auto. @@ -289,8 +289,7 @@ Qed. Ltac use_star_step_triangle := match goal with - | [ S1: star (step L) (genv L) _ ?t1 _, S2: star (step L) (genv L) _ ?t2 ?s2, - NO: nostep (step L) (genv L) ?s2 |- _ ] => + | [ S1: Star L _ ?t1 _, S2: Star L _ ?t2 ?s2, NO: Nostep L ?s2 |- _ ] => let t := fresh "t" in let P := fresh "P" in let EQ := fresh "EQ" in destruct (star_step_triangle _ _ _ _ _ S1 S2 NO) as [t [P EQ]]; subst @@ -298,8 +297,8 @@ Ltac use_star_step_triangle := Lemma steps_deterministic: forall s0 t1 s1 t2 s2, - star L (genv L) s0 t1 s1 -> star L (genv L) s0 t2 s2 -> - nostep L (genv L) s1 -> nostep L (genv L) s2 -> + Star L s0 t1 s1 -> Star L s0 t2 s2 -> + Nostep L s1 -> Nostep L s2 -> t1 = t2 /\ s1 = s2. Proof. intros. use_star_step_triangle. inv P. @@ -308,8 +307,8 @@ Qed. Lemma terminates_not_goes_wrong: forall s t1 s1 r t2 s2, - star L (genv L) s t1 s1 -> final_state L s1 r -> - star L (genv L) s t2 s2 -> nostep L (genv L) s2 -> + Star L s t1 s1 -> final_state L s1 r -> + Star L s t2 s2 -> Nostep L s2 -> (forall r, ~final_state L s2 r) -> False. Proof. intros. @@ -321,9 +320,9 @@ Qed. (** Determinism for infinite transition sequences. *) Lemma star_final_not_forever_silent: - forall s t s', star L (genv L) s t s' -> - nostep L (genv L) s' -> - forever_silent L (genv L) s -> False. + forall s t s', Star L s t s' -> + Nostep L s' -> + Forever_silent L s -> False. Proof. induction 1; intros. inv H0. use_nostep. @@ -332,8 +331,8 @@ Qed. Lemma star2_final_not_forever_silent: forall s t1 s1 t2 s2, - star L (genv L) s t1 s1 -> nostep L (genv L) s1 -> - star L (genv L) s t2 s2 -> forever_silent L (genv L) s2 -> + Star L s t1 s1 -> Nostep L s1 -> + Star L s t2 s2 -> Forever_silent L s2 -> False. Proof. intros. use_star_step_triangle. @@ -341,8 +340,8 @@ Proof. Qed. Lemma star_final_not_forever_reactive: - forall s t s', star L (genv L) s t s' -> - forall T, nostep L (genv L) s' -> forever_reactive L (genv L) s T -> False. + forall s t s', Star L s t s' -> + forall T, Nostep L s' -> Forever_reactive L s T -> False. Proof. induction 1; intros. inv H0. inv H1. congruence. use_nostep. @@ -353,9 +352,9 @@ Proof. Qed. Lemma star_forever_silent_inv: - forall s t s', star L (genv L) s t s' -> - forever_silent L (genv L) s -> - t = E0 /\ forever_silent L (genv L) s'. + forall s t s', Star L s t s' -> + Forever_silent L s -> + t = E0 /\ Forever_silent L s'. Proof. induction 1; intros. auto. @@ -364,23 +363,23 @@ Qed. Lemma forever_silent_reactive_exclusive: forall s T, - forever_silent L (genv L) s -> forever_reactive L (genv L) s T -> False. + Forever_silent L s -> Forever_reactive L s T -> False. Proof. intros. inv H0. exploit star_forever_silent_inv; eauto. intros [A B]. contradiction. Qed. Lemma forever_reactive_inv2: - forall s t1 s1, star L (genv L) s t1 s1 -> + forall s t1 s1, Star L s t1 s1 -> forall t2 s2 T1 T2, - star L (genv L) s t2 s2 -> + Star L s t2 s2 -> t1 <> E0 -> t2 <> E0 -> - forever_reactive L (genv L) s1 T1 -> - forever_reactive L (genv L) s2 T2 -> + Forever_reactive L s1 T1 -> + Forever_reactive L s2 T2 -> exists s', exists t, exists T1', exists T2', t <> E0 /\ - forever_reactive L (genv L) s' T1' /\ - forever_reactive L (genv L) s' T2' /\ + Forever_reactive L s' T1' /\ + Forever_reactive L s' T2' /\ t1 *** T1 = t *** T1' /\ t2 *** T2 = t *** T2'. Proof. @@ -401,8 +400,8 @@ Qed. Lemma forever_reactive_determ': forall s T1 T2, - forever_reactive L (genv L) s T1 -> - forever_reactive L (genv L) s T2 -> + Forever_reactive L s T1 -> + Forever_reactive L s T2 -> traceinf_sim' T1 T2. Proof. cofix COINDHYP; intros. @@ -415,17 +414,17 @@ Qed. Lemma forever_reactive_determ: forall s T1 T2, - forever_reactive L (genv L) s T1 -> - forever_reactive L (genv L) s T2 -> + Forever_reactive L s T1 -> + Forever_reactive L s T2 -> traceinf_sim T1 T2. Proof. intros. apply traceinf_sim'_sim. eapply forever_reactive_determ'; eauto. Qed. Lemma star_forever_reactive_inv: - forall s t s', star L (genv L) s t s' -> - forall T, forever_reactive L (genv L) s T -> - exists T', forever_reactive L (genv L) s' T' /\ T = t *** T'. + forall s t s', Star L s t s' -> + forall T, Forever_reactive L s T -> + exists T', Forever_reactive L s' T' /\ T = t *** T'. Proof. induction 1; intros. exists T; auto. @@ -437,8 +436,8 @@ Qed. Lemma forever_silent_reactive_exclusive2: forall s t s' T, - star L (genv L) s t s' -> forever_silent L (genv L) s' -> - forever_reactive L (genv L) s T -> + Star L s t s' -> Forever_silent L s' -> + Forever_reactive L s T -> False. Proof. intros. exploit star_forever_reactive_inv; eauto. @@ -529,28 +528,28 @@ Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. Local Open Scope pair_scope. -Definition world_sem : semantics := @mk_semantics +Definition world_sem : semantics := @Semantics (state L * world)%type (funtype L) (vartype L) - (fun ge s t s' => L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2) + (fun ge s t s' => step L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2) (fun s => initial_state L s#1 /\ s#2 = initial_world) (fun s r => final_state L s#1 r) - (genv L). + (globalenv L). (** If the original semantics is determinate, the world-aware semantics is deterministic. *) -Hypothesis D: sem_determinate L. +Hypothesis D: determinate L. Theorem world_sem_deterministic: sem_deterministic world_sem. Proof. constructor; simpl; intros. (* steps *) destruct H; destruct H0. - exploit (sd_match D). eexact H. eexact H0. intros MT. + exploit (sd_determ D). eexact H. eexact H0. intros [A B]. exploit match_possible_traces; eauto. intros [EQ1 EQ2]. subst t2. - exploit (sd_determ D). eexact H. eexact H0. intros EQ3. - split; auto. rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). congruence. + split; auto. + rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). intuition congruence. (* initial states *) destruct H; destruct H0. rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). decEq. @@ -562,8 +561,8 @@ Proof. red; simpl; intros. red; intros [A B]. exploit (sd_final_nostep D); eauto. Qed. - - +(*** To be updated. *) +(*********** Variable genv: Type. Variable state: Type. Variable step: genv -> state -> trace -> state -> Prop. @@ -822,6 +821,8 @@ Qed. End INTERNAL_DET_TO_DET. +***********) + End WORLD_SEM. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 4a57a37..a9db51e 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -33,6 +33,8 @@ place during program linking and program loading in a real operating system. *) +Require Recdef. +Require Import Zwf. Require Import Axioms. Require Import Coqlib. Require Import Errors. @@ -99,6 +101,13 @@ Definition find_funct (ge: t) (v: val) : option F := | _ => None end. +(** [invert_symbol ge b] returns the name associated with the given block, if any *) + +Definition invert_symbol (ge: t) (b: block) : option ident := + PTree.fold + (fun res id b' => if eq_block b b' then Some id else res) + ge.(genv_symb) None. + (** [find_var_info ge b] returns the information attached to the variable at address [b]. *) @@ -468,6 +477,39 @@ Proof. intros. red; intros; subst. elim H. destruct ge. eauto. Qed. +Theorem invert_find_symbol: + forall ge id b, + invert_symbol ge b = Some id -> find_symbol ge id = Some b. +Proof. + intros until b; unfold find_symbol, invert_symbol. + apply PTree_Properties.fold_rec. + intros. rewrite H in H0; auto. + congruence. + intros. destruct (eq_block b v). inv H2. apply PTree.gss. + rewrite PTree.gsspec. destruct (peq id k). + subst. assert (m!k = Some b) by auto. congruence. + auto. +Qed. + +Theorem find_invert_symbol: + forall ge id b, + find_symbol ge id = Some b -> invert_symbol ge b = Some id. +Proof. + intros until b. + assert (find_symbol ge id = Some b -> exists id', invert_symbol ge b = Some id'). + unfold find_symbol, invert_symbol. + apply PTree_Properties.fold_rec. + intros. rewrite H in H0; auto. + rewrite PTree.gempty; congruence. + intros. destruct (eq_block b v). exists k; auto. + rewrite PTree.gsspec in H2. destruct (peq id k). + inv H2. congruence. auto. + + intros; exploit H; eauto. intros [id' A]. + assert (id = id'). eapply genv_vars_inj; eauto. apply invert_find_symbol; auto. + congruence. +Qed. + (** * Construction of the initial memory state *) Section INITMEM. @@ -517,6 +559,18 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data) end end. +Function store_zeros (m: mem) (b: block) (n: Z) {wf (Zwf 0) n}: option mem := + if zle n 0 then Some m else + let n' := n - 1 in + match Mem.store Mint8unsigned m b n' Vzero with + | Some m' => store_zeros m' b n' + | None => None + end. +Proof. + intros. red. omega. + apply Zwf_well_founded. +Qed. + Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := match il with | nil => 0 @@ -530,10 +584,15 @@ Definition perm_globvar (gv: globvar V) : permission := Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem := let init := idv#2.(gvar_init) in - let (m', b) := Mem.alloc m 0 (init_data_list_size init) in - match store_init_data_list m' b 0 init with + let sz := init_data_list_size init in + let (m1, b) := Mem.alloc m 0 sz in + match store_zeros m1 b sz with | None => None - | Some m'' => Mem.drop_perm m'' b 0 (init_data_list_size init) (perm_globvar idv#2) + | Some m2 => + match store_init_data_list m2 b 0 init with + | None => None + | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar idv#2) + end end. Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V)) @@ -561,6 +620,15 @@ Proof. destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. Qed. +Remark store_zeros_nextblock: + forall m b n m', store_zeros m b n = Some m' -> Mem.nextblock m' = Mem.nextblock m. +Proof. + intros until n. functional induction (store_zeros m b n); intros. + inv H; auto. + rewrite IHo; eauto with mem. + congruence. +Qed. + Remark alloc_variables_nextblock: forall vl m m', alloc_variables m vl = Some m' -> @@ -571,17 +639,31 @@ Proof. simpl length; rewrite inj_S; simpl. intros m m'. unfold alloc_variable. set (init := gvar_init a#2). - caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE. - caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. - intros m3 DROP REC. + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC. + caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. + caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC. rewrite (IHvl _ _ REC). rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + rewrite (store_zeros_nextblock _ _ _ STZ). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. Qed. + +Remark store_zeros_perm: + forall prm b' q m b n m', + store_zeros m b n = Some m' -> + Mem.perm m b' q prm -> Mem.perm m' b' q prm. +Proof. + intros until n. functional induction (store_zeros m b n); intros. + inv H; auto. + eauto with mem. + congruence. +Qed. + Remark store_init_data_list_perm: forall prm b' q idl b m p m', store_init_data_list m b p idl = Some m' -> @@ -605,17 +687,31 @@ Proof. simpl; intros. congruence. intros until m'. simpl. unfold alloc_variable. set (init := gvar_init a#2). - caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE. - caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. - intros m3 DROP REC PERM. + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC. + caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. + caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC PERM. assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. eapply IHvl; eauto. eapply Mem.perm_drop_3; eauto. - eapply store_init_data_list_perm; eauto. + eapply store_init_data_list_perm; eauto. + eapply store_zeros_perm; eauto. eauto with mem. Qed. +Remark store_zeros_outside: + forall m b n m', + store_zeros m b n = Some m' -> + forall chunk b' p, + b' <> b -> Mem.load chunk m' b' p = Mem.load chunk m b' p. +Proof. + intros until n. functional induction (store_zeros m b n); intros. + inv H; auto. + rewrite IHo; auto. eapply Mem.load_store_other; eauto. + inv H. +Qed. + Remark store_init_data_list_outside: forall b il m p m', store_init_data_list m b p il = Some m' -> @@ -699,20 +795,24 @@ Proof. congruence. unfold alloc_variable. set (init := gvar_init a#2). - caseEq (Mem.alloc m 0 (init_data_list_size init)); intros m1 b1 ALLOC. - caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO. - caseEq (Mem.drop_perm m2 b1 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. - intros m3 DROP RED VALID. + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC. + caseEq (store_zeros m1 b1 sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list m2 b1 0 init); try congruence. intros m3 STORE. + caseEq (Mem.drop_perm m3 b1 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID. assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem. - transitivity (Mem.load chunk m3 b p). + transitivity (Mem.load chunk m4 b p). apply IHvl; auto. red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STO). + rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + rewrite (store_zeros_nextblock _ _ _ STZ). change (Mem.valid_block m1 b). eauto with mem. - transitivity (Mem.load chunk m2 b p). + transitivity (Mem.load chunk m3 b p). eapply Mem.load_drop; eauto. + transitivity (Mem.load chunk m2 b p). + eapply store_init_data_list_outside; eauto. transitivity (Mem.load chunk m1 b p). - eapply store_init_data_list_outside; eauto. + eapply store_zeros_outside; eauto. eapply Mem.load_alloc_unchanged; eauto. Qed. @@ -742,14 +842,15 @@ Proof. contradiction. intros until m'; intro NEXT. unfold alloc_variable. destruct a as [id' gv']. simpl. - caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init gv'))); try congruence. - intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 (gvar_init gv')); try congruence. - intros m2 STORE. - caseEq (Mem.drop_perm m2 b 0 (init_data_list_size (gvar_init gv')) (perm_globvar gv')); try congruence. - intros m3 DROP REC NOREPET IN. inv NOREPET. + set (init := gvar_init gv'). + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC. + caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. + caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar gv')); try congruence. + intros m4 DROP REC NOREPET IN. inv NOREPET. exploit Mem.alloc_result; eauto. intro BEQ. - destruct IN. inv H. + destruct IN. inversion H; subst id gv. exists (Mem.nextblock m); split. rewrite add_variables_same_symb; auto. unfold find_symbol; simpl. rewrite PTree.gss. congruence. @@ -757,23 +858,24 @@ Proof. rewrite NEXT. apply ZMap.gss. simpl. rewrite <- NEXT; omega. split. red; intros. - eapply alloc_variables_perm; eauto. - eapply Mem.perm_drop_1; eauto. + rewrite <- BEQ. eapply alloc_variables_perm; eauto. eapply Mem.perm_drop_1; eauto. intros NOVOL. - apply load_store_init_data_invariant with m2. - intros. transitivity (Mem.load chunk m3 (Mem.nextblock m) ofs). + apply load_store_init_data_invariant with m3. + intros. transitivity (Mem.load chunk m4 (Mem.nextblock m) ofs). eapply load_alloc_variables; eauto. red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - change (Mem.valid_block m1 (Mem.nextblock m)). eauto with mem. + rewrite (store_zeros_nextblock _ _ _ STZ). + change (Mem.valid_block m1 (Mem.nextblock m)). rewrite <- BEQ. eauto with mem. eapply Mem.load_drop; eauto. repeat right. - unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv); auto with mem. - eapply store_init_data_list_charact; eauto. + unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv'); auto with mem. + rewrite <- BEQ. eapply store_init_data_list_charact; eauto. - apply IHvl with m3; auto. + apply IHvl with m4; auto. simpl. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + rewrite (store_zeros_nextblock _ _ _ STZ). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. Qed. @@ -861,6 +963,19 @@ Proof. eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. Qed. +Lemma store_zeros_neutral: + forall m b n m', + Mem.inject_neutral thr m -> + b < thr -> + store_zeros m b n = Some m' -> + Mem.inject_neutral thr m'. +Proof. + intros until n. functional induction (store_zeros m b n); intros. + inv H1; auto. + apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor. + inv H1. +Qed. + Lemma alloc_variable_neutral: forall id m m', alloc_variable ge m id = Some m' -> @@ -868,16 +983,18 @@ Lemma alloc_variable_neutral: Mem.nextblock m < thr -> Mem.inject_neutral thr m'. Proof. - intros until m'. unfold alloc_variable. - caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b ALLOC. - caseEq (store_init_data_list ge m1 b 0 (gvar_init id#2)); try congruence. - intros m2 STORE DROP NEUTRAL NEXT. + intros until m'. unfold alloc_variable. + set (init := gvar_init id#2). + set (sz := init_data_list_size init). + caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC. + caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. + caseEq (store_init_data_list ge m2 b 0 init); try congruence. + intros m3 STORE DROP NEUTRAL NEXT. + assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. eapply Mem.drop_inject_neutral; eauto. - eapply store_init_data_list_neutral with (b := b). + eapply store_init_data_list_neutral with (m := m2) (b := b); eauto. + eapply store_zeros_neutral with (m := m1); eauto. eapply Mem.alloc_inject_neutral; eauto. - rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. - eauto. - rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. Qed. Lemma alloc_variables_neutral: @@ -1099,11 +1216,12 @@ Proof. inv H. unfold alloc_variable; simpl. destruct (Mem.alloc m 0 (init_data_list_size init)). + destruct (store_zeros m0 b (init_data_list_size init)); auto. rewrite store_init_data_list_match. - destruct (store_init_data_list (globalenv p) m0 b 0 init); auto. + destruct (store_init_data_list (globalenv p) m1 b 0 init); auto. change (perm_globvar (mkglobvar info2 init ro vo)) with (perm_globvar (mkglobvar info1 init ro vo)). - destruct (Mem.drop_perm m1 b 0 (init_data_list_size init) + destruct (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar (mkglobvar info1 init ro vo))); auto. Qed. diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml index edf8821..6d38b55 100644 --- a/cparser/StructAssign.ml +++ b/cparser/StructAssign.ml @@ -50,20 +50,17 @@ let default_memcpy () = memcpy_decl := Some id; (id, memcpy_type) -let rec find_memcpy env = function - | [] -> - default_memcpy() - | name :: rem -> - try lookup_function env name with Env.Error _ -> find_memcpy env rem - -let memcpy_1_ident env = - find_memcpy env ["__builtin_memcpy"; "memcpy"] -let memcpy_2_ident env = - find_memcpy env ["__builtin_memcpy_al2"; "__builtin_memcpy"; "memcpy"] -let memcpy_4_ident env = - find_memcpy env ["__builtin_memcpy_al4"; "__builtin_memcpy"; "memcpy"] -let memcpy_8_ident env = - find_memcpy env ["__builtin_memcpy_al8"; "__builtin_memcpy"; "memcpy"] +let find_memcpy env = + try + (lookup_function env "__builtin_memcpy_aligned", true) + with Env.Error _ -> + try + (lookup_function env "__builtin_memcpy", false) + with Env.Error _ -> + try + (lookup_function env "memcpy", false) + with Env.Error _ -> + (default_memcpy(), false) (* Smart constructor for "," expressions *) @@ -84,20 +81,19 @@ let rec addrof e = [lhs] and [rhs] must be l-values. *) let transf_assign env lhs rhs = - let (al, sz) = - match Cutil.alignof env lhs.etyp, Cutil.sizeof env lhs.etyp with - | Some al, Some sz -> (al, sz) - | _, _ -> (1, 1) in - let (ident, ty) = - if al mod 8 = 0 && sz mod 8 = 0 then memcpy_8_ident env - else if al mod 4 = 0 && sz mod 4 = 0 then memcpy_4_ident env - else if al mod 2 = 0 && sz mod 2 = 0 then memcpy_2_ident env - else memcpy_1_ident env in + let al = + match Cutil.alignof env lhs.etyp with Some al -> al | None -> 1 in + let ((ident, ty), four_args) = find_memcpy env in let memcpy = {edesc = EVar(ident); etyp = ty} in - let e_lhs = addrof lhs in - let e_rhs = addrof rhs in - let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in - {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]); etyp = TVoid[]} + let e_lhs = addrof lhs + and e_rhs = addrof rhs + and e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} + and e_align = intconst (Int64.of_int al) size_t_ikind in + let args = + if four_args + then [e_lhs; e_rhs; e_size; e_align] + else [e_lhs; e_rhs; e_size] in + {edesc = ECall(memcpy, args); etyp = TVoid[]} (* Detect invariant l-values *) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2a96c38..87de59f 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -22,6 +22,7 @@ let option_fbitfields = ref false let option_fvararg_calls = ref true let option_fpacked_structs = ref false let option_fmadd = ref false +let option_fsse = ref true let option_dparse = ref false let option_dcmedium = ref false let option_dclight = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index a51cd8f..37a187e 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -24,6 +24,7 @@ Require Import Smallstep. Require Csyntax. Require Csem. Require Cstrategy. +Require Cexec. Require Clight. Require Csharpminor. Require Cminor. @@ -82,8 +83,8 @@ Require Reloadtyping. Require Stackingproof. Require Stackingtyping. Require Asmgenproof. + (** Pretty-printers (defined in Caml). *) -Parameter print_Csyntax: Csyntax.program -> unit. Parameter print_Clight: Clight.program -> unit. Parameter print_Cminor: Cminor.program -> unit. Parameter print_RTL: RTL.fundef -> unit. @@ -180,13 +181,13 @@ Definition transf_clight_program (p: Clight.program) : res Asm.program := Definition transf_c_program (p: Csyntax.program) : res Asm.program := OK p - @@ print print_Csyntax @@@ SimplExpr.transl_program @@@ transf_clight_program. -(** Force [Initializers] to be extracted as well. *) +(** Force [Initializers] and [Cexec] to be extracted as well. *) Definition transl_init := Initializers.transl_init. +Definition cexec_do_step := Cexec.do_step. (** The following lemmas help reason over compositions of passes. *) @@ -403,7 +404,7 @@ Theorem transf_cstrategy_program_correct: Proof. intros. assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)). - revert H; unfold transf_c_program; simpl. rewrite print_identity. + revert H; unfold transf_c_program; simpl. caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. intros EQ1. eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto. diff --git a/driver/Driver.ml b/driver/Driver.ml index 6aa63e0..d5a659d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -62,9 +62,9 @@ let preprocess ifile ofile = exit 2 end -(* From preprocessed C to asm *) +(* From preprocessed C to Csyntax *) -let compile_c_file sourcename ifile ofile = +let parse_c_file sourcename ifile = Sections.initialize(); (* Simplification options *) let simplifs = @@ -94,11 +94,22 @@ let compile_c_file sourcename ifile ofile = | None -> exit 2 | Some p -> p in flush stderr; - (* Prepare to dump Csyntax, Clight, RTL, etc, if requested *) + (* Save CompCert C AST if requested *) + if !option_dcmedium then begin + let ofile = Filename.chop_suffix sourcename ".c" ^ ".compcert.c" in + let oc = open_out ofile in + PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; + close_out oc + end; + csyntax + +(* From CompCert C AST to asm *) + +let compile_c_ast sourcename csyntax ofile = + (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = dst := if !opt then Some (Filename.chop_suffix sourcename ".c" ^ ext) else None in - set_dest PrintCsyntax.destination option_dcmedium ".compcert.c"; set_dest PrintClight.destination option_dclight ".light.c"; set_dest PrintCminor.destination option_dcminor ".cm"; set_dest PrintRTL.destination_rtl option_drtl ".rtl"; @@ -120,6 +131,11 @@ let compile_c_file sourcename ifile ofile = PrintAsm.print_program oc asm; close_out oc +(* From C source to asm *) + +let compile_c_file sourcename ifile ofile = + compile_c_ast sourcename (parse_c_file sourcename ifile) ofile + (* From Cminor to asm *) let compile_cminor_file ifile ofile = @@ -178,6 +194,8 @@ let linker exe_name files = (* Processing of a .c file *) +let option_interp = ref false + let process_c_file sourcename = let prefixname = Filename.chop_suffix sourcename ".c" in if !option_E then begin @@ -185,7 +203,10 @@ let process_c_file sourcename = end else begin let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; - if !option_S then begin + if !option_interp then begin + let csyntax = parse_c_file sourcename preproname in + Interp.execute csyntax + end else if !option_S then begin compile_c_file sourcename preproname (prefixname ^ ".s") end else begin let asmname = @@ -235,57 +256,13 @@ let process_S_file sourcename = end; prefixname ^ ".o" -(* Command-line parsing *) +(* Interpretation of a .c file *) -let usage_string = -"ccomp [options] <source files> -Recognized source files: - .c C source file - .cm Cminor source file - .s Assembly file - .S Assembly file, to be run through the preprocessor - .o Object file - .a Library file -Processing options: - -E Preprocess only, send result to standard output - -S Compile to assembler only, save result in <file>.s - -c Compile to object file only (no linking), result in <file>.o -Preprocessing options: - -I<dir> Add <dir> to search path for #include files - -D<symb>=<val> Define preprocessor symbol - -U<symb> Undefine preprocessor symbol -Language support options (use -fno-<opt> to turn off -f<opt>) : - -fbitfields Emulate bit fields in structs [off] - -flonglong Partial emulation of 'long long' types [on] - -fstruct-passing Emulate passing structs and unions by value [off] - -fstruct-assign Emulate assignment between structs or unions [off] - -fvararg-calls Emulate calls to variable-argument functions [on] - -fpacked-structs Emulate packed structs [off] -Code generation options: - -fmadd Use fused multiply-add and multiply-sub instructions [off] - -fsmall-data <n> Set maximal size <n> for allocation in small data area - -fsmall-const <n> Set maximal size <n> for allocation in small constant area -Tracing options: - -dparse Save C file after parsing and elaboration in <file>.parse.c - -dc Save generated Compcert C in <file>.compcert.c - -dclight Save generated Clight in <file>.light.c - -dcminor Save generated Cminor in <file>.cm - -drtl Save unoptimized generated RTL in <file>.rtl - -dtailcall Save RTL after tail call optimization in <file>.tailcall.rtl - -dcastopt Save RTL after cast optimization in <file>.castopt.rtl - -dconstprop Save RTL after constant propagation in <file>.constprop.rtl - -dcse Save RTL after CSE optimization in <file>.cse.rtl - -dalloc Save LTL after register allocation in <file>.alloc.ltl - -dmach Save generated Mach code in <file>.mach - -dasm Save generated assembly in <file>.s -Linking options: - -l<lib> Link library <lib> - -L<dir> Add <dir> to search path for libraries - -o <file> Generate executable in <file> (default: a.out) -General options: - -stdlib <dir> Set the path of the Compcert run-time library [MacOS X only] - -v Print external commands before invoking them -" +let execute_c_file sourcename = + let preproname = Filename.temp_file "compcert" ".i" in + preprocess sourcename preproname + +(* Command-line parsing *) type action = | Set of bool ref @@ -340,6 +317,63 @@ let parse_cmdline spec usage = end in parse 1 +let usage_string = +"ccomp [options] <source files> +Recognized source files: + .c C source file + .cm Cminor source file + .s Assembly file + .S Assembly file, to be run through the preprocessor + .o Object file + .a Library file +Processing options: + -E Preprocess only, send result to standard output + -S Compile to assembler only, save result in <file>.s + -c Compile to object file only (no linking), result in <file>.o +Preprocessing options: + -I<dir> Add <dir> to search path for #include files + -D<symb>=<val> Define preprocessor symbol + -U<symb> Undefine preprocessor symbol +Language support options (use -fno-<opt> to turn off -f<opt>) : + -fbitfields Emulate bit fields in structs [off] + -flonglong Partial emulation of 'long long' types [on] + -fstruct-passing Emulate passing structs and unions by value [off] + -fstruct-assign Emulate assignment between structs or unions [off] + -fvararg-calls Emulate calls to variable-argument functions [on] + -fpacked-structs Emulate packed structs [off] +Code generation options: (use -fno-<opt> to turn off -f<opt>) : + -fmadd (PowerPC) Use fused multiply-add and multiply-sub instructions [off] + -fsse (IA32) Use SSE2 instructions for some integer operations [on] + -fsmall-data <n> Set maximal size <n> for allocation in small data area + -fsmall-const <n> Set maximal size <n> for allocation in small constant area +Tracing options: + -dparse Save C file after parsing and elaboration in <file>.parse.c + -dc Save generated Compcert C in <file>.compcert.c + -dclight Save generated Clight in <file>.light.c + -dcminor Save generated Cminor in <file>.cm + -drtl Save unoptimized generated RTL in <file>.rtl + -dtailcall Save RTL after tail call optimization in <file>.tailcall.rtl + -dcastopt Save RTL after cast optimization in <file>.castopt.rtl + -dconstprop Save RTL after constant propagation in <file>.constprop.rtl + -dcse Save RTL after CSE optimization in <file>.cse.rtl + -dalloc Save LTL after register allocation in <file>.alloc.ltl + -dmach Save generated Mach code in <file>.mach + -dasm Save generated assembly in <file>.s +Linking options: + -l<lib> Link library <lib> + -L<dir> Add <dir> to search path for libraries + -o <file> Generate executable in <file> (default: a.out) +General options: + -stdlib <dir> Set the path of the Compcert run-time library [MacOS X only] + -v Print external commands before invoking them +Interpreter mode: + -interp Execute given .c files using the reference interpreter + -quiet Suppress diagnostic messages for the interpreter + -trace Have the interpreter produce a detailed trace of reductions + -random Randomize execution order + -all Simulate all possible execution orders +" + let cmdline_actions = let f_opt name ref = ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in @@ -367,6 +401,11 @@ let cmdline_actions = "-S$", Set option_S; "-c$", Set option_c; "-v$", Set option_v; + "-interp$", Set option_interp; + "-quiet$", Self (fun _ -> Interp.trace := 0); + "-trace$", Self (fun _ -> Interp.trace := 2); + "-random$", Self (fun _ -> Interp.mode := Interp.Random); + "-all$", Self (fun _ -> Interp.mode := Interp.All); ".*\\.c$", Self (fun s -> let objfile = process_c_file s in linker_options := objfile :: !linker_options); @@ -391,6 +430,7 @@ let cmdline_actions = @ f_opt "vararg-calls" option_fvararg_calls @ f_opt "madd" option_fmadd @ f_opt "packed-structs" option_fpacked_structs + @ f_opt "sse" option_fsse let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 }; @@ -405,7 +445,7 @@ let _ = CPragmas.initialize(); parse_cmdline cmdline_actions usage_string; if !linker_options <> [] - && not (!option_c || !option_S || !option_E) + && not (!option_c || !option_S || !option_E || !option_interp) then begin linker !exe_name !linker_options end diff --git a/driver/Interp.ml b/driver/Interp.ml new file mode 100644 index 0000000..84037ae --- /dev/null +++ b/driver/Interp.ml @@ -0,0 +1,408 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Interpreting CompCert C sources *) + +open Format +open Camlcoq +open Datatypes +open BinPos +open BinInt +open AST +open Values +open Memory +open Globalenvs +open Events +open Csyntax +open Csem +open Clflags + +(* Configuration *) + +let trace = ref 1 (* 0 if quiet, 1 if normally verbose, 2 if full trace *) + +type mode = First | Random | All + +let mode = ref First + +(* Printing events *) + +let print_eventval p = function + | EVint n -> fprintf p "%ld" (camlint_of_coqint n) + | EVfloat f -> fprintf p "%F" f + | EVptr_global(id, ofs) -> + fprintf p "&%s%+ld" (extern_atom id) (camlint_of_coqint ofs) + +let print_eventval_list p = function + | [] -> () + | v1 :: vl -> + print_eventval p v1; + List.iter (fun v -> fprintf p ",@ %a" print_eventval v) vl + +let print_event p = function + | Event_syscall(id, args, res) -> + fprintf p "extcall %s(%a) -> %a" + (extern_atom id) + print_eventval_list args + print_eventval res + | Event_vload(chunk, id, ofs, res) -> + fprintf p "volatile load %s[&%s%+ld] -> %a" + (PrintCminor.name_of_chunk chunk) + (extern_atom id) (camlint_of_coqint ofs) + print_eventval res + | Event_vstore(chunk, id, ofs, arg) -> + fprintf p "volatile store %s[&%s%+ld] <- %a" + (PrintCminor.name_of_chunk chunk) + (extern_atom id) (camlint_of_coqint ofs) + print_eventval arg + | Event_annot(text, args) -> + fprintf p "annotation \"%s\" %a" + (extern_atom text) + print_eventval_list args + +(* Printing states *) + +let name_of_fundef prog fd = + let rec find_name = function + | [] -> "<unknown function>" + | Coq_pair(id, fd') :: rem -> + if fd = fd' then extern_atom id else find_name rem + in find_name prog.prog_funct + +let name_of_function prog fn = + name_of_fundef prog (Internal fn) + +let print_val p = function + | Vint n -> fprintf p "%ld" (camlint_of_coqint n) + | Vfloat f -> fprintf p "%F" f + | Vptr(b, ofs) -> fprintf p "<ptr>" + | Vundef -> fprintf p "<undef>" + +let print_val_list p = function + | [] -> () + | v1 :: vl -> + print_val p v1; + List.iter (fun v -> fprintf p ",@ %a" print_val v) vl + +let print_state prog p = function + | State(f, s, k, e, m) -> + fprintf p "in function %s, statement@ @[<hv 0>%a@]" + (name_of_function prog f) + PrintCsyntax.print_stmt s + | ExprState(f, r, k, e, m) -> + fprintf p "in function %s, expression@ @[<hv 0>%a@]" + (name_of_function prog f) + PrintCsyntax.print_expr r + | Callstate(fd, args, k, m) -> + fprintf p "calling@ @[<hov 2>%s(%a)@]" + (name_of_fundef prog fd) + print_val_list args + | Returnstate(res, k, m) -> + fprintf p "returning@ %a" + print_val res + +let mem_of_state = function + | State(f, s, k, e, m) -> m + | ExprState(f, r, k, e, m) -> m + | Callstate(fd, args, k, m) -> m + | Returnstate(res, k, m) -> m + +(* Comparing memory states *) + +let rec compare_Z_range lo hi f = + if coq_Zcompare lo hi = Lt then begin + let c = f lo in if c <> 0 then c else compare_Z_range (coq_Zsucc lo) hi f + end else 0 + +let compare_mem m1 m2 = + if m1 == m2 then 0 else + let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else + compare_Z_range Z0 m1.Mem.nextblock (fun b -> + let (Coq_pair(lo, hi) as bnds) = m1.Mem.bounds b in + let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else + let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in + if contents1 == contents2 then 0 else + let c = compare_Z_range lo hi (fun ofs -> + compare (contents1 ofs) (contents2 ofs)) in if c <> 0 then c else + let access1 = m1.Mem.mem_access b and access2 = m2.Mem.mem_access b in + if access1 == access2 then 0 else + compare_Z_range lo hi (fun ofs -> compare (access1 ofs) (access2 ofs))) + +(* Comparing continuations *) + +let some_expr = Evar(Coq_xH, Tvoid) + +let rank_cont = function + | Kstop -> 0 + | Kdo _ -> 1 + | Kseq _ -> 2 + | Kifthenelse _ -> 3 + | Kwhile1 _ -> 4 + | Kwhile2 _ -> 5 + | Kdowhile1 _ -> 6 + | Kdowhile2 _ -> 7 + | Kfor2 _ -> 8 + | Kfor3 _ -> 9 + | Kfor4 _ -> 10 + | Kswitch1 _ -> 11 + | Kswitch2 _ -> 12 + | Kreturn _ -> 13 + | Kcall _ -> 14 + +let rec compare_cont k1 k2 = + if k1 == k2 then 0 else + match k1, k2 with + | Kstop, Kstop -> 0 + | Kdo k1, Kdo k2 -> compare_cont k1 k2 + | Kseq(s1, k1), Kseq(s2, k2) -> + let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2 + | Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) -> + let c = compare (s1,s1') (s2,s2') in + if c <> 0 then c else compare_cont k1 k2 + | Kwhile1(e1, s1, k1), Kwhile1(e2, s2, k2) -> + let c = compare (e1,s1) (e2,s2) in + if c <> 0 then c else compare_cont k1 k2 + | Kwhile2(e1, s1, k1), Kwhile2(e2, s2, k2) -> + let c = compare (e1,s1) (e2,s2) in + if c <> 0 then c else compare_cont k1 k2 + | Kdowhile1(e1, s1, k1), Kdowhile1(e2, s2, k2) -> + let c = compare (e1,s1) (e2,s2) in + if c <> 0 then c else compare_cont k1 k2 + | Kdowhile2(e1, s1, k1), Kdowhile2(e2, s2, k2) -> + let c = compare (e1,s1) (e2,s2) in + if c <> 0 then c else compare_cont k1 k2 + | Kfor2(e1, s1, s1', k1), Kfor2(e2, s2, s2', k2) -> + let c = compare (e1,s1,s1') (e2,s2,s2') in + if c <> 0 then c else compare_cont k1 k2 + | Kfor3(e1, s1, s1', k1), Kfor3(e2, s2, s2', k2) -> + let c = compare (e1,s1,s1') (e2,s2,s2') in + if c <> 0 then c else compare_cont k1 k2 + | Kfor4(e1, s1, s1', k1), Kfor4(e2, s2, s2', k2) -> + let c = compare (e1,s1,s1') (e2,s2,s2') in + if c <> 0 then c else compare_cont k1 k2 + | Kswitch1(sl1, k1), Kswitch1(sl2, k2) -> + let c = compare sl1 sl2 in + if c <> 0 then c else compare_cont k1 k2 + | Kreturn k1, Kreturn k2 -> + compare_cont k1 k2 + | Kcall(f1, e1, c1, ty1, k1), Kcall(f2, e2, c2, ty2, k2) -> + let c = compare (f1, e1, c1 some_expr, ty1) (f2, e2, c2 some_expr, ty2) in + if c <> 0 then c else compare_cont k1 k2 + | _, _ -> + compare (rank_cont k1) (rank_cont k2) + +(* Comparing states *) + +let rank_state = function + | State _ -> 0 + | ExprState _ -> 1 + | Callstate _ -> 2 + | Returnstate _ -> 3 + +let compare_state s1 s2 = + if s1 == s2 then 0 else + match s1, s2 with + | State(f1,s1,k1,e1,m1), State(f2,s2,k2,e2,m2) -> + let c = compare (f1,s1,e1) (f2,s2,e2) in if c <> 0 then c else + let c = compare_cont k1 k2 in if c <> 0 then c else + compare_mem m1 m2 + | ExprState(f1,r1,k1,e1,m1), ExprState(f2,r2,k2,e2,m2) -> + let c = compare (f1,r1,e1) (f2,r2,e2) in if c <> 0 then c else + let c = compare_cont k1 k2 in if c <> 0 then c else + compare_mem m1 m2 + | Callstate(fd1,args1,k1,m1), Callstate(fd2,args2,k2,m2) -> + let c = compare (fd1,args1) (fd2,args2) in if c <> 0 then c else + let c = compare_cont k1 k2 in if c <> 0 then c else + compare_mem m1 m2 + | Returnstate(res1,k1,m1), Returnstate(res2,k2,m2) -> + let c = compare res1 res2 in if c <> 0 then c else + let c = compare_cont k1 k2 in if c <> 0 then c else + compare_mem m1 m2 + | _, _ -> + compare (rank_state s1) (rank_state s2) + +module StateSet = + Set.Make(struct type t = state let compare = compare_state end) + +(* Extract a string from a global pointer *) + +let extract_string ge m id ofs = + let b = Buffer.create 80 in + let rec extract blk ofs = + match Memory.Mem.load Mint8unsigned m blk ofs with + | Some(Vint n) -> + let c = Char.chr (Int32.to_int (camlint_of_coqint n)) in + if c = '\000' then begin + Some(Buffer.contents b) + end else begin + Buffer.add_char b c; + extract blk (coq_Zsucc ofs) + end + | _ -> + None in + match Genv.find_symbol ge id with + | None -> None + | Some blk -> extract blk ofs + +(* Emulation of printf *) + +(* All ISO C 99 formats except size modifiers [ll] (long long) and [L] + (long double) *) + +let re_conversion = Str.regexp + "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\)?\\([aAcdeEfgGinopsuxX%]\\)" + +external format_float: string -> float -> string + = "caml_format_float" +external format_int32: string -> int32 -> string + = "caml_int32_format" + +let do_printf ge m fmt args = + + let b = Buffer.create 80 in + let len = String.length fmt in + + let opt_search_forward pos = + try Some(Str.search_forward re_conversion fmt pos) + with Not_found -> None in + + let rec scan pos args = + if pos < len then begin + match opt_search_forward pos with + | None -> + Buffer.add_substring b fmt pos (len - pos) + | Some pos1 -> + Buffer.add_substring b fmt pos (pos1 - pos); + let pat = Str.matched_string fmt + and conv = Str.matched_group 3 fmt + and pos' = Str.match_end() in + match args, conv.[0] with + | _, '%' -> + Buffer.add_char b '%'; + scan pos' args + | [], _ -> + Buffer.add_string b "<missing argument>"; + scan pos' [] + | EVint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') -> + Buffer.add_string b (format_int32 pat (camlint_of_coqint i)); + scan pos' args' + | EVfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') -> + Buffer.add_string b (format_float pat f); + scan pos' args' + | EVptr_global(id, ofs) :: args', 's' -> + Buffer.add_string b + (match extract_string ge m id ofs with + | Some s -> s + | None -> "<bad string>"); + scan pos' args' + | EVptr_global(id, ofs) :: args', 'p' -> + Printf.bprintf b "<&%s%+ld>" (extern_atom id) (camlint_of_coqint ofs); + scan pos' args' + | _ :: args', _ -> + Buffer.add_string b "<formatting error>"; + scan pos' args' + end + in scan 0 args; Buffer.contents b + +(* Implementing external functions *) + +let re_stub = Str.regexp "\\$[if]*$" + +let chop_stub name = Str.replace_first re_stub "" name + +let rec world = Determinism.World(world_io, world_vload, world_vstore) + +and world_io id args = + match chop_stub(extern_atom id), args with + | "printf", EVptr_global(id, ofs) :: args' -> + Some(Coq_pair(EVint Integers.Int.zero, world)) + | _, _ -> + None + +and world_vload chunk id ofs = + let res = match chunk with + | Mint8signed -> EVint(coqint_of_camlint(Int32.sub (Random.int32 0x100l) 0x80l)) + | Mint8unsigned -> EVint(coqint_of_camlint(Random.int32 0x100l)) + | Mint16signed -> EVint(coqint_of_camlint(Int32.sub (Random.int32 0x10000l) 0x8000l)) + | Mint16unsigned -> EVint(coqint_of_camlint(Random.int32 0x10000l)) + | Mint32 -> EVint(coqint_of_camlint(Random.int32 0x7FFF_FFFFl)) + | Mfloat32 -> EVfloat(Floats.Float.singleoffloat(Random.float 1.0)) + | Mfloat64 -> EVfloat(Random.float 1.0) + in Some(Coq_pair(res, world)) + +and world_vstore chunk id ofs arg = + Some world + +let do_event p ge time s ev = + if !trace >= 1 then + fprintf p "@[<hov 2>Time %d: observable event: %a@]@." + time print_event ev; + match ev with + | Event_syscall(name, EVptr_global(id, ofs) :: args', res) + when chop_stub (extern_atom name) = "printf" -> + flush stderr; + let m = mem_of_state s in + begin match extract_string ge m id ofs with + | Some fmt -> print_string (do_printf ge m fmt args') + | None -> print_string "<bad printf>\n" + end; + flush stdout + | _ -> () + +let do_events p ge time s t = + List.iter (do_event p ge time s) t + +(* Exploration *) + +let do_step p prog ge time s = + if !trace >= 2 then + fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s; + match Cexec.at_final_state s with + | Some r -> + if !trace >= 1 then begin + fprintf p "Time %d: program terminated (exit code = %ld)@." + time (camlint_of_coqint r); + [] + end else begin + exit (Int32.to_int (camlint_of_coqint r)) + end + | None -> + match Cexec.do_step ge world s with + | [] -> + if !trace = 1 then + fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s; + fprintf p "ERROR: Undefined behavior@."; + fprintf p "@]."; + exit 126 + | l -> + List.iter (fun (Coq_pair(t, s')) -> do_events p ge time s t) l; + List.map snd l + +let rec explore p prog ge time ss = + let succs = + StateSet.fold (fun s l -> do_step p prog ge time s @ l) ss [] in + if succs <> [] then begin + let ss' = + match !mode with + | First -> StateSet.singleton (List.hd succs) + | Random -> StateSet.singleton (List.nth succs (Random.int (List.length succs))) + | All -> List.fold_right StateSet.add succs StateSet.empty in + explore p prog ge (time + 1) ss' + end + +let execute prog = + let p = err_formatter in + pp_set_max_boxes p 10; + begin match Cexec.do_initial_state prog with + | None -> fprintf p "ERROR: Initial state undefined@." + | Some(Coq_pair(ge, s)) -> explore p prog ge 0 (StateSet.singleton s) + end diff --git a/extraction/extraction.v b/extraction/extraction.v index 765bebd..4bfac69 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -82,7 +82,6 @@ Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. (* Compiler *) -Extract Constant Compiler.print_Csyntax => "PrintCsyntax.print_if". Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_rtl". diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index c9ee970..842957f 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -268,21 +268,26 @@ let print_annot_val oc txt args res = (* Unaligned memory accesses are quite fast on IA32, so use large memory accesses regardless of alignment. *) -let print_builtin_memcpy oc sz al args = - let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in +let print_builtin_memcpy_small oc sz al src dst = let tmp = if src <> ECX && dst <> ECX then ECX else if src <> EDX && dst <> EDX then EDX else EAX in + let need_tmp = + sz mod 4 <> 0 || not !Clflags.option_fsse in let rec copy ofs sz = - if sz >= 8 then begin + if sz >= 8 && !Clflags.option_fsse then begin fprintf oc " movq %d(%a), %a\n" ofs ireg src freg XMM6; fprintf oc " movq %a, %d(%a)\n" freg XMM6 ofs ireg dst; copy (ofs + 8) (sz - 8) end else if sz >= 4 then begin - fprintf oc " movd %d(%a), %a\n" ofs ireg src freg XMM6; - fprintf oc " movd %a, %d(%a)\n" freg XMM6 ofs ireg dst; + if !Clflags.option_fsse then begin + fprintf oc " movd %d(%a), %a\n" ofs ireg src freg XMM6; + fprintf oc " movd %a, %d(%a)\n" freg XMM6 ofs ireg dst + end else begin + fprintf oc " movl %d(%a), %a\n" ofs ireg src ireg tmp; + fprintf oc " movl %a, %d(%a)\n" ireg tmp ofs ireg dst + end; copy (ofs + 4) (sz - 4) end else if sz >= 2 then begin fprintf oc " movw %d(%a), %a\n" ofs ireg src ireg16 tmp; @@ -293,14 +298,39 @@ let print_builtin_memcpy oc sz al args = fprintf oc " movb %a, %d(%a)\n" ireg8 tmp ofs ireg dst; copy (ofs + 1) (sz - 1) end in - fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n" - comment sz al; - if tmp = EAX && sz mod 4 <> 0 then - fprintf oc " movd %a, %a\n" ireg EAX freg XMM7; + if need_tmp && tmp = EAX then + fprintf oc " pushl %a\n" ireg EAX; copy 0 sz; - if tmp = EAX && sz mod 4 <> 0 then - fprintf oc " movd %a, %a\n" freg XMM7 ireg EAX; - fprintf oc "%s end builtin __builtin_memcpy\n" comment + if need_tmp && tmp = EAX then + fprintf oc " popl %a\n" ireg EAX + +let print_builtin_memcpy_big oc sz al src dst = + fprintf oc " pushl %a\n" ireg ESI; + fprintf oc " pushl %a\n" ireg EDI; + begin match src, dst with + | ESI, EDI -> () + | EDI, ESI -> fprintf oc " xchgl %a, %a\n" ireg ESI ireg EDI + | ESI, _ -> fprintf oc " movl %a, %a\n" ireg dst ireg EDI + | _, EDI -> fprintf oc " movl %a, %a\n" ireg src ireg ESI + | _, _ -> fprintf oc " movl %a, %a\n" ireg src ireg ESI; + fprintf oc " movl %a, %a\n" ireg dst ireg EDI + end; + fprintf oc " movl $%d, %a\n" (sz / 4) ireg ECX; + fprintf oc " rep movsl\n"; + if sz mod 4 >= 2 then fprintf oc " movsw\n"; + if sz mod 2 >= 1 then fprintf oc " movsb\n"; + fprintf oc " popl %a\n" ireg EDI; + fprintf oc " popl %a\n" ireg ESI + +let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in + fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" + comment sz al; + if sz <= 64 + then print_builtin_memcpy_small oc sz al src dst + else print_builtin_memcpy_big oc sz al src dst; + fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment (* Handling of volatile reads and writes *) @@ -414,47 +444,6 @@ let print_builtin_inline oc name args res = end; fprintf oc "%s end builtin %s\n" comment name -(* Handling of other builtins *) - -let re_builtin_function = Str.regexp "__builtin_" - -let is_builtin_function s = - Str.string_match re_builtin_function (extern_atom s) 0 - -let print_memcpy oc sz = - fprintf oc " movl %%esi, %%eax\n"; (* Preserve esi, edi *) - fprintf oc " movl %%edi, %%edx\n"; - fprintf oc " movl 0(%%esp), %%edi\n"; (* Load args *) - fprintf oc " movl 4(%%esp), %%esi\n"; - fprintf oc " movl 8(%%esp), %%ecx\n"; - fprintf oc " shr $2, %%ecx\n"; - fprintf oc " rep movsl\n"; (* Copy by words *) - if sz < 4 then begin - fprintf oc " movl 8(%%esp), %%ecx\n"; - fprintf oc " andl $3, %%ecx\n"; - fprintf oc " rep movsb\n" (* Finish copy by bytes *) - end; - fprintf oc " movl %%eax, %%esi\n"; (* Restore esi, edi *) - fprintf oc " movl %%edx, %%edi\n" - -let print_builtin_function oc s = - fprintf oc "%s begin builtin function %s\n" comment (extern_atom s); - (* arguments: on stack, starting at offset 0 *) - (* result: EAX or ST0 *) - begin match extern_atom s with - (* Block copy *) - | "__builtin_memcpy" -> - print_memcpy oc 1 - | "__builtin_memcpy_al2" -> - print_memcpy oc 2 - | "__builtin_memcpy_al4" | "__builtin_memcpy_al8" -> - print_memcpy oc 4 - (* Catch-all *) - | s -> - invalid_arg ("unrecognized builtin function " ^ s) - end; - fprintf oc "%s end builtin function %s\n" comment (extern_atom s) - (* Printing of instructions *) let float_literals : (int * int64) list ref = ref [] @@ -631,12 +620,7 @@ let print_instruction oc = function | Pjmp_l(l) -> fprintf oc " jmp %a\n" label (transl_label l) | Pjmp_s(f) -> - if not (is_builtin_function f) then - fprintf oc " jmp %a\n" symbol f - else begin - print_builtin_function oc f; - fprintf oc " ret\n" - end + fprintf oc " jmp %a\n" symbol f | Pjmp_r(r) -> fprintf oc " jmp *%a\n" ireg r | Pjcc(c, l) -> @@ -658,10 +642,7 @@ let print_instruction oc = function fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r; jumptables := (l, tbl) :: !jumptables | Pcall_s(f) -> - if not (is_builtin_function f) then - fprintf oc " call %a\n" symbol f - else - print_builtin_function oc f + fprintf oc " call %a\n" symbol f | Pcall_r(r) -> fprintf oc " call *%a\n" ireg r | Pret -> diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index efe5b98..0567f3f 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -316,14 +316,12 @@ let print_annot_val oc txt args res = (* On the PowerPC, unaligned accesses to 16- and 32-bit integers are fast, but unaligned accesses to 64-bit floats can be slow (not so much on G5, but clearly so on Power7). - So, use 64-bit accesses only if alignment >= 8. + So, use 64-bit accesses only if alignment >= 4. Note that lfd and stfd cannot trap on ill-formed floats. *) -let print_builtin_memcpy oc sz al args = - let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in +let print_builtin_memcpy_small oc sz al src dst = let rec copy ofs sz = - if sz >= 8 && al >= 8 then begin + if sz >= 8 && al >= 4 then begin fprintf oc " lfd %a, %d(%a)\n" freg FPR0 ofs ireg src; fprintf oc " stfd %a, %d(%a)\n" freg FPR0 ofs ireg dst; copy (ofs + 8) (sz - 8) @@ -340,10 +338,40 @@ let print_builtin_memcpy oc sz al args = fprintf oc " stb %a, %d(%a)\n" ireg GPR0 ofs ireg dst; copy (ofs + 1) (sz - 1) end in - fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n" + copy 0 sz + +let print_builtin_memcpy_big oc sz al src dst = + assert (sz >= 4); + fprintf oc " li %a, %d\n" ireg GPR0 (sz / 4); + fprintf oc " mtctr %a\n" ireg GPR0; + let (s,d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in + fprintf oc " addi %a, %a, -4\n" ireg s ireg src; + fprintf oc " addi %a, %a, -4\n" ireg d ireg dst; + let lbl = new_label() in + fprintf oc "%a: lwzu %a, 4(%a)\n" ireg GPR0 ireg s; + fprintf oc " stwu %a, 4(%a)\n" ireg GPR0 ireg d; + fprintf oc " bdnz %a\n" label lbl; + (* s and d lag behind by 4 bytes *) + match sz land 3 with + | 1 -> fprintf oc " lbz %a, 4(%a)\n" ireg GPR0 ireg s; + fprintf oc " stb %a, 4(%a)\n" ireg GPR0 ireg d + | 2 -> fprintf oc " lhz %a, 4(%a)\n" ireg GPR0 ireg s; + fprintf oc " sth %a, 4(%a)\n" ireg GPR0 ireg d + | 3 -> fprintf oc " lhz %a, 4(%a)\n" ireg GPR0 ireg s; + fprintf oc " sth %a, 4(%a)\n" ireg GPR0 ireg d; + fprintf oc " lbz %a, 6(%a)\n" ireg GPR0 ireg s; + fprintf oc " stb %a, 6(%a)\n" ireg GPR0 ireg d + | _ -> () + +let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in + fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" comment sz al; - copy 0 sz; - fprintf oc "%s end builtin __builtin_memcpy\n" comment + if sz <= 64 + then print_builtin_memcpy_small oc sz al src dst + else print_builtin_memcpy_big oc sz al src dst; + fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment (* Handling of volatile reads and writes *) @@ -441,61 +469,6 @@ let print_builtin_inline oc name args res = end; fprintf oc "%s end builtin %s\n" comment name -(* Handling of other builtins *) - -let re_builtin_function = Str.regexp "__builtin_" - -let is_builtin_function s = - Str.string_match re_builtin_function (extern_atom s) 0 - -let print_memcpy oc sz prepare load store = - let lbl1 = new_label() in - let lbl2 = new_label() in - prepare GPR5; - fprintf oc " beq %a, %a\n" creg 0 label lbl1; - fprintf oc " mtctr %a\n" ireg GPR5; - fprintf oc " addi %a, %a, -%d\n" ireg GPR3 ireg GPR3 sz; - fprintf oc " addi %a, %a, -%d\n" ireg GPR4 ireg GPR4 sz; - fprintf oc "%a:\n" label lbl2; - load GPR4; - store GPR3; - fprintf oc " bdnz %a\n" label lbl2; - fprintf oc "%a:\n" label lbl1 - -let print_builtin_function oc s = - fprintf oc "%s begin builtin function %s\n" comment (extern_atom s); - (* int args: GPR3, GPR4, GPR5 float args: FPR1, FPR2, FPR3 - int res: GPR3 float res: FPR1 - Watch out for MacOSX/EABI incompatibility: functions that take - some floats then some ints. There are none here. *) - (* Block copy *) - begin match extern_atom s with - | "__builtin_memcpy" -> - print_memcpy oc 1 - (fun r -> fprintf oc " cmplwi %a, %a, 0\n" creg 0 ireg r) - (fun r -> fprintf oc " lbzu %a, 1(%a)\n" ireg GPR0 ireg r) - (fun r -> fprintf oc " stbu %a, 1(%a)\n" ireg GPR0 ireg r) - | "__builtin_memcpy_al2" -> - print_memcpy oc 2 - (fun r -> fprintf oc " rlwinm. %a, %a, 31, 1, 31\n" ireg r ireg r) - (fun r -> fprintf oc " lhzu %a, 2(%a)\n" ireg GPR0 ireg r) - (fun r -> fprintf oc " sthu %a, 2(%a)\n" ireg GPR0 ireg r) - | "__builtin_memcpy_al4" -> - print_memcpy oc 4 - (fun r -> fprintf oc " rlwinm. %a, %a, 30, 2, 31\n" ireg r ireg r) - (fun r -> fprintf oc " lwzu %a, 4(%a)\n" ireg GPR0 ireg r) - (fun r -> fprintf oc " stwu %a, 4(%a)\n" ireg GPR0 ireg r) - | "__builtin_memcpy_al8" -> - print_memcpy oc 8 - (fun r -> fprintf oc " rlwinm. %a, %a, 29, 3, 31\n" ireg r ireg r) - (fun r -> fprintf oc " lfdu %a, 8(%a)\n" freg FPR0 ireg r) - (fun r -> fprintf oc " stfdu %a, 8(%a)\n" freg FPR0 ireg r) - (* Catch-all *) - | s -> - invalid_arg ("unrecognized builtin function " ^ s) - end; - fprintf oc "%s end builtin function %s\n" comment (extern_atom s) - (* Printing of instructions *) let float_literals : (int * int64) list ref = ref [] @@ -543,17 +516,9 @@ let print_instruction oc = function | Pbf(bit, lbl) -> fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl) | Pbl s -> - if not (is_builtin_function s) then - fprintf oc " bl %a\n" symbol s - else - print_builtin_function oc s + fprintf oc " bl %a\n" symbol s | Pbs s -> - if not (is_builtin_function s) then - fprintf oc " b %a\n" symbol s - else begin - print_builtin_function oc s; - fprintf oc " blr\n" - end + fprintf oc " b %a\n" symbol s | Pblr -> fprintf oc " blr\n" | Pbt(bit, lbl) -> @@ -955,15 +920,18 @@ let print_fundef oc (Coq_pair(name, defn)) = match defn with | Internal code -> print_function oc name code - | External ef -> - if not (is_builtin_function name) then stub_function oc name (ef_sig ef) + | External (EF_external _ as ef) -> + if function_needs_stub name then stub_function oc name (ef_sig ef) + | External _ -> + () let record_extfun (Coq_pair(name, defn)) = match defn with | Internal _ -> () - | External _ -> - if function_needs_stub name && not (is_builtin_function name) then + | External (EF_external _) -> + if function_needs_stub name then stubbed_functions := IdentSet.add name !stubbed_functions + | External _ -> () let print_init oc = function | Init_int8 n -> diff --git a/test/regression/expr1.c b/test/regression/expr1.c index 132ce44..10c9ea6 100644 --- a/test/regression/expr1.c +++ b/test/regression/expr1.c @@ -7,7 +7,7 @@ struct list * f(struct list ** p) return ((*p)->tl = 0); } -int main(int argc, char ** argv) +int main() { struct list l; l.tl = &l; diff --git a/test/regression/initializers.c b/test/regression/initializers.c index 7384091..c16a356 100644 --- a/test/regression/initializers.c +++ b/test/regression/initializers.c @@ -46,7 +46,7 @@ char * x18 = "Hello!"; char * x19[2] = { "Hello", "world!" }; -int main(int argc, char ** argv) +int main() { int i; diff --git a/test/regression/volatile2.c b/test/regression/volatile2.c index d83927b..0608650 100644 --- a/test/regression/volatile2.c +++ b/test/regression/volatile2.c @@ -8,7 +8,7 @@ *((ty *) &x) = v2; \ printf("%s 2: %s\n", msg, *((volatile ty *) &x) == v2 ? "OK" : "FAILED"); -int main(int argc, char ** argv) +int main() { signed char sc; unsigned char uc; |