Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Get 'make all' to work in VST 2.15, 32-bit mode #806

Merged
merged 6 commits into from
Jan 9, 2025
Merged

Get 'make all' to work in VST 2.15, 32-bit mode #806

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
73b100f
Get 'make all' to work in VST 2.15, 32-bit mode
andrew-appel Jan 9, 2025
afd9979
Update submodules
andrew-appel Jan 9, 2025
1c0c67f
Update release notes; tweak a coq-dev compatibility issue
andrew-appel Jan 9, 2025
22b7d21
Tweak the Coq-dev compatibility problem in a different way
andrew-appel Jan 9, 2025
3cf19dc
Another try to get fix_sub_eq_ext to work in coq.dev
andrew-appel Jan 9, 2025
36b3f14
Another try at fix_sub_eq_ext
andrew-appel Jan 9, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 0 additions & 5 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -334,11 +334,6 @@ DEPFLAGS:=$(COQFLAGS)

COQFLAGS+=$(COQEXTRAFLAGS)

# The following extra flags can probably be removed with Coq 8.21,
# after Coq pulls https://github.com/coq/coq/pull/19653
# and/or https://github.com/coq/coq/pull/19981 are merged.
COQFLAGS+= -w "-notation-incompatible-prefix,-automatic-prop-lowering"

PROFILING?=

ifneq (,$(PROFILING))
Expand Down
21 changes: 20 additions & 1 deletion floyd/printf.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,14 +140,33 @@ Proof.
eapply Z.lt_le_trans, Z_mult_div_ge with (b := 10); lia.
Defined.

Import Program.Wf.
Program Lemma fix_sub_eq_ext :
(* need to copy this from Coq standard library because it moved from
one location to another between Coq 8.20 and Coq 8.21 *)
forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
(P : A -> Type)
(F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
forall x : A,
Fix_sub A R Rwf P F_sub x =
F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
Proof.
intros A R Rwf P F_sub x; apply Fix_eq ; auto.
intros ? f g H.
assert(f = g) as H0.
- extensionality y ; apply H.
- rewrite H0 ; auto.
Qed.


Lemma chars_of_Z_eq : forall n, chars_of_Z n =
match n <? 0 with true => charminus :: chars_of_Z (Z.abs n) | false =>
let n' := n / 10 in
match n' <=? 0 with true => [Byte.repr (n + char0)] | false => chars_of_Z n' ++ [Byte.repr (n mod 10 + char0)] end end.
Proof.
intros.
unfold chars_of_Z at 1.
rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
destruct (_ <? _); auto.
destruct (_ <=? _); auto.
Qed.
Expand Down
3 changes: 3 additions & 0 deletions hmacdrbg/hmac_drbg.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,9 @@
#include <stddef.h>
#include "../sha/hmac.c"

void *malloc(size_t);
void free(void *);

struct mbedtls_md_info_t {
int dummy;
};
Expand Down
130 changes: 61 additions & 69 deletions hmacdrbg/hmac_drbg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Module Info.
Definition bitsize := 32.
Definition big_endian := false.
Definition source_file := "hmacdrbg/hmac_drbg.c".
Definition normalized := true.
Definition normalized := false.
End Info.

Definition _HMAC : ident := 118%positive.
Expand Down Expand Up @@ -117,32 +117,32 @@ Definition _e : ident := 53%positive.
Definition _entropy_len : ident := 128%positive.
Definition _f : ident := 54%positive.
Definition _fragment : ident := 74%positive.
Definition _free : ident := 153%positive.
Definition _free : ident := 133%positive.
Definition _g : ident := 55%positive.
Definition _get_entropy : ident := 155%positive.
Definition _h : ident := 2%positive.
Definition _hmac : ident := 142%positive.
Definition _hmac : ident := 143%positive.
Definition _hmac_ctx : ident := 124%positive.
Definition _hmac_ctx_st : ident := 101%positive.
Definition _i : ident := 64%positive.
Definition _i_ctx : ident := 103%positive.
Definition _ilen : ident := 149%positive.
Definition _ilen : ident := 150%positive.
Definition _in : ident := 48%positive.
Definition _info : ident := 138%positive.
Definition _input : ident := 148%positive.
Definition _info : ident := 140%positive.
Definition _input : ident := 149%positive.
Definition _interval : ident := 178%positive.
Definition _j : ident := 106%positive.
Definition _key : ident := 105%positive.
Definition _key_len : ident := 117%positive.
Definition _keylen : ident := 145%positive.
Definition _keylen : ident := 146%positive.
Definition _l : ident := 62%positive.
Definition _left : ident := 182%positive.
Definition _len : ident := 67%positive.
Definition _ll : ident := 77%positive.
Definition _m : ident := 116%positive.
Definition _m__1 : ident := 119%positive.
Definition _main : ident := 100%positive.
Definition _malloc : ident := 141%positive.
Definition _malloc : ident := 132%positive.
Definition _mbedtls_hmac_drbg_context : ident := 125%positive.
Definition _mbedtls_hmac_drbg_free : ident := 187%positive.
Definition _mbedtls_hmac_drbg_init : ident := 158%positive.
Expand All @@ -157,32 +157,32 @@ Definition _mbedtls_hmac_drbg_set_reseed_interval : ident := 179%positive.
Definition _mbedtls_hmac_drbg_update : ident := 166%positive.
Definition _mbedtls_md_context_t : ident := 121%positive.
Definition _mbedtls_md_free : ident := 154%positive.
Definition _mbedtls_md_get_size : ident := 137%positive.
Definition _mbedtls_md_hmac_finish : ident := 152%positive.
Definition _mbedtls_md_hmac_reset : ident := 147%positive.
Definition _mbedtls_md_hmac_starts : ident := 146%positive.
Definition _mbedtls_md_hmac_update : ident := 150%positive.
Definition _mbedtls_md_info_from_string : ident := 134%positive.
Definition _mbedtls_md_info_from_type : ident := 136%positive.
Definition _mbedtls_md_get_size : ident := 139%positive.
Definition _mbedtls_md_hmac_finish : ident := 153%positive.
Definition _mbedtls_md_hmac_reset : ident := 148%positive.
Definition _mbedtls_md_hmac_starts : ident := 147%positive.
Definition _mbedtls_md_hmac_update : ident := 151%positive.
Definition _mbedtls_md_info_from_string : ident := 136%positive.
Definition _mbedtls_md_info_from_type : ident := 138%positive.
Definition _mbedtls_md_info_t : ident := 123%positive.
Definition _mbedtls_md_setup : ident := 144%positive.
Definition _mbedtls_md_setup : ident := 145%positive.
Definition _mbedtls_zeroize : ident := 157%positive.
Definition _md : ident := 76%positive.
Definition _md_ctx : ident := 102%positive.
Definition _md_info : ident := 122%positive.
Definition _md_len : ident := 161%positive.
Definition _md_name : ident := 133%positive.
Definition _md_name : ident := 135%positive.
Definition _md_size : ident := 173%positive.
Definition _md_type : ident := 135%positive.
Definition _md_type : ident := 137%positive.
Definition _memcpy : ident := 44%positive.
Definition _memset : ident := 45%positive.
Definition _mocked_sha256_info : ident := 132%positive.
Definition _mocked_sha256_info : ident := 134%positive.
Definition _n : ident := 73%positive.
Definition _num : ident := 6%positive.
Definition _o_ctx : ident := 104%positive.
Definition _out : ident := 183%positive.
Definition _out_len : ident := 181%positive.
Definition _output : ident := 151%positive.
Definition _output : ident := 152%positive.
Definition _p : ident := 72%positive.
Definition _p_rng : ident := 180%positive.
Definition _pad : ident := 108%positive.
Expand All @@ -191,7 +191,7 @@ Definition _reseed_counter : ident := 127%positive.
Definition _reseed_interval : ident := 130%positive.
Definition _reset : ident := 107%positive.
Definition _resistance : ident := 175%positive.
Definition _ret : ident := 139%positive.
Definition _ret : ident := 141%positive.
Definition _rounds : ident := 162%positive.
Definition _s0 : ident := 56%positive.
Definition _s1 : ident := 57%positive.
Expand All @@ -200,9 +200,9 @@ Definition _seedlen : ident := 170%positive.
Definition _sep : ident := 163%positive.
Definition _sep_value : ident := 165%positive.
Definition _sha256_block_data_order : ident := 65%positive.
Definition _sha_ctx : ident := 143%positive.
Definition _sha_ctx : ident := 144%positive.
Definition _t : ident := 60%positive.
Definition _test_md_get_size : ident := 140%positive.
Definition _test_md_get_size : ident := 142%positive.
Definition _use_len : ident := 184%positive.
Definition _v : ident := 156%positive.
Definition _xn : ident := 78%positive.
Expand All @@ -221,7 +221,7 @@ Definition f_HMAC_Init := {|
fn_vars := ((_pad, (tarray tuchar 64)) :: (_ctx_key, (tarray tuchar 64)) ::
nil);
fn_temps := ((_i, tint) :: (_j, tint) :: (_reset, tint) ::
(_aux, tuchar) :: (_t'2, tuchar) :: (_t'1, tuchar) :: nil);
(_aux, tuchar) :: nil);
fn_body :=
(Ssequence
(Sset _reset (Econst_int (Int.repr 0) tint))
Expand Down Expand Up @@ -313,12 +313,11 @@ Definition f_HMAC_Init := {|
Sskip
Sbreak)
(Ssequence
(Ssequence
(Sset _t'2
(Sset _aux
(Ecast
(Ederef
(Ebinop Oadd (Evar _ctx_key (tarray tuchar 64))
(Etempvar _i tint) (tptr tuchar)) tuchar))
(Sset _aux (Ecast (Etempvar _t'2 tuchar) tuchar)))
(Etempvar _i tint) (tptr tuchar)) tuchar) tuchar))
(Ssequence
(Sset _aux
(Ecast
Expand Down Expand Up @@ -369,12 +368,12 @@ Definition f_HMAC_Init := {|
Sskip
Sbreak)
(Ssequence
(Ssequence
(Sset _t'1
(Sset _aux
(Ecast
(Ederef
(Ebinop Oadd (Evar _ctx_key (tarray tuchar 64))
(Etempvar _i tint) (tptr tuchar)) tuchar))
(Sset _aux (Ecast (Etempvar _t'1 tuchar) tuchar)))
(Etempvar _i tint) (tptr tuchar)) tuchar)
tuchar))
(Sassign
(Ederef
(Ebinop Oadd (Evar _pad (tarray tuchar 64))
Expand Down Expand Up @@ -737,16 +736,16 @@ Definition f_mbedtls_md_setup := {|
(_hmac, tint) :: nil);
fn_vars := nil;
fn_temps := ((_sha_ctx, (tptr (Tstruct _hmac_ctx_st noattr))) ::
(_t'1, tint) :: nil);
(_t'1, (tptr tvoid)) :: nil);
fn_body :=
(Ssequence
(Ssequence
(Scall (Some _t'1)
(Evar _malloc (Tfunction nil tint
{|cc_vararg:=None; cc_unproto:=true; cc_structret:=false|}))
(Evar _malloc (Tfunction (tuint :: nil) (tptr tvoid) cc_default))
((Esizeof (Tstruct _hmac_ctx_st noattr) tuint) :: nil))
(Sset _sha_ctx
(Ecast (Etempvar _t'1 tint) (tptr (Tstruct _hmac_ctx_st noattr)))))
(Ecast (Etempvar _t'1 (tptr tvoid))
(tptr (Tstruct _hmac_ctx_st noattr)))))
(Ssequence
(Sifthenelse (Ebinop Oeq
(Etempvar _sha_ctx (tptr (Tstruct _hmac_ctx_st noattr)))
Expand Down Expand Up @@ -877,9 +876,7 @@ Definition f_mbedtls_md_free := {|
(Efield
(Ederef (Etempvar _ctx (tptr (Tstruct _mbedtls_md_context_t noattr)))
(Tstruct _mbedtls_md_context_t noattr)) _hmac_ctx (tptr tvoid)))
(Scall None
(Evar _free (Tfunction nil tint
{|cc_vararg:=None; cc_unproto:=true; cc_structret:=false|}))
(Scall None (Evar _free (Tfunction ((tptr tvoid) :: nil) tvoid cc_default))
((Etempvar _hmac_ctx (tptr (Tstruct _hmac_ctx_st noattr))) :: nil)))
|}.

Expand Down Expand Up @@ -2142,22 +2139,18 @@ Definition global_definitions : list (ident * globdef fundef type) :=
(_HMAC_cleanup, Gfun(Internal f_HMAC_cleanup)) :: (_m, Gvar v_m) ::
(_HMAC, Gfun(Internal f_HMAC)) :: (_m__1, Gvar v_m__1) ::
(_HMAC2, Gfun(Internal f_HMAC2)) ::
(_malloc, Gfun(External EF_malloc (tuint :: nil) (tptr tvoid) cc_default)) ::
(_free, Gfun(External EF_free ((tptr tvoid) :: nil) tvoid cc_default)) ::
(_mocked_sha256_info, Gvar v_mocked_sha256_info) ::
(_mbedtls_md_info_from_string, Gfun(Internal f_mbedtls_md_info_from_string)) ::
(_mbedtls_md_info_from_type, Gfun(Internal f_mbedtls_md_info_from_type)) ::
(_mbedtls_md_get_size, Gfun(Internal f_mbedtls_md_get_size)) ::
(_test_md_get_size, Gfun(Internal f_test_md_get_size)) ::
(_malloc,
Gfun(External EF_malloc nil tint
{|cc_vararg:=None; cc_unproto:=true; cc_structret:=false|})) ::
(_mbedtls_md_setup, Gfun(Internal f_mbedtls_md_setup)) ::
(_mbedtls_md_hmac_starts, Gfun(Internal f_mbedtls_md_hmac_starts)) ::
(_mbedtls_md_hmac_reset, Gfun(Internal f_mbedtls_md_hmac_reset)) ::
(_mbedtls_md_hmac_update, Gfun(Internal f_mbedtls_md_hmac_update)) ::
(_mbedtls_md_hmac_finish, Gfun(Internal f_mbedtls_md_hmac_finish)) ::
(_free,
Gfun(External EF_free nil tint
{|cc_vararg:=None; cc_unproto:=true; cc_structret:=false|})) ::
(_mbedtls_md_free, Gfun(Internal f_mbedtls_md_free)) ::
(_get_entropy,
Gfun(External (EF_external "get_entropy"
Expand Down Expand Up @@ -2185,31 +2178,30 @@ Definition public_idents : list ident :=
_mbedtls_hmac_drbg_set_prediction_resistance :: _mbedtls_hmac_drbg_seed ::
_mbedtls_hmac_drbg_reseed :: _mbedtls_hmac_drbg_seed_buf ::
_mbedtls_hmac_drbg_update :: _mbedtls_hmac_drbg_init :: _get_entropy ::
_mbedtls_md_free :: _free :: _mbedtls_md_hmac_finish ::
_mbedtls_md_hmac_update :: _mbedtls_md_hmac_reset ::
_mbedtls_md_hmac_starts :: _mbedtls_md_setup :: _malloc ::
_mbedtls_md_free :: _mbedtls_md_hmac_finish :: _mbedtls_md_hmac_update ::
_mbedtls_md_hmac_reset :: _mbedtls_md_hmac_starts :: _mbedtls_md_setup ::
_test_md_get_size :: _mbedtls_md_get_size :: _mbedtls_md_info_from_type ::
_mbedtls_md_info_from_string :: _HMAC2 :: _HMAC :: _HMAC_cleanup ::
_HMAC_Final :: _HMAC_Update :: _HMAC_Init :: _SHA256_Final ::
_SHA256_Update :: _SHA256_Init :: _memset :: _memcpy :: ___builtin_debug ::
___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_expect :: ___builtin_unreachable :: ___builtin_va_end ::
___builtin_va_copy :: ___builtin_va_arg :: ___builtin_va_start ::
___builtin_membar :: ___builtin_annot_intval :: ___builtin_annot ::
___builtin_sel :: ___builtin_memcpy_aligned :: ___builtin_sqrt ::
___builtin_fsqrt :: ___builtin_fabsf :: ___builtin_fabs ::
___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: ___builtin_clzll ::
___builtin_clzl :: ___builtin_clz :: ___builtin_bswap16 ::
___builtin_bswap32 :: ___builtin_bswap :: ___builtin_bswap64 ::
___builtin_ais_annot :: ___compcert_i64_umulh :: ___compcert_i64_smulh ::
___compcert_i64_sar :: ___compcert_i64_shr :: ___compcert_i64_shl ::
___compcert_i64_umod :: ___compcert_i64_smod :: ___compcert_i64_udiv ::
___compcert_i64_sdiv :: ___compcert_i64_utof :: ___compcert_i64_stof ::
___compcert_i64_utod :: ___compcert_i64_stod :: ___compcert_i64_dtou ::
___compcert_i64_dtos :: ___compcert_va_composite ::
_mbedtls_md_info_from_string :: _free :: _malloc :: _HMAC2 :: _HMAC ::
_HMAC_cleanup :: _HMAC_Final :: _HMAC_Update :: _HMAC_Init ::
_SHA256_Final :: _SHA256_Update :: _SHA256_Init :: _memset :: _memcpy ::
___builtin_debug :: ___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_expect :: ___builtin_unreachable ::
___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg ::
___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval ::
___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned ::
___builtin_sqrt :: ___builtin_fsqrt :: ___builtin_fabsf ::
___builtin_fabs :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz ::
___builtin_clzll :: ___builtin_clzl :: ___builtin_clz ::
___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap ::
___builtin_bswap64 :: ___builtin_ais_annot :: ___compcert_i64_umulh ::
___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr ::
___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod ::
___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof ::
___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod ::
___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite ::
___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 ::
nil).

Expand Down
Loading
Loading