Skip to content

Commit

Permalink
propagate const information and cleanup axiom generation
Browse files Browse the repository at this point in the history
  • Loading branch information
@ole-thoeb
ole-thoeb committed Nov 5, 2024
1 parent bb3fe37 commit 71a19ac
Show file tree
Hide file tree
Showing 4 changed files with 375 additions and 160 deletions.
44 changes: 44 additions & 0 deletions src/ast/shared.rs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
use ref_cast::RefCast;
use std::cmp::Ordering;
use std::hash::{Hash, Hasher};
use std::{
fmt,
ops::{Deref, DerefMut},
Expand Down Expand Up @@ -72,3 +75,44 @@ impl<T: ?Sized + fmt::Debug> fmt::Debug for Shared<T> {
fmt::Debug::fmt(&**self, f)
}
}

/// [Shared] wrapper that provides pointer based [Eq] and [Hash] implementations.
#[repr(transparent)]
#[derive(RefCast)]
pub struct PointerHashShared<T>(Shared<T>);

impl<T> PointerHashShared<T> {
pub fn new(shared: Shared<T>) -> Self {
Self(shared)
}

pub fn into_shared(self) -> Shared<T> {
self.0
}
}

impl<T> PartialEq for PointerHashShared<T> {
fn eq(&self, other: &Self) -> bool {
Shared::as_ptr(&self.0) == Shared::as_ptr(&other.0)
}
}

impl<T> Eq for PointerHashShared<T> {}

impl<T> Ord for PointerHashShared<T> {
fn cmp(&self, other: &Self) -> Ordering {
Shared::as_ptr(&self.0).cmp(&Shared::as_ptr(&other.0))
}
}

impl<T> PartialOrd for PointerHashShared<T> {
fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
Some(Shared::as_ptr(&self.0).cmp(&Shared::as_ptr(&other.0)))
}
}

impl<T> Hash for PointerHashShared<T> {
fn hash<H: Hasher>(&self, state: &mut H) {
Shared::as_ptr(&self.0).hash(state)
}
}
244 changes: 235 additions & 9 deletions src/smt/limited.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,19 @@
//! For this to work the SMT solver is not allowed to synthesis fuel values itself.
//! Therefore, MBQI must be disabled.
use crate::ast::{Expr, FuncDecl};
use crate::ast::visit::{walk_expr, VisitorMut};
use crate::ast::{
Expr, ExprBuilder, ExprData, ExprKind, FuncDecl, Ident, PointerHashShared, SpanVariant,
};
use crate::smt::translate_exprs::{FuelContext, TranslateExprs};
use crate::smt::{ty_to_sort, SmtCtx};
use crate::tyctx::TyCtx;
use indexmap::IndexSet;
use itertools::Itertools;
use std::convert::Infallible;
use z3::ast::{Ast, Bool};
use z3::{Pattern, Sort};
use z3rro::SmtEq;
use z3rro::{SmtEq, SmtInvariant};

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

/// Creates a call to the function.
fn build_call(tcx: &TyCtx, func: &FuncDecl) -> Expr {
let span = func.span.variant(SpanVariant::VC);
let builder = ExprBuilder::new(span);
builder.call(
func.name,
func.inputs
.node
.iter()
.map(|param| builder.var(param.name, tcx)),
tcx,
)
}

/// Creates the fuel synonym axiom that states that the result of the function is independent
/// of the fuel parameter. It has the form:
/// ```txt
/// forall fuel: Fuel, <args...> . func_name(Succ(fuel), <args...>) = func_name(fuel, <args...>)
/// ```
pub fn fuel_synonym_axiom<'smt, 'ctx>(
translate: &mut TranslateExprs<'smt, 'ctx>,
app: &Expr,
) -> Bool<'ctx> {
translate_defining_axiom(translate, app, app)
func: &FuncDecl,
) -> Option<Bool<'ctx>> {
if translate.ctx.is_limited_function_decl(func) {
let app = build_call(translate.ctx.tcx, func);
Some(translate_defining_axiom(translate, &app, &app))
} else {
None
}
}

/// Creates the default defining axiom for a function. It has the form:
Expand All @@ -83,8 +109,208 @@ pub fn fuel_synonym_axiom<'smt, 'ctx>(
/// where only `fuel` is used as the fuel parameter in `<body>`.
pub fn defining_axiom<'smt, 'ctx>(
translate: &mut TranslateExprs<'smt, 'ctx>,
app: &Expr,
body: &Expr,
) -> Bool<'ctx> {
translate_defining_axiom(translate, app, body)
func: &FuncDecl,
) -> Option<Bool<'ctx>> {
func.body.borrow().as_ref().map(|body| {
let app = build_call(translate.ctx.tcx, func);
translate_defining_axiom(translate, &app, body)
})
}

/// Creates the computation axiom that allows for constant arguments instantiation without
/// consuming fuel. It is very similar to the [defining_axiom]. The only differences are that
/// - all arguments must be known constant values (marked with [super::Lit]),
/// - the fuel value can be zero,
/// - the fuel value is not decreased in the body
/// - and the constant information is also propagated to the result.
///
/// It has the form:
/// ```txt
/// forall fuel: Fuel, <args...> . func_name(fuel, Lit(<args...>)) = <body>
/// ```
pub fn computation_axiom<'smt, 'ctx>(
translate: &mut TranslateExprs<'smt, 'ctx>,
func: &FuncDecl,
) -> Option<Bool<'ctx>> {
if !translate.ctx.lit_wrap {
return None;
}
if !translate.ctx.is_limited_function_decl(func) {
return None;
}
assert!(func.body.borrow().is_some());

translate.push();
translate.set_fuel_context(FuelContext::Body);
{
let constant_vars = func
.inputs
.node
.iter()
.map(|param| param.name)
.collect_vec();

translate.set_constant_exprs(
constant_vars.as_slice(),
func.body.borrow_mut().as_mut().unwrap(),
);
}

let app = build_call(translate.ctx.tcx, func);

let body_ref = func.body.borrow();
let body = body_ref.as_ref().unwrap();

let app_z3 = translate.t_symbolic(&app).into_dynamic(translate.ctx);
let body_z3 = translate.t_symbolic(body).into_dynamic(translate.ctx);

let axiom = translate.local_scope().forall(
&[&Pattern::new(
translate.ctx.ctx,
&[&app_z3 as &dyn Ast<'ctx>],
)],
&app_z3.smt_eq(&body_z3),
);
translate.clear_constant_exprs();
translate.set_fuel_context(FuelContext::Call);
translate.pop();

Some(axiom)
}

/// Invariant for the functions return value.
pub fn return_value_invariant<'smt, 'ctx>(
translate: &mut TranslateExprs<'smt, 'ctx>,
func: &FuncDecl,
) -> Option<Bool<'ctx>> {
translate.push();
translate.set_fuel_context(FuelContext::Body);

let app = build_call(translate.ctx.tcx, func);
let app_z3 = translate.t_symbolic(&app);
let axiom = app_z3
.smt_invariant()
.map(|invariant| translate.local_scope().forall(&[], &invariant));

translate.set_fuel_context(FuelContext::Call);
translate.pop();

axiom
}

type HashExpr = PointerHashShared<ExprData>;

#[derive(Default)]
pub struct ConstantExprs(IndexSet<HashExpr>);

impl ConstantExprs {
pub fn is_constant(&self, expr: &Expr) -> bool {
self.0.contains(&HashExpr::new(expr.clone()))
}

fn insert(&mut self, expr: &Expr) -> bool {
self.0.insert(HashExpr::new(expr.clone()))
}

fn remove(&mut self, expr: &Expr) -> bool {
self.0.remove(&HashExpr::new(expr.clone()))
}
}

/// Collects the maximal constant subexpressions of an expression.
/// An expression is to be considered constant if it is a literal, a known constant variable, or
/// all its children are constant. Maximality is in relation to the expression size. Meaning if an
/// expression is reported as constant, none of its children are reported
///
/// # Example
/// If `a` is a known constant variable then for the expression `a + 4 * b` this analysis will
/// return only `a + 4`.
#[derive(Default)]
pub struct ConstantExprCollector {
constant_exprs: ConstantExprs,
constant_vars: IndexSet<Ident>,
}

impl ConstantExprCollector {
pub fn new(constant_vars: &[Ident]) -> Self {
Self {
constant_exprs: ConstantExprs::default(),
constant_vars: constant_vars.iter().cloned().collect(),
}
}

fn is_constant(&self, expr: &Expr) -> bool {
self.constant_exprs.is_constant(expr)
}

pub fn into_constant_exprs(self) -> ConstantExprs {
self.constant_exprs
}
}

impl VisitorMut for ConstantExprCollector {
type Err = Infallible;

fn visit_expr(&mut self, expr: &mut Expr) -> Result<(), Self::Err> {
walk_expr(self, expr)?; // visit children first

match &expr.kind {
ExprKind::Var(ident) => {
if self.constant_vars.contains(ident) {
self.constant_exprs.insert(expr);
}
}
ExprKind::Call(_, args) => {
if args.iter().all(|arg| self.is_constant(arg)) {
self.constant_exprs.insert(expr);
for arg in args {
self.constant_exprs.remove(arg);
}
}
}
ExprKind::Ite(cond, then, other) => {
// TODO: maybe this should never be consider const?
// If-then-else is used as a stopper for constant values and therefore itself
// never considered constant. The paper mentions that this works well
// in practise.
if self.is_constant(cond) && self.is_constant(then) && self.is_constant(other) {
self.constant_exprs.insert(expr);
self.constant_exprs.remove(cond);
self.constant_exprs.remove(then);
self.constant_exprs.remove(other);
}
}
ExprKind::Binary(_, lhs, rhs) => {
if self.is_constant(lhs) && self.is_constant(rhs) {
self.constant_exprs.insert(expr);
self.constant_exprs.remove(lhs);
self.constant_exprs.remove(rhs);
}
}
ExprKind::Unary(_, inner_expr) => {
if self.is_constant(inner_expr) {
self.constant_exprs.insert(expr);
self.constant_exprs.remove(inner_expr);
}
}
ExprKind::Cast(inner_expr) => {
if self.is_constant(inner_expr) {
self.constant_exprs.insert(expr);
self.constant_exprs.remove(inner_expr);
}
}
ExprKind::Quant(_, _, _, _) => {}
ExprKind::Subst(_, _, _) => {
panic!(
"cannot determine constant subexpressions in expressions with substitutions: {}",
expr
);
}
ExprKind::Lit(_) => {
self.constant_exprs.insert(expr);
}
}

Ok(())
}
}
Loading

0 comments on commit 71a19ac

Please sign in to comment.