Skip to content

Instantly share code, notes, and snippets.

@ildyria

ildyria/details.md

Created January 4, 2018 16:43
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save ildyria/8604984298dfcc9234e776be4197181b to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save ildyria/8604984298dfcc9234e776be4197181b to your computer and use it in GitHub Desktop.
Download ZIP
Problem with operations between Int and Long on VST.
Raw
details.md

Compilation

The test.c file can be compiled as follow:

gcc test.c -Wall -Wextra -o test

or with Compcert (2.7.2)

ccomp test.c -o test

or interpreted with Compcert (2.7.2)

ccomp -interp test.c

In all these cases, no error or warning will be returned which leads to the thought that test.c is a valide C11 file.

VST typechecking

In test.c I test the different operations ( +, -, *, >> and <<) with either side of the operand being a constant (thus of type Int). I also test assignment to a uchar which does not typecast.

Please execute the .v file in order to see precisely the errors.

Raw
test.c
#define sv static void
#include <stdio.h>
typedef unsigned char u8;
typedef unsigned long u32;
typedef unsigned long long u64;
typedef __attribute__((aligned(8))) long long i64;
u8 test_simpl(const i64 n)
{
i64 b,c;
u8 d;
b = n * 2;
c = 2 * n;
b = b + 4;
b = (-4) + b;
c = c - 4;
c = 4 - c;
b = b >> 8;
c = c << 8;
d = c & 0xff;
d = d & b;
return d;
}
int main () {
printf("%i\n",test_simpl(5));
return 0;
}
Raw
test.v
Require Import VST.floyd.proofauto.
Local Open Scope Z_scope.
Definition ___builtin_annot : ident := 3%positive.
Definition ___builtin_annot_intval : ident := 4%positive.
Definition ___builtin_bswap : ident := 27%positive.
Definition ___builtin_bswap16 : ident := 29%positive.
Definition ___builtin_bswap32 : ident := 28%positive.
Definition ___builtin_clz : ident := 30%positive.
Definition ___builtin_clzl : ident := 31%positive.
Definition ___builtin_clzll : ident := 32%positive.
Definition ___builtin_ctz : ident := 33%positive.
Definition ___builtin_ctzl : ident := 34%positive.
Definition ___builtin_ctzll : ident := 35%positive.
Definition ___builtin_debug : ident := 48%positive.
Definition ___builtin_fabs : ident := 1%positive.
Definition ___builtin_fmadd : ident := 39%positive.
Definition ___builtin_fmax : ident := 37%positive.
Definition ___builtin_fmin : ident := 38%positive.
Definition ___builtin_fmsub : ident := 40%positive.
Definition ___builtin_fnmadd : ident := 41%positive.
Definition ___builtin_fnmsub : ident := 42%positive.
Definition ___builtin_fsqrt : ident := 36%positive.
Definition ___builtin_membar : ident := 5%positive.
Definition ___builtin_memcpy_aligned : ident := 2%positive.
Definition ___builtin_nop : ident := 47%positive.
Definition ___builtin_read16_reversed : ident := 43%positive.
Definition ___builtin_read32_reversed : ident := 44%positive.
Definition ___builtin_va_arg : ident := 7%positive.
Definition ___builtin_va_copy : ident := 8%positive.
Definition ___builtin_va_end : ident := 9%positive.
Definition ___builtin_va_start : ident := 6%positive.
Definition ___builtin_write16_reversed : ident := 45%positive.
Definition ___builtin_write32_reversed : ident := 46%positive.
Definition ___compcert_va_composite : ident := 13%positive.
Definition ___compcert_va_float64 : ident := 12%positive.
Definition ___compcert_va_int32 : ident := 10%positive.
Definition ___compcert_va_int64 : ident := 11%positive.
Definition ___i64_dtos : ident := 14%positive.
Definition ___i64_dtou : ident := 15%positive.
Definition ___i64_sar : ident := 26%positive.
Definition ___i64_sdiv : ident := 20%positive.
Definition ___i64_shl : ident := 24%positive.
Definition ___i64_shr : ident := 25%positive.
Definition ___i64_smod : ident := 22%positive.
Definition ___i64_stod : ident := 16%positive.
Definition ___i64_stof : ident := 18%positive.
Definition ___i64_udiv : ident := 21%positive.
Definition ___i64_umod : ident := 23%positive.
Definition ___i64_utod : ident := 17%positive.
Definition ___i64_utof : ident := 19%positive.
Definition ___stringlit_1 : ident := 55%positive.
Definition _b : ident := 51%positive.
Definition _c : ident := 52%positive.
Definition _d : ident := 53%positive.
Definition _main : ident := 56%positive.
Definition _n : ident := 50%positive.
Definition _printf : ident := 49%positive.
Definition _test_simpl : ident := 54%positive.
Definition _t'1 : ident := 57%positive.
Definition v___stringlit_1 := {|
gvar_info := (tarray tschar 4);
gvar_init := (Init_int8 (Int.repr 37) :: Init_int8 (Int.repr 105) ::
Init_int8 (Int.repr 10) :: Init_int8 (Int.repr 0) :: nil);
gvar_readonly := true;
gvar_volatile := false
|}.
Definition f_test_simpl := {|
fn_return := tuchar;
fn_callconv := cc_default;
fn_params := ((_n, tlong) :: nil);
fn_vars := nil;
fn_temps := ((_b, tlong) :: (_c, tlong) :: (_d, tuchar) :: nil);
fn_body :=
(Ssequence
(Sset _b
(Ebinop Omul (Etempvar _n tlong) (Econst_int (Int.repr 2) tint) tlong))
(Ssequence
(Sset _c
(Ebinop Omul (Econst_int (Int.repr 2) tint) (Etempvar _n tlong) tlong))
(Ssequence
(Sset _b
(Ebinop Oadd (Etempvar _b tlong) (Econst_int (Int.repr 4) tint)
tlong))
(Ssequence
(Sset _b
(Ebinop Oadd (Eunop Oneg (Econst_int (Int.repr 4) tint) tint)
(Etempvar _b tlong) tlong))
(Ssequence
(Sset _c
(Ebinop Osub (Etempvar _c tlong) (Econst_int (Int.repr 4) tint)
tlong))
(Ssequence
(Sset _c
(Ebinop Osub (Econst_int (Int.repr 4) tint) (Etempvar _c tlong)
tlong))
(Ssequence
(Sset _b
(Ebinop Oshr (Etempvar _b tlong)
(Econst_int (Int.repr 8) tint) tlong))
(Ssequence
(Sset _c
(Ebinop Oshl (Etempvar _c tlong)
(Econst_int (Int.repr 8) tint) tlong))
(Ssequence
(Sset _d
(Ecast
(Ebinop Oand (Etempvar _c tlong)
(Econst_int (Int.repr 255) tint) tlong) tuchar))
(Ssequence
(Sset _d
(Ecast
(Ebinop Oand (Etempvar _d tuchar) (Etempvar _b tlong)
tlong) tuchar))
(Sreturn (Some (Etempvar _d tuchar)))))))))))))
|}.
Definition f_main := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := ((_t'1, tuchar) :: nil);
fn_body :=
(Ssequence
(Ssequence
(Ssequence
(Scall (Some _t'1)
(Evar _test_simpl (Tfunction (Tcons tlong Tnil) tuchar cc_default))
((Econst_int (Int.repr 5) tint) :: nil))
(Scall None
(Evar _printf (Tfunction (Tcons (tptr tschar) Tnil) tint
{|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
((Evar ___stringlit_1 (tarray tschar 4)) :: (Etempvar _t'1 tuchar) ::
nil)))
(Sreturn (Some (Econst_int (Int.repr 0) tint))))
(Sreturn (Some (Econst_int (Int.repr 0) tint))))
|}.
Definition composites : list composite_definition :=
nil.
Definition prog : Clight.program := {|
prog_defs :=
((___stringlit_1, Gvar v___stringlit_1) ::
(___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_unproto:=false; cc_structret:=false|}))
(Tcons (tptr tschar) Tnil) tvoid
{|cc_vararg:=true; cc_unproto:=false; 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_membar,
Gfun(External (EF_builtin "__builtin_membar"
(mksignature nil None cc_default)) Tnil tvoid 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)) ::
(___compcert_va_composite,
Gfun(External (EF_external "__compcert_va_composite"
(mksignature (AST.Tint :: AST.Tint :: nil) (Some AST.Tint)
cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
(tptr tvoid) cc_default)) ::
(___i64_dtos,
Gfun(External (EF_runtime "__i64_dtos"
(mksignature (AST.Tfloat :: nil) (Some AST.Tlong)
cc_default)) (Tcons tdouble Tnil) tlong cc_default)) ::
(___i64_dtou,
Gfun(External (EF_runtime "__i64_dtou"
(mksignature (AST.Tfloat :: nil) (Some AST.Tlong)
cc_default)) (Tcons tdouble Tnil) tulong cc_default)) ::
(___i64_stod,
Gfun(External (EF_runtime "__i64_stod"
(mksignature (AST.Tlong :: nil) (Some AST.Tfloat)
cc_default)) (Tcons tlong Tnil) tdouble cc_default)) ::
(___i64_utod,
Gfun(External (EF_runtime "__i64_utod"
(mksignature (AST.Tlong :: nil) (Some AST.Tfloat)
cc_default)) (Tcons tulong Tnil) tdouble cc_default)) ::
(___i64_stof,
Gfun(External (EF_runtime "__i64_stof"
(mksignature (AST.Tlong :: nil) (Some AST.Tsingle)
cc_default)) (Tcons tlong Tnil) tfloat cc_default)) ::
(___i64_utof,
Gfun(External (EF_runtime "__i64_utof"
(mksignature (AST.Tlong :: nil) (Some AST.Tsingle)
cc_default)) (Tcons tulong Tnil) tfloat cc_default)) ::
(___i64_sdiv,
Gfun(External (EF_runtime "__i64_sdiv"
(mksignature (AST.Tlong :: AST.Tlong :: nil)
(Some AST.Tlong) cc_default))
(Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) ::
(___i64_udiv,
Gfun(External (EF_runtime "__i64_udiv"
(mksignature (AST.Tlong :: AST.Tlong :: nil)
(Some AST.Tlong) cc_default))
(Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) ::
(___i64_smod,
Gfun(External (EF_runtime "__i64_smod"
(mksignature (AST.Tlong :: AST.Tlong :: nil)
(Some AST.Tlong) cc_default))
(Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) ::
(___i64_umod,
Gfun(External (EF_runtime "__i64_umod"
(mksignature (AST.Tlong :: AST.Tlong :: nil)
(Some AST.Tlong) cc_default))
(Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) ::
(___i64_shl,
Gfun(External (EF_runtime "__i64_shl"
(mksignature (AST.Tlong :: AST.Tint :: nil)
(Some AST.Tlong) cc_default))
(Tcons tlong (Tcons tint Tnil)) tlong cc_default)) ::
(___i64_shr,
Gfun(External (EF_runtime "__i64_shr"
(mksignature (AST.Tlong :: AST.Tint :: nil)
(Some AST.Tlong) cc_default))
(Tcons tulong (Tcons tint Tnil)) tulong cc_default)) ::
(___i64_sar,
Gfun(External (EF_runtime "__i64_sar"
(mksignature (AST.Tlong :: AST.Tint :: nil)
(Some AST.Tlong) cc_default))
(Tcons tlong (Tcons tint Tnil)) tlong 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_clz,
Gfun(External (EF_builtin "__builtin_clz"
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons tuint Tnil) tint cc_default)) ::
(___builtin_clzl,
Gfun(External (EF_builtin "__builtin_clzl"
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons tuint Tnil) tint cc_default)) ::
(___builtin_clzll,
Gfun(External (EF_builtin "__builtin_clzll"
(mksignature (AST.Tlong :: nil) (Some AST.Tint)
cc_default)) (Tcons tulong Tnil) tint cc_default)) ::
(___builtin_ctz,
Gfun(External (EF_builtin "__builtin_ctz"
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons tuint Tnil) tint cc_default)) ::
(___builtin_ctzl,
Gfun(External (EF_builtin "__builtin_ctzl"
(mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default))
(Tcons tuint Tnil) tint cc_default)) ::
(___builtin_ctzll,
Gfun(External (EF_builtin "__builtin_ctzll"
(mksignature (AST.Tlong :: nil) (Some AST.Tint)
cc_default)) (Tcons tulong Tnil) tint 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)) ::
(___builtin_nop,
Gfun(External (EF_builtin "__builtin_nop"
(mksignature nil None cc_default)) Tnil tvoid cc_default)) ::
(___builtin_debug,
Gfun(External (EF_external "__builtin_debug"
(mksignature (AST.Tint :: nil) None
{|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
(Tcons tint Tnil) tvoid
{|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) ::
(_printf,
Gfun(External (EF_external "printf"
(mksignature (AST.Tint :: nil) (Some AST.Tint)
{|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
(Tcons (tptr tschar) Tnil) tint
{|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) ::
(_test_simpl, Gfun(Internal f_test_simpl)) ::
(_main, Gfun(Internal f_main)) :: nil);
prog_public :=
(_main :: _test_simpl :: _printf :: ___builtin_debug :: ___builtin_nop ::
___builtin_write32_reversed :: ___builtin_write16_reversed ::
___builtin_read32_reversed :: ___builtin_read16_reversed ::
___builtin_fnmsub :: ___builtin_fnmadd :: ___builtin_fmsub ::
___builtin_fmadd :: ___builtin_fmin :: ___builtin_fmax ::
___builtin_fsqrt :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz ::
___builtin_clzll :: ___builtin_clzl :: ___builtin_clz ::
___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap ::
___i64_sar :: ___i64_shr :: ___i64_shl :: ___i64_umod :: ___i64_smod ::
___i64_udiv :: ___i64_sdiv :: ___i64_utof :: ___i64_stof :: ___i64_utod ::
___i64_stod :: ___i64_dtou :: ___i64_dtos :: ___compcert_va_composite ::
___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 ::
___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg ::
___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval ::
___builtin_annot :: ___builtin_memcpy_aligned :: ___builtin_fabs :: nil);
prog_main := _main;
prog_types := composites;
prog_comp_env := make_composite_env composites;
prog_comp_env_eq := refl_equal _
|}.
(*
u8 test_simpl(const i64 n)
{
i64 b,c;
u8 d;
b = n * 2;
c = 2 * n;
b = b + 4;
b = (-4) + b;
c = c - 4;
c = 4 - c;
b = b >> 8;
c = c << 8;
d = c & 0xff;
d = d & b;
return d;
}
*)
(* The next line is "boilerplate", always required after importing an AST. *)
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Notation tlg := (Tlong Signed {| attr_volatile := false; attr_alignas := Some 3%N |}).
Definition test_simpl_spec :=
DECLARE _test_simpl
WITH n: Z
PRE [ _n OF tlong ]
PROP (0 <= n < Int.max_signed)
LOCAL (temp _n (Vlong (Int64.repr n)))
SEP ()
POST [ tuchar ]
PROP ()
LOCAL(temp ret_temp (Vint (Int.repr 0)))
SEP ().
(* Packaging the API spec all together. *)
Definition Gprog : funspecs :=
ltac:(with_library prog [test_simpl_spec]).
(*
u8 test_simpl(const i64 n)
{
i64 b,c;
u8 d;
b = n * 2;
c = 2 * n;
b = b >> 1;
c = c << 1;
d = c b;
return d;
}
*)
Lemma body_test_simpl: semax_body Vprog Gprog f_test_simpl test_simpl_spec.
Proof.
start_function.
forward. (* _b = (_n * (2) *)
simpl cast_int_long; rewrite Int.signed_repr by computable.
forward. (* _c = ((2) * _n *)
entailer!.
(* WHY ???
emp |-- FF
*)
admit.
forward. (* _b = (_b + (4)) *)
forward. (* _b = (- (4) + _b) *)
entailer!.
(* WHY ???
emp |-- FF
*)
admit.
forward. (* _c = (_c - (4)) *)
forward. (* _c = ((4) - _c) *)
entailer!.
(* WHY ???
emp |-- FF
*)
admit.
forward. (* _b = _b >> (8) *)
forward. (* _c = _c << (8) *)
forward. (* _d = (tuchar) (_c & (255)) *)
entailer!.
(* WHY ???
typecheck_error (invalid_cast_result tuchar tuchar)
*)
admit.
forward. (* _d = (tuchar) (_d & _b) *)
entailer!.
(* WHY ???
typecheck_error (invalid_cast_result tuchar tuchar)
*)
admit.
deadvars!. (* clean vars *)
forward. (* return _d; *)
entailer!.
clear H0 Delta Delta_specs Espec.
f_equal.
rewrite Int.zero_ext_and by omega.
rewrite Int.zero_ext_and by omega.
change (two_p 8 - 1) with (Z.ones 8).
rewrite and_repr.
rewrite mul64_repr.
rewrite mul64_repr.
rewrite add64_repr.
rewrite Int.neg_repr.
rewrite Int.signed_repr by computable.
rewrite add64_repr.
replace (- (4) + (n * 2 + 4)) with (n * 2) by omega.
rewrite sub64_repr.
rewrite sub64_repr.
replace (4 - (2 * n - 4)) with (-(n * 2) + 8) by omega.
rewrite Int64.shl_mul_two_p.
rewrite Int64.shr_div_two_p.
rewrite Int64.unsigned_repr.
Focus 2. (* 0 <= 8 <= Int64.max_unsigned *)
try computable. (* computable does not work here ??? WHY ? *)
compute ; split ; intro ; discriminate. (*ugly but whatever... *)
rewrite mul64_repr.
rewrite and64_repr.
rewrite and64_repr.
change 255 with (Z.ones 8).
rewrite Z.land_ones by omega.
rewrite Z.land_ones by omega.
rewrite Z_mod_mult.
rewrite (Int64.unsigned_repr 0).
Focus 2. (* 0 <= 0 <= Int64.max_unsigned *)
try computable. (* computable does not work here ??? WHY ? *)
compute ; split ; intro ; discriminate. (*ugly but whatever... *)
rewrite and_repr.
change (Z.land 0 (Z.ones 8)) with 0.
rewrite (Int.unsigned_repr 0).
Focus 2. (* 0 <= 0 <= Int.max_unsigned *)
computable. (* computable do work here! WHY ? *)
rewrite Z.land_0_l.
rewrite (Int64.unsigned_repr 0).
Focus 2. (* 0 <= 0 <= Int64.max_unsigned *)
try computable. (* computable does not work here ??? WHY ? *)
compute ; split ; intro ; discriminate. (*ugly but whatever... *)
reflexivity.
Admitted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment