Skip to content

Instantly share code, notes, and snippets.

@agl agl/test.c
Created Sep 13, 2014

Embed
What would you like to do?
VST forward issue.
#include <stdint.h>
typedef int64_t limb;
typedef int32_t s32;
void product(limb out[19], const limb *a, const limb *b) {
s32 t1, t2;
t1 = a[0];
t2 = b[0];
out[0] = (limb) t1 * t2;
}
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.
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.
apply cast_l2i.
exact H4.
forward.
entailer!.
assert(is_long (orig_b 0)).
apply H1 with (i:=0).
omega.
apply cast_l2i.
exact H5.
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.