Skip to content

Commit 71a19ac

Browse files
ole-thoebole-thoeb
committed
propagate const information and cleanup axiom generation
1 parent bb3fe37 commit 71a19ac

File tree

4 files changed

+375
-160
lines changed

4 files changed

+375
-160
lines changed

‎src/ast/shared.rs

+44
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
use ref_cast::RefCast;
2+
use std::cmp::Ordering;
3+
use std::hash::{Hash, Hasher};
14
use std::{
25
fmt,
36
ops::{Deref, DerefMut},
@@ -72,3 +75,44 @@ impl<T: ?Sized + fmt::Debug> fmt::Debug for Shared<T> {
7275
fmt::Debug::fmt(&**self, f)
7376
}
7477
}
78+
79+
/// [Shared] wrapper that provides pointer based [Eq] and [Hash] implementations.
80+
#[repr(transparent)]
81+
#[derive(RefCast)]
82+
pub struct PointerHashShared<T>(Shared<T>);
83+
84+
impl<T> PointerHashShared<T> {
85+
pub fn new(shared: Shared<T>) -> Self {
86+
Self(shared)
87+
}
88+
89+
pub fn into_shared(self) -> Shared<T> {
90+
self.0
91+
}
92+
}
93+
94+
impl<T> PartialEq for PointerHashShared<T> {
95+
fn eq(&self, other: &Self) -> bool {
96+
Shared::as_ptr(&self.0) == Shared::as_ptr(&other.0)
97+
}
98+
}
99+
100+
impl<T> Eq for PointerHashShared<T> {}
101+
102+
impl<T> Ord for PointerHashShared<T> {
103+
fn cmp(&self, other: &Self) -> Ordering {
104+
Shared::as_ptr(&self.0).cmp(&Shared::as_ptr(&other.0))
105+
}
106+
}
107+
108+
impl<T> PartialOrd for PointerHashShared<T> {
109+
fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
110+
Some(Shared::as_ptr(&self.0).cmp(&Shared::as_ptr(&other.0)))
111+
}
112+
}
113+
114+
impl<T> Hash for PointerHashShared<T> {
115+
fn hash<H: Hasher>(&self, state: &mut H) {
116+
Shared::as_ptr(&self.0).hash(state)
117+
}
118+
}

‎src/smt/limited.rs

+235-9
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,19 @@
88
//! For this to work the SMT solver is not allowed to synthesis fuel values itself.
99
//! Therefore, MBQI must be disabled.
1010
11-
use crate::ast::{Expr, FuncDecl};
11+
use crate::ast::visit::{walk_expr, VisitorMut};
12+
use crate::ast::{
13+
Expr, ExprBuilder, ExprData, ExprKind, FuncDecl, Ident, PointerHashShared, SpanVariant,
14+
};
1215
use crate::smt::translate_exprs::{FuelContext, TranslateExprs};
1316
use crate::smt::{ty_to_sort, SmtCtx};
17+
use crate::tyctx::TyCtx;
18+
use indexmap::IndexSet;
19+
use itertools::Itertools;
20+
use std::convert::Infallible;
1421
use z3::ast::{Ast, Bool};
1522
use z3::{Pattern, Sort};
16-
use z3rro::SmtEq;
23+
use z3rro::{SmtEq, SmtInvariant};
1724

1825
/// Builds the domain (parameter list) for `func`. If the limited function transformation is
1926
/// applicable a fuel parameter is implicitly added as the first parameter.
@@ -64,16 +71,35 @@ fn translate_defining_axiom<'smt, 'ctx>(
6471
axiom
6572
}
6673

74+
/// Creates a call to the function.
75+
fn build_call(tcx: &TyCtx, func: &FuncDecl) -> Expr {
76+
let span = func.span.variant(SpanVariant::VC);
77+
let builder = ExprBuilder::new(span);
78+
builder.call(
79+
func.name,
80+
func.inputs
81+
.node
82+
.iter()
83+
.map(|param| builder.var(param.name, tcx)),
84+
tcx,
85+
)
86+
}
87+
6788
/// Creates the fuel synonym axiom that states that the result of the function is independent
6889
/// of the fuel parameter. It has the form:
6990
/// ```txt
7091
/// forall fuel: Fuel, <args...> . func_name(Succ(fuel), <args...>) = func_name(fuel, <args...>)
7192
/// ```
7293
pub fn fuel_synonym_axiom<'smt, 'ctx>(
7394
translate: &mut TranslateExprs<'smt, 'ctx>,
74-
app: &Expr,
75-
) -> Bool<'ctx> {
76-
translate_defining_axiom(translate, app, app)
95+
func: &FuncDecl,
96+
) -> Option<Bool<'ctx>> {
97+
if translate.ctx.is_limited_function_decl(func) {
98+
let app = build_call(translate.ctx.tcx, func);
99+
Some(translate_defining_axiom(translate, &app, &app))
100+
} else {
101+
None
102+
}
77103
}
78104

79105
/// Creates the default defining axiom for a function. It has the form:
@@ -83,8 +109,208 @@ pub fn fuel_synonym_axiom<'smt, 'ctx>(
83109
/// where only `fuel` is used as the fuel parameter in `<body>`.
84110
pub fn defining_axiom<'smt, 'ctx>(
85111
translate: &mut TranslateExprs<'smt, 'ctx>,
86-
app: &Expr,
87-
body: &Expr,
88-
) -> Bool<'ctx> {
89-
translate_defining_axiom(translate, app, body)
112+
func: &FuncDecl,
113+
) -> Option<Bool<'ctx>> {
114+
func.body.borrow().as_ref().map(|body| {
115+
let app = build_call(translate.ctx.tcx, func);
116+
translate_defining_axiom(translate, &app, body)
117+
})
118+
}
119+
120+
/// Creates the computation axiom that allows for constant arguments instantiation without
121+
/// consuming fuel. It is very similar to the [defining_axiom]. The only differences are that
122+
/// - all arguments must be known constant values (marked with [super::Lit]),
123+
/// - the fuel value can be zero,
124+
/// - the fuel value is not decreased in the body
125+
/// - and the constant information is also propagated to the result.
126+
///
127+
/// It has the form:
128+
/// ```txt
129+
/// forall fuel: Fuel, <args...> . func_name(fuel, Lit(<args...>)) = <body>
130+
/// ```
131+
pub fn computation_axiom<'smt, 'ctx>(
132+
translate: &mut TranslateExprs<'smt, 'ctx>,
133+
func: &FuncDecl,
134+
) -> Option<Bool<'ctx>> {
135+
if !translate.ctx.lit_wrap {
136+
return None;
137+
}
138+
if !translate.ctx.is_limited_function_decl(func) {
139+
return None;
140+
}
141+
assert!(func.body.borrow().is_some());
142+
143+
translate.push();
144+
translate.set_fuel_context(FuelContext::Body);
145+
{
146+
let constant_vars = func
147+
.inputs
148+
.node
149+
.iter()
150+
.map(|param| param.name)
151+
.collect_vec();
152+
153+
translate.set_constant_exprs(
154+
constant_vars.as_slice(),
155+
func.body.borrow_mut().as_mut().unwrap(),
156+
);
157+
}
158+
159+
let app = build_call(translate.ctx.tcx, func);
160+
161+
let body_ref = func.body.borrow();
162+
let body = body_ref.as_ref().unwrap();
163+
164+
let app_z3 = translate.t_symbolic(&app).into_dynamic(translate.ctx);
165+
let body_z3 = translate.t_symbolic(body).into_dynamic(translate.ctx);
166+
167+
let axiom = translate.local_scope().forall(
168+
&[&Pattern::new(
169+
translate.ctx.ctx,
170+
&[&app_z3 as &dyn Ast<'ctx>],
171+
)],
172+
&app_z3.smt_eq(&body_z3),
173+
);
174+
translate.clear_constant_exprs();
175+
translate.set_fuel_context(FuelContext::Call);
176+
translate.pop();
177+
178+
Some(axiom)
179+
}
180+
181+
/// Invariant for the functions return value.
182+
pub fn return_value_invariant<'smt, 'ctx>(
183+
translate: &mut TranslateExprs<'smt, 'ctx>,
184+
func: &FuncDecl,
185+
) -> Option<Bool<'ctx>> {
186+
translate.push();
187+
translate.set_fuel_context(FuelContext::Body);
188+
189+
let app = build_call(translate.ctx.tcx, func);
190+
let app_z3 = translate.t_symbolic(&app);
191+
let axiom = app_z3
192+
.smt_invariant()
193+
.map(|invariant| translate.local_scope().forall(&[], &invariant));
194+
195+
translate.set_fuel_context(FuelContext::Call);
196+
translate.pop();
197+
198+
axiom
199+
}
200+
201+
type HashExpr = PointerHashShared<ExprData>;
202+
203+
#[derive(Default)]
204+
pub struct ConstantExprs(IndexSet<HashExpr>);
205+
206+
impl ConstantExprs {
207+
pub fn is_constant(&self, expr: &Expr) -> bool {
208+
self.0.contains(&HashExpr::new(expr.clone()))
209+
}
210+
211+
fn insert(&mut self, expr: &Expr) -> bool {
212+
self.0.insert(HashExpr::new(expr.clone()))
213+
}
214+
215+
fn remove(&mut self, expr: &Expr) -> bool {
216+
self.0.remove(&HashExpr::new(expr.clone()))
217+
}
218+
}
219+
220+
/// Collects the maximal constant subexpressions of an expression.
221+
/// An expression is to be considered constant if it is a literal, a known constant variable, or
222+
/// all its children are constant. Maximality is in relation to the expression size. Meaning if an
223+
/// expression is reported as constant, none of its children are reported
224+
///
225+
/// # Example
226+
/// If `a` is a known constant variable then for the expression `a + 4 * b` this analysis will
227+
/// return only `a + 4`.
228+
#[derive(Default)]
229+
pub struct ConstantExprCollector {
230+
constant_exprs: ConstantExprs,
231+
constant_vars: IndexSet<Ident>,
232+
}
233+
234+
impl ConstantExprCollector {
235+
pub fn new(constant_vars: &[Ident]) -> Self {
236+
Self {
237+
constant_exprs: ConstantExprs::default(),
238+
constant_vars: constant_vars.iter().cloned().collect(),
239+
}
240+
}
241+
242+
fn is_constant(&self, expr: &Expr) -> bool {
243+
self.constant_exprs.is_constant(expr)
244+
}
245+
246+
pub fn into_constant_exprs(self) -> ConstantExprs {
247+
self.constant_exprs
248+
}
249+
}
250+
251+
impl VisitorMut for ConstantExprCollector {
252+
type Err = Infallible;
253+
254+
fn visit_expr(&mut self, expr: &mut Expr) -> Result<(), Self::Err> {
255+
walk_expr(self, expr)?; // visit children first
256+
257+
match &expr.kind {
258+
ExprKind::Var(ident) => {
259+
if self.constant_vars.contains(ident) {
260+
self.constant_exprs.insert(expr);
261+
}
262+
}
263+
ExprKind::Call(_, args) => {
264+
if args.iter().all(|arg| self.is_constant(arg)) {
265+
self.constant_exprs.insert(expr);
266+
for arg in args {
267+
self.constant_exprs.remove(arg);
268+
}
269+
}
270+
}
271+
ExprKind::Ite(cond, then, other) => {
272+
// TODO: maybe this should never be consider const?
273+
// If-then-else is used as a stopper for constant values and therefore itself
274+
// never considered constant. The paper mentions that this works well
275+
// in practise.
276+
if self.is_constant(cond) && self.is_constant(then) && self.is_constant(other) {
277+
self.constant_exprs.insert(expr);
278+
self.constant_exprs.remove(cond);
279+
self.constant_exprs.remove(then);
280+
self.constant_exprs.remove(other);
281+
}
282+
}
283+
ExprKind::Binary(_, lhs, rhs) => {
284+
if self.is_constant(lhs) && self.is_constant(rhs) {
285+
self.constant_exprs.insert(expr);
286+
self.constant_exprs.remove(lhs);
287+
self.constant_exprs.remove(rhs);
288+
}
289+
}
290+
ExprKind::Unary(_, inner_expr) => {
291+
if self.is_constant(inner_expr) {
292+
self.constant_exprs.insert(expr);
293+
self.constant_exprs.remove(inner_expr);
294+
}
295+
}
296+
ExprKind::Cast(inner_expr) => {
297+
if self.is_constant(inner_expr) {
298+
self.constant_exprs.insert(expr);
299+
self.constant_exprs.remove(inner_expr);
300+
}
301+
}
302+
ExprKind::Quant(_, _, _, _) => {}
303+
ExprKind::Subst(_, _, _) => {
304+
panic!(
305+
"cannot determine constant subexpressions in expressions with substitutions: {}",
306+
expr
307+
);
308+
}
309+
ExprKind::Lit(_) => {
310+
self.constant_exprs.insert(expr);
311+
}
312+
}
313+
314+
Ok(())
315+
}
90316
}

0 commit comments

Comments
 (0)