diff options
| -rw-r--r-- | cfrontend/C2C.ml | 49 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 4 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 2 | ||||
| -rwxr-xr-x | configure | 10 | ||||
| -rw-r--r-- | test/c/sha1.c | 2 | ||||
| -rw-r--r-- | test/regression/Makefile | 12 | ||||
| -rw-r--r-- | test/regression/Results/initializers | 1 | ||||
| -rw-r--r-- | test/regression/initializers.c | 6 |
8 files changed, 29 insertions, 57 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d4faa2b..a5a9fee 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -74,14 +74,6 @@ let builtins_generic = { (* Floating-point absolute value *) "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); - (* Block copy *) - "__builtin_memcpy_aligned", - (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, []); - TInt(Cutil.size_t_ikind, [])], - false); (* Annotations *) "__builtin_annot", (TVoid [], @@ -200,36 +192,6 @@ let register_annotation_val txt targ = Evalof(Evar(intern_string fun_name, Tfunction(targs, tres)), Tfunction(targs, tres)) -(** ** Handling of inlined memcpy functions *) - -let register_inlined_memcpy sz al = - let al = - 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, noattr), - Tcons(Tpointer(Tvoid, noattr), Tnil)) - and tres = Tvoid - and ef = EF_memcpy(coqint_of_camlint sz, coqint_of_camlint al) in - register_special_external name ef targs tres; - Evalof(Evar(intern_string name, Tfunction(targs, tres)), - Tfunction(targs, tres)) - -let make_builtin_memcpy args = - match args with - | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) -> - let sz1 = - match Initializers.constval sz with - | 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) - | _ -> - assert false - (** ** Translation functions *) (** Constants *) @@ -550,9 +512,6 @@ let rec convertExpr env e = ezero end - | 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 | None -> @@ -588,14 +547,14 @@ and convertLvalue env e = | C.EUnop(C.Oderef, e1) -> Ederef(convertExpr env e1, ty) | C.EUnop(C.Odot id, e1) -> - Efield(convertLvalue env e1, intern_string id, ty) + Efield(convertExpr env e1, intern_string id, ty) | C.EUnop(C.Oarrow id, e1) -> let e1' = convertExpr env e1 in let ty1 = match typeof e1' with | Tpointer(t, _) -> t | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in - Efield(Ederef(e1', ty1), intern_string id, ty) + Efield(Evalof(Ederef(e1', ty1), ty1), intern_string id, ty) | C.EBinop(C.Oindex, e1, e2, _) -> coq_Eindex (convertExpr env e1) (convertExpr env e2) ty | _ -> @@ -784,7 +743,9 @@ let convertInitializer env ty i = match Initializers.transl_init (convertTyp env ty) (convertInit env i) with | CompcertErrors.OK init -> init - | CompcertErrors.Error msg -> error (string_of_errmsg msg); [] + | CompcertErrors.Error msg -> + error (sprintf "Initializer is not a compile-time constant (%s)" + (string_of_errmsg msg)); [] (** Global variable *) diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index e9c40a2..9690ba8 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -58,8 +58,8 @@ Fixpoint constval (a: expr) : res val := end | Evalof l ty => match access_mode ty with - | By_reference => constval l - | _ => Error(msg "dereference operation") + | By_reference | By_copy => constval l + | _ => Error(msg "dereferencing of an l-value") end | Eaddrof l ty => constval l diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 4d287bc..057933e 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -445,7 +445,7 @@ Proof. (* val *) destruct v; monadInv CV; constructor. (* rval *) - inv H1; rewrite H2 in CV; try congruence. eauto. + inv H1; rewrite H2 in CV; try congruence. eauto. eauto. (* addrof *) eauto. (* unop *) @@ -17,16 +17,6 @@ bindir='$(PREFIX)/bin' libdir='$(PREFIX)/lib/compcert' target='' -prompt() { - echo "$1 [$x] ? " | tr -d '\n' - read y - case "$y" in - "") ;; - none) x="";; - *) x="$y";; - esac -} - usage='Usage: ./configure [options] target Supported targets: diff --git a/test/c/sha1.c b/test/c/sha1.c index 7ea413a..84d0072 100644 --- a/test/c/sha1.c +++ b/test/c/sha1.c @@ -210,7 +210,9 @@ static void do_bench(int nblocks) struct SHA1Context ctx; unsigned char output[20]; unsigned char data[64]; + int i; + for (i = 0; i < 64; i++) data[i] = i; SHA1_init(&ctx); for (; nblocks > 0; nblocks--) SHA1_add_data(&ctx, data, 64); diff --git a/test/regression/Makefile b/test/regression/Makefile index e9d0318..186bddd 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -44,4 +44,16 @@ test: fi; \ done +interp: + @for i in $(TESTS); do \ + if $(CCOMP) -fall -interp 2>/dev/null $$i.c > _cinterp.log; then \ + if cmp -s _cinterp.log Results/$$i; \ + then echo "$$i: interpreter passed"; \ + else echo "$$i: interpreter FAILED"; \ + fi; \ + else \ + echo "$$i: interpreter undefined behavior"; \ + fi; \ + done + bench: diff --git a/test/regression/Results/initializers b/test/regression/Results/initializers index 67460cc..d3fc91a 100644 --- a/test/regression/Results/initializers +++ b/test/regression/Results/initializers @@ -19,3 +19,4 @@ x18 = "Hello!" x19 = { "Hello", "world!" } x20 = { 'H', 'e', 'l', } x21 = { 'H', 'e', 'l', 'l', 'o', '!', 0, 0, 0, 0, } +x22 ok diff --git a/test/regression/initializers.c b/test/regression/initializers.c index a0913fd..f831c67 100644 --- a/test/regression/initializers.c +++ b/test/regression/initializers.c @@ -50,6 +50,8 @@ char x20[3] = "Hello!"; char x21[10] = "Hello!"; +char * x22 = &(x10.u.y); + static void print_chars(char * s, int sz) { int i; @@ -106,6 +108,10 @@ int main() printf("x21 = { "); print_chars(x21, sizeof(x21)); printf("}\n"); + if (x22 == &(x10.u.y)) + printf("x22 ok\n"); + else + printf("x22 error\n"); return 0; } |