Commit 8eb639e0 authored by Michael Sammler's avatar Michael Sammler Committed by Paul
Browse files

comment out bits.c

parent 4d4e6c46
#include "bits.h"
// #define BIT(i) (1UL << (i))
[[rc::tactics("all: have ? := Z_shiftl_1_range i 64; try solve_goal.")]]
[[rc::lemmas("bf_mask_bit")]]
u64 BIT(int i)
{
return (1UL << (i));
}
/* [[rc::tactics("all: have ? := Z_shiftl_1_range i 64; try solve_goal.")]] */
/* [[rc::lemmas("bf_mask_bit")]] */
/* u64 BIT(int i) */
/* { */
/* return (1UL << (i)); */
/* } */
/*
* Create a contiguous bitmask starting at bit position @l and ending at
......@@ -15,19 +15,19 @@ u64 BIT(int i)
*/
// #define GENMASK(h, l) \
(((~0UL) - (1UL << (l)) + 1) & (~0UL >> (BITS_PER_LONG - 1 - (h))))
[[rc::tactics("all: have [??] : 1 ≤ 1 ≪ l ≤ 2^64 - 1 by apply Z_shiftl_1_range; solve_goal.")]]
[[rc::tactics("all: try have -> : max_int u64 = 2^64 - 1 by solve_goal.")]]
[[rc::tactics("all: try have -> : ly_size i64 * 8 = bits_per_int u64 by solve_goal.")]]
[[rc::tactics("all: try have -> : bits_per_int u64 = 64 by solve_goal.")]]
[[rc::tactics("all: try have -> : Z_lunot 64 0 = 2^64 - 1 by solve_goal.")]]
[[rc::tactics("all: try solve_goal.")]]
[[rc::lemmas("bf_mask_gen")]]
u64 GENMASK(int h, int l)
{
return (((~0UL) - (1UL << (l)) + 1) & (~0UL >> (BITS_PER_LONG - 1 - (h))));
}
/* [[rc::tactics("all: have [??] : 1 ≤ 1 ≪ l ≤ 2^64 - 1 by apply Z_shiftl_1_range; solve_goal.")]] */
/* [[rc::tactics("all: try have -> : max_int u64 = 2^64 - 1 by solve_goal.")]] */
/* [[rc::tactics("all: try have -> : ly_size i64 * 8 = bits_per_int u64 by solve_goal.")]] */
/* [[rc::tactics("all: try have -> : bits_per_int u64 = 64 by solve_goal.")]] */
/* [[rc::tactics("all: try have -> : Z_lunot 64 0 = 2^64 - 1 by solve_goal.")]] */
/* [[rc::tactics("all: try solve_goal.")]] */
/* [[rc::lemmas("bf_mask_gen")]] */
/* u64 GENMASK(int h, int l) */
/* { */
/* return (((~0UL) - (1UL << (l)) + 1) & (~0UL >> (BITS_PER_LONG - 1 - (h)))); */
/* } */
#define __bf_shf(x) (__builtin_ffsll(x) - 1)
/* #define __bf_shf(x) (__builtin_ffsll(x) - 1) */
/**
......@@ -45,14 +45,14 @@ u64 GENMASK(int h, int l)
(typeof(_mask))(((_reg) & (_mask)) >> __bf_shf(_mask)); \
})
*/
[[rc::tactics("all: unfold normalize_bitfield_eq in *; subst.")]]
[[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask.")]]
[[rc::tactics("all: try solve_goal.")]]
[[rc::lemmas("bf_mask_cons_singleton_nonempty", "bf_shr_singleton")]]
u64 FIELD_GET(u64 _mask, u64 _reg)
{
return (((_reg) & (_mask)) >> __bf_shf(_mask));
}
/* [[rc::tactics("all: unfold normalize_bitfield_eq in *; subst.")]] */
/* [[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask.")]] */
/* [[rc::tactics("all: try solve_goal.")]] */
/* [[rc::lemmas("bf_mask_cons_singleton_nonempty", "bf_shr_singleton")]] */
/* u64 FIELD_GET(u64 _mask, u64 _reg) */
/* { */
/* return (((_reg) & (_mask)) >> __bf_shf(_mask)); */
/* } */
/**
* FIELD_PREP() - prepare a bitfield element
......@@ -69,12 +69,12 @@ u64 FIELD_GET(u64 _mask, u64 _reg)
((typeof(_mask))(_val) << __bf_shf(_mask)) & (_mask); \
})
*/
[[rc::tactics("all: have [??] : v ≤ v ≪ a ≤ 2^64 - 1 by apply (Z_shl_bound k _ _ _); solve_goal.")]]
[[rc::tactics("all: try have -> : max_int u64 = 2^64 - 1 by solve_goal.")]]
[[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask ?bf_slice_shl.")]]
[[rc::tactics("all: try solve_goal.")]]
[[rc::lemmas("bf_mask_cons_singleton_nonempty")]]
u64 FIELD_PREP(u64 _mask, u64 _val)
{
return ((_val) << __bf_shf(_mask)) & (_mask);
}
/* [[rc::tactics("all: have [??] : v ≤ v ≪ a ≤ 2^64 - 1 by apply (Z_shl_bound k _ _ _); solve_goal.")]] */
/* [[rc::tactics("all: try have -> : max_int u64 = 2^64 - 1 by solve_goal.")]] */
/* [[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask ?bf_slice_shl.")]] */
/* [[rc::tactics("all: try solve_goal.")]] */
/* [[rc::lemmas("bf_mask_cons_singleton_nonempty")]] */
/* u64 FIELD_PREP(u64 _mask, u64 _val) */
/* { */
/* return ((_val) << __bf_shf(_mask)) & (_mask); */
/* } */
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment