Skip to content

Instantly share code, notes, and snippets.

@agl agl/test1.v
Created Oct 4, 2014

Embed
What would you like to do?
VST forward issue (VST 1.5, Coq 8.4p4, CompCert 2.4)
Require Import Clightdefs.
Require Import floyd.proofauto.
Require Import Coq.ZArith.Zdiv.
Require Import compcert.common.Values.
Local Open Scope Z_scope.
Definition _b : ident := 32%positive.
Definition ___compcert_va_int64 : ident := 16%positive.
Definition ___builtin_fmadd : ident := 24%positive.
Definition ___builtin_fmax : ident := 22%positive.
Definition ___compcert_va_float64 : ident := 17%positive.
Definition ___builtin_memcpy_aligned : ident := 8%positive.
Definition ___builtin_subl : ident := 5%positive.
Definition ___builtin_va_arg : ident := 12%positive.
Definition ___builtin_annot_intval : ident := 10%positive.
Definition ___builtin_negl : ident := 3%positive.
Definition ___builtin_write32_reversed : ident := 2%positive.
Definition ___builtin_write16_reversed : ident := 1%positive.
Definition _main : ident := 36%positive.
Definition _a : ident := 31%positive.
Definition ___builtin_va_end : ident := 14%positive.
Definition ___builtin_mull : ident := 6%positive.
Definition ___builtin_fnmadd : ident := 26%positive.
Definition ___builtin_bswap32 : ident := 19%positive.
Definition ___builtin_va_start : ident := 11%positive.
Definition ___builtin_addl : ident := 4%positive.
Definition ___builtin_read16_reversed : ident := 28%positive.
Definition ___builtin_fabs : ident := 7%positive.
Definition ___builtin_fsqrt : ident := 21%positive.
Definition ___builtin_bswap : ident := 18%positive.
Definition ___builtin_annot : ident := 9%positive.
Definition ___builtin_va_copy : ident := 13%positive.
Definition ___builtin_fnmsub : ident := 27%positive.
Definition _t1 : ident := 33%positive.
Definition ___builtin_fmsub : ident := 25%positive.
Definition ___compcert_va_int32 : ident := 15%positive.
Definition _t2 : ident := 34%positive.
Definition ___builtin_read32_reversed : ident := 29%positive.
Definition _product : ident := 35%positive.
Definition _out : ident := 30%positive.
Definition ___builtin_fmin : ident := 23%positive.
Definition ___builtin_bswap16 : ident := 20%positive.
Definition f_product := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_out, (tptr tlong)) :: (_a, (tptr tlong)) ::
(_b, (tptr tlong)) :: nil);
fn_vars := nil;
fn_temps := ((_t1, tint) :: (_t2, tint) :: nil);
fn_body :=
(Ssequence
(Sset _t1
(Ecast
(Ederef
(Ebinop Oadd (Etempvar _a (tptr tlong))
(Econst_int (Int.repr 0) tint) (tptr tlong)) tlong) tint))
(Ssequence
(Sset _t2
(Ecast
(Ederef
(Ebinop Oadd (Etempvar _b (tptr tlong))
(Econst_int (Int.repr 0) tint) (tptr tlong)) tlong) tint))
(Sassign
(Ederef
(Ebinop Oadd (Etempvar _out (tptr tlong))
(Econst_int (Int.repr 0) tint) (tptr tlong)) tlong)
(Ebinop Omul (Ecast (Etempvar _t1 tint) tlong) (Etempvar _t2 tint)
tlong))))
|}.
Definition prog : Clight.program := {|
prog_defs :=
((___builtin_fabs,
Gfun(External (EF_builtin ___builtin_fabs
(mksignature (AST.Tfloat :: nil) (Some AST.Tfloat)
cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) ::
(___builtin_memcpy_aligned,
Gfun(External (EF_builtin ___builtin_memcpy_aligned
(mksignature
(AST.Tint :: AST.Tint :: AST.Tint :: AST.Tint :: nil)
None cc_default))
(Tcons (tptr tvoid)
(Tcons (tptr tvoid) (Tcons tuint (Tcons tuint Tnil)))) tvoid
cc_default)) ::
(___builtin_annot,
Gfun(External (EF_builtin ___builtin_annot
(mksignature (AST.Tint :: nil) None
{|cc_vararg:=true; cc_structret:=false|}))
(Tcons (tptr tschar) Tnil) tvoid
{|cc_vararg:=true; cc_structret:=false|})) ::
(___builtin_annot_intval,
Gfun(External (EF_builtin ___builtin_annot_intval
(mksignature (AST.Tint :: AST.Tint :: nil) (Some AST.Tint)
cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil))
tint cc_default)) ::
(___builtin_va_start,
Gfun(External (EF_builtin ___builtin_va_start
(mksignature (AST.Tint :: nil) None cc_default))
(Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
(___builtin_va_arg,
Gfun(External (EF_builtin ___builtin_va_arg
(mksignature (AST.Tint :: AST.Tint :: nil) None
cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
tvoid cc_default)) ::
(___builtin_va_copy,
Gfun(External (EF_builtin ___builtin_va_copy
(mksignature (AST.Tint :: AST.Tint :: nil) None
cc_default))
(Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) ::
(___builtin_va_end,
Gfun(External (EF_builtin ___builtin_va_end
(mksignature (AST.Tint :: nil) None cc_default))
(Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
(___compcert_va_int32,
Gfun(External (EF_external ___compcert_va_int32
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons (tptr tvoid) Tnil) tuint cc_default)) ::
(___compcert_va_int64,
Gfun(External (EF_external ___compcert_va_int64
(mksignature (AST.Tint :: nil) (Some AST.Tlong)
cc_default)) (Tcons (tptr tvoid) Tnil) tulong
cc_default)) ::
(___compcert_va_float64,
Gfun(External (EF_external ___compcert_va_float64
(mksignature (AST.Tint :: nil) (Some AST.Tfloat)
cc_default)) (Tcons (tptr tvoid) Tnil) tdouble
cc_default)) ::
(___builtin_bswap,
Gfun(External (EF_builtin ___builtin_bswap
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons tuint Tnil) tuint cc_default)) ::
(___builtin_bswap32,
Gfun(External (EF_builtin ___builtin_bswap32
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons tuint Tnil) tuint cc_default)) ::
(___builtin_bswap16,
Gfun(External (EF_builtin ___builtin_bswap16
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons tushort Tnil) tushort cc_default)) ::
(___builtin_fsqrt,
Gfun(External (EF_builtin ___builtin_fsqrt
(mksignature (AST.Tfloat :: nil) (Some AST.Tfloat)
cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) ::
(___builtin_fmax,
Gfun(External (EF_builtin ___builtin_fmax
(mksignature (AST.Tfloat :: AST.Tfloat :: nil)
(Some AST.Tfloat) cc_default))
(Tcons tdouble (Tcons tdouble Tnil)) tdouble cc_default)) ::
(___builtin_fmin,
Gfun(External (EF_builtin ___builtin_fmin
(mksignature (AST.Tfloat :: AST.Tfloat :: nil)
(Some AST.Tfloat) cc_default))
(Tcons tdouble (Tcons tdouble Tnil)) tdouble cc_default)) ::
(___builtin_fmadd,
Gfun(External (EF_builtin ___builtin_fmadd
(mksignature
(AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
(Some AST.Tfloat) cc_default))
(Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
cc_default)) ::
(___builtin_fmsub,
Gfun(External (EF_builtin ___builtin_fmsub
(mksignature
(AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
(Some AST.Tfloat) cc_default))
(Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
cc_default)) ::
(___builtin_fnmadd,
Gfun(External (EF_builtin ___builtin_fnmadd
(mksignature
(AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
(Some AST.Tfloat) cc_default))
(Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
cc_default)) ::
(___builtin_fnmsub,
Gfun(External (EF_builtin ___builtin_fnmsub
(mksignature
(AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
(Some AST.Tfloat) cc_default))
(Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
cc_default)) ::
(___builtin_read16_reversed,
Gfun(External (EF_builtin ___builtin_read16_reversed
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons (tptr tushort) Tnil) tushort cc_default)) ::
(___builtin_read32_reversed,
Gfun(External (EF_builtin ___builtin_read32_reversed
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons (tptr tuint) Tnil) tuint cc_default)) ::
(___builtin_write16_reversed,
Gfun(External (EF_builtin ___builtin_write16_reversed
(mksignature (AST.Tint :: AST.Tint :: nil) None
cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil))
tvoid cc_default)) ::
(___builtin_write32_reversed,
Gfun(External (EF_builtin ___builtin_write32_reversed
(mksignature (AST.Tint :: AST.Tint :: nil) None
cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil))
tvoid cc_default)) :: (_product, Gfun(Internal f_product)) :: nil);
prog_main := _main
|}.
Definition bound_int (v : val) (b : Z) :=
match v with
| Vint i => -b < (Int.signed i) < b
| _ => False
end.
Definition product (a : Z -> val) (b : Z -> val) (i : Z) :=
Val.mul (a i) (b i).
Definition product_spec :=
DECLARE _product
WITH b0 : val, sh : share, orig_a : Z -> val, orig_b : Z -> val, result : Z -> val, out0 : val, a0 : val
PRE [_out OF (tptr tlong), _a OF (tptr tint), _b OF (tptr tint)]
PROP (writable_share sh;
forall i, 0 <= i < 10 -> is_long (orig_a i);
forall i, 0 <= i < 10 -> is_long (orig_b i);
forall i, 0 <= i < 10 -> bound_int (orig_a i) 134217728;
forall i, 0 <= i < 10 -> bound_int (orig_b i) 134217728)
LOCAL (`(eq out0) (eval_id _out);
`(eq a0) (eval_id _a);
`(eq b0) (eval_id _b);
`isptr (eval_id _out);
`isptr (eval_id _a);
`isptr (eval_id _b))
SEP (`(array_at tlong sh orig_a 0 10 a0);
`(array_at tlong sh orig_b 0 10 b0);
`(array_at_ tlong sh 0 1 out0))
POST [ tvoid ]
PROP ()
LOCAL ()
SEP (`(array_at tlong sh (product orig_a orig_b) 0 1 out0);
`(array_at tlong sh orig_a 0 10 a0);
`(array_at tlong sh orig_b 0 10 b0)).
Local Open Scope logic.
Definition Vprog : varspecs := nil.
Definition Gprog : funspecs := product_spec :: nil.
Lemma cast_l2i : forall (x : val), is_long x -> is_int (force_val (sem_cast_l2i I32 Signed x)).
Proof.
intros.
unfold force_val, sem_cast_l2i.
induction x.
auto.
auto.
Focus 2.
auto.
Focus 2.
auto.
auto.
auto.
Qed.
Lemma product_sumarray : semax_body Vprog Gprog f_product product_spec.
Proof.
start_function.
forward.
entailer!.
assert(is_long (orig_a 0)).
apply H0 with (i:=0).
omega.
omega.
apply cast_l2i.
apply H0.
omega.
forward.
entailer!.
omega.
assert(is_long (orig_b 0)).
apply H1 with (i:=0).
omega.
apply cast_l2i.
apply H1.
omega.
forward.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.