Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
pub
framac
Commits
9176cd9e
Commit
9176cd9e
authored
Nov 04, 2020
by
Allan Blanchard
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
[wp/doc] Document tactic: BitTest Range
parent
bc4a7baa
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
24 additions
and
5 deletions
+24
5
src/plugins/wp/doc/manual/wp_plugin.tex
src/plugins/wp/doc/manual/wp_plugin.tex
+24
5
No files found.
src/plugins/wp/doc/manual/wp_plugin.tex
View file @
9176cd9e
...
...
@@ 405,6 +405,30 @@ to apply the theorems. Such a strategy is \emph{not} complete in general.
Typically,
$
\mathtt
{
land
}
(
x,y
)
<
38
$
is true whenever both
$
x
$
and
$
y
$
are in range
$
0
\ldots
31
$
, but this is also true
in other cases.
\paragraph
{
BitTest Range
}
Tighten Bounds with respect to bits
\\
The
\lstinline
{
bit
_
test(a,b)
}
function is predefined in
\textsf
{
WP
}
and is equivalent
to the
\textsf
{
ACSL
}
expression
\lstinline
{
(a
&
(1 << k)) != 0
}
. The
\textsf
{
Qed
}
engine has many simplification rules that applies to
such patterns.
The user selects an expression
$
\mathtt
{
bit
\_
test
}
(
n,k
)
$
with
$
k
$
a
\emph
{
constant
}
integer value greater or equal to 0 and lower than
128. The tactic uses this test to thighten the bounds of
$
n
$
.
$$
\TACTIC
{
\Delta\models\,
G
}{
%
\begin
{
array
}
[
t
]
{
ll
}
\Delta
,T
&
\models
G
\\
\Delta
,F
&
\models
G
\end
{
array
}}
$$
with
$$
\begin
{
array
}
[
t
]
{
rlcll
}
T
\equiv
&
\mathtt
{
bit
\_
test
}
(
n,k
)
&
\wedge
&
(
0
\leq
n
&
\Rightarrow
2
^{
k
}
\leq
n
)
\\
F
\equiv
&
\neg
\mathtt
{
bit
\_
test
}
(
n,k
)
&
\wedge
&
(
0
\leq
n <
2
^{
k
+
1
}
&
\Rightarrow
n <
2
^{
k
}
)
\end
{
array
}
$$
\paragraph
{
Bitwise
}
Decompose equalities over
$
N
$
bits
\\
The use selects an integer equality and a number of bits.
Providing the two members of the equality are in range
$
0
..
2
^
N

1
$
,
...
...
@@ 422,11 +446,6 @@ where $\sigma$ is the following subsitution:
\right
]
\]
The
\lstinline
{
bit
_
test(a,b)
}
function is predefined in
\textsf
{
WP
}
and is equivalent
to the
\textsf
{
ACSL
}
expression
\lstinline
{
(a
&
(1 << k)) != 0
}
. The
\textsf
{
Qed
}
engine has many simplification rules that applies to
such patterns, and the a tactic is good way to reason over bits.
\paragraph
{
Congruence
}
Simplify Divisions and Products
\\
This tactic rewrites integer comparisons involving products and divisions.
The tactic applies one of the following theorems to the current goal.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment