From f7daa4f91f70a0c8c34421e3a3d3d6af6ee3a47b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 11 Jan 2022 10:05:18 +0100
Subject: [PATCH] [wp/doc] Document Mod-Mask
---
src/plugins/wp/Changelog | 1 +
src/plugins/wp/doc/manual/wp_plugin.tex | 21 ++++++++++++++++++++-
2 files changed, 21 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 0da478f24ee..c43afbaba78 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,7 @@
Plugin WP <next-release>
########################
+- TIP [2022-01-10] New tactic Mod-Mask: rewrite bitmask into/from modulo
- TIP [2022-01-05] New tactic Clear: remove hypothesis
-* WP [2022-01-05] Fix loop invariant order
- WP [2022-01-05] Weaken check loop invariant
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index c79c2da2730..5f9ccb2b571 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -497,10 +497,29 @@ $G(n) \equiv P(n)\Longrightarrow\,Q(n)$:
\Delta,\; \forall i,\, n < i \leq b \Longrightarrow G(i) \; & \models G(n)
\end{array}} \]
+\paragraph{Mod-Mask} Rewrite bitmask into/from modulo \\
+This tactic is used to rewrite a bitmask into a modulo (or a modulo into a
+bitmask) when possible. The user selects an expression $e$ of the form
+$b \% m$ (resp. $b \& m$ - $\texttt{land b m}$) than can be rewritten into
+$b \& (m+1)$ (resp. $b \% (m - 1)$), if $0 \leq b$ and $m$ is a positive power
+of 2 (resp. $m + 1$ is a positive power of 2). When selecting an expression
+$x \& y$, both directions $x \% (y - 1)$ and $y \% (x - 1)$ can be considered.
+
+Since establishing that $m$ is a positive power of 2 can be hard, the tactic has
+several behaviors. If \textsf{Qed} can prove immediately that an operand $m$ (or
+$m+1$ for bitmaks) is a positive power of 2, the tactic only generates the guard
+$0 \leq b$ and the rewritten goal. If it is not the case, the tactic appears
+with the name ``Mod-Mask (hard)'' in the GUI. In this situation, the guard
+consists of two conditions: $0 \leq b$ and $m$ (or $m+1$) is a positive power of
+2. This guard involves an existential quantification, so it can be hard to
+prove. When the selected term is a bitmask, the tactic cannot decide itself the
+direction of the modulo, thus a checkbox is added in the configuration of the
+tactic to select the direction of rewriting.
+
\paragraph{Overflow} Integer Conversions \\
This tactic split machine integer conversions into three cases: value in integer
range, lower than range and upper than range. The tactic applies on expression
-with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer
+with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a machine-integer
name, \emph{eg.} \texttt{to\_uint32}.
\[\TACTIC{\Delta\models G}{%
--
GitLab