Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improved version of the AST rule #23

Draft
wants to merge 4 commits into
base: main
Choose a base branch
from
+172 −86
Draft

Improved version of the AST rule #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
06f8bfa
ast rule improvements WIP
Philipp15b Apr 9, 2024
93f4707
add missing change
Philipp15b Apr 10, 2024
850d898
update test to use ast annotation
Philipp15b Apr 10, 2024
6cdb988
smt: add additional debugging assertions to detect type confusions
Philipp15b Apr 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions src/ast/expr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -451,6 +451,13 @@ impl ExprBuilder {
}

pub fn cast(&self, ty: TyKind, operand: Expr) -> Expr {
let cast_not_needed = operand
.ty
.as_ref()
.is_some_and(|operand_ty| operand_ty == &ty);
if cast_not_needed {
return operand;
}
Shared::new(ExprData {
kind: ExprKind::Cast(operand),
ty: Some(ty),
Expand Down
65 changes: 47 additions & 18 deletions src/proof_rules/mciver_ast.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,8 +39,8 @@ impl ASTAnnotation {
let name = Ident::with_dummy_file_span(Symbol::intern("ast"), file);

let invariant_param = intrinsic_param(file, "invariant", TyKind::Bool, false);
let variant_param = intrinsic_param(file, "variant", TyKind::SpecTy, false);
let free_var_param = intrinsic_param(file, "free_variable", TyKind::UInt, false);
let variant_param = intrinsic_param(file, "variant", TyKind::UReal, false);
let free_var_param = intrinsic_param(file, "free_variable", TyKind::UReal, false);
let prob_param = intrinsic_param(file, "prob", TyKind::UReal, false);
let decr_param = intrinsic_param(file, "decrease", TyKind::UReal, false);

Expand Down Expand Up @@ -93,26 +93,34 @@ impl Encoding for ASTAnnotation {
if let ExprKind::Var(var_ref) = &free_var.kind {
let var_decl = VarDecl {
name: *var_ref,
ty: TyKind::UInt,
ty: TyKind::UReal,
kind: VarKind::Mut,
init: None,
span: call_span,
created_from: None,
};
// Declare the free variable to be used in the omega invariant
resolve.declare(DeclKind::VarDecl(DeclRef::new(var_decl)))?;
} else {
todo!() // TODO: print an error message otherwise!
}

resolve.visit_expr(prob)?;
resolve.visit_expr(decrease)
}

// TODO: handle nondeterminism!
// - only allow demonic nondet
// - transform to angelic nondet for upper bounds reasoning

fn tycheck(
&self,
tycheck: &mut Tycheck<'_>,
call_span: Span,
args: &mut [Expr],
) -> Result<(), TycheckError> {
// TODO: does not check that the proc lower bounds!

check_annotation_call(tycheck, call_span, &self.0, args)?;
Ok(())
}
Expand Down Expand Up @@ -302,56 +310,74 @@ impl Encoding for ASTAnnotation {

let cond3_proc = generate_proc(annotation_span, cond3_proc_info, base_proc_ident, tcx);

// ?((~loop_guard) == (variant = 0))
// ?(loop_guard ==> (variant > 0))
let cond4_expr = builder.unary(
UnOpKind::Embed,
Some(TyKind::EUReal),
builder.binary(
BinOpKind::Eq,
BinOpKind::Impl,
Some(TyKind::Bool),
builder.unary(UnOpKind::Not, Some(TyKind::Bool), loop_guard.clone()),
loop_guard.clone(),
builder.binary(
BinOpKind::Eq,
BinOpKind::Gt,
Some(TyKind::Bool),
variant.clone(),
builder.cast(TyKind::EUReal, builder.uint(0)),
builder.cast(TyKind::UReal, builder.uint(0)),
),
),
);

// !G iff V = 0
// if G then V > 0
let cond4_proc_info = ProcInfo {
// create the ProcInfo according to the generate_proc function below
name: "termination_condition".to_string(),
inputs: params_from_idents(input_vars, tcx),
outputs: vec![],
spec: vec![],
spec: vec![ProcSpec::Requires(builder.unary(
UnOpKind::Embed,
Some(TyKind::EUReal),
invariant.to_owned(),
))],
body: vec![Spanned::new(
annotation_span,
StmtKind::Assert(Direction::Down, cond4_expr),
)],
direction: Direction::Down,
};
let cond4_proc = generate_proc(annotation_span, cond4_proc_info, base_proc_ident, tcx);

// Phi_{V}(V) <= V
let mut cond5_body = init_assigns.clone();
cond5_body.push(Spanned::new(
annotation_span,
StmtKind::Assume(
Direction::Up,
builder.unary(
UnOpKind::Embed,
Some(TyKind::EUReal),
builder.unary(UnOpKind::Not, Some(TyKind::Bool), invariant.to_owned()),
),
),
));
cond5_body.push(
encode_iter(
annotation_span,
inner_stmt,
// hey_const(annotation_span, &variant, tcx),
vec![],
)
.unwrap(),
);

// Phi_{V}(V) <= V
let cond5_proc_info = ProcInfo {
name: "V_wp_superinvariant".to_string(),
inputs: params_from_idents(input_init_vars.clone(), tcx),
outputs: params_from_idents(modified_vars.clone(), tcx),
spec: vec![
ProcSpec::Requires(to_init_expr(tcx, annotation_span, variant, &modified_vars)),
ProcSpec::Ensures(variant.clone()),
ProcSpec::Requires(builder.cast(
TyKind::EUReal,
to_init_expr(tcx, annotation_span, variant, &modified_vars),
)),
ProcSpec::Ensures(builder.cast(TyKind::EUReal, variant.clone())),
],
body: cond5_body,
direction: Direction::Up,
Expand All @@ -375,7 +401,10 @@ impl Encoding for ASTAnnotation {
Some(TyKind::EUReal),
loop_guard.to_owned(),
),
builder.subst(prob.clone(), [(free_var, variant.clone())]),
builder.cast(
TyKind::EUReal,
builder.subst(prob.clone(), [(free_var, variant.clone())]),
),
),
);

Expand All @@ -388,7 +417,7 @@ impl Encoding for ASTAnnotation {
variant.clone(),
builder.binary(
BinOpKind::Sub,
Some(TyKind::EUReal),
Some(TyKind::UReal),
init_variant.clone(),
builder.subst(decrease.clone(), [(free_var, init_variant)]),
),
Expand All @@ -398,7 +427,7 @@ impl Encoding for ASTAnnotation {
let mut cond6_body = init_assigns;
cond6_body.extend(loop_body.clone());

//[I] * [G] * (p o V) <= \\s. wp[P]([V < V(s) - d(V(s))])(s)
// [I] * [G] * (p o V) <= \\s. wp[P]([V <= V(s) - d(V(s))])(s)
let cond6_proc_info = ProcInfo {
name: "progress_condition".to_string(),
inputs: params_from_idents(input_init_vars, tcx),
Expand All @@ -420,7 +449,7 @@ impl Encoding for ASTAnnotation {

Ok(EncodingGenerated {
span: annotation_span,
stmts: vec![],
stmts: vec![], // TODO: the body is missing, call the police
decls: Some(vec![
cond1_proc, cond2_proc, cond3_proc, cond4_proc, cond5_proc, cond6_proc,
]),
Expand Down
17 changes: 16 additions & 1 deletion src/smt/translate_exprs.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,8 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
}

pub fn t_bool(&mut self, expr: &Expr) -> Bool<'ctx> {
assert_eq!(&expr.ty, &Some(TyKind::Bool), "expr is not of type Bool: {:?}", expr);

if is_expr_worth_caching(expr) {
if let Some(res) = self.cache.get(expr) {
return res.clone().into_bool().unwrap();
Expand Down Expand Up @@ -198,6 +200,8 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
}

pub fn t_int(&mut self, expr: &Expr) -> Int<'ctx> {
assert_eq!(&expr.ty, &Some(TyKind::Int), "expr is not of type Int: {:?}", expr);

if is_expr_worth_caching(expr) {
if let Some(res) = self.cache.get(expr) {
tracing::trace!(ref_count = Shared::ref_count(expr), "uncaching expr");
Expand Down Expand Up @@ -252,6 +256,8 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
}

pub fn t_uint(&mut self, expr: &Expr) -> UInt<'ctx> {
assert_eq!(&expr.ty, &Some(TyKind::UInt), "expr is not of type UInt: {:?}", expr);

if is_expr_worth_caching(expr) {
if let Some(res) = self.cache.get(expr) {
tracing::trace!(ref_count = Shared::ref_count(expr), "uncaching expr");
Expand Down Expand Up @@ -303,6 +309,8 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
}

pub fn t_real(&mut self, expr: &Expr) -> Real<'ctx> {
assert_eq!(&expr.ty, &Some(TyKind::Real), "expr is not of type Real: {:?}", expr);

if is_expr_worth_caching(expr) {
if let Some(res) = self.cache.get(expr) {
tracing::trace!(ref_count = Shared::ref_count(expr), "uncaching expr");
Expand Down Expand Up @@ -365,6 +373,8 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
}

pub fn t_ureal(&mut self, expr: &Expr) -> UReal<'ctx> {
assert_eq!(&expr.ty, &Some(TyKind::UReal), "expr is not of type UReal: {:?}", expr);

if is_expr_worth_caching(expr) {
if let Some(res) = self.cache.get(expr) {
tracing::trace!(ref_count = Shared::ref_count(expr), "uncaching expr");
Expand Down Expand Up @@ -427,6 +437,8 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
}

pub fn t_eureal(&mut self, expr: &Expr) -> EUReal<'ctx> {
assert_eq!(&expr.ty, &Some(TyKind::EUReal), "expr is not of type EUReal: {:?}", expr);

match &expr.kind {
ExprKind::Var(ident) => self
.get_local(*ident)
Expand Down Expand Up @@ -615,7 +627,10 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
fn t_pair(&mut self, a: &Expr, b: &Expr) -> SymbolicPair<'ctx> {
let t_a = self.t_symbolic(a);
let t_b = self.t_symbolic(b);
SymbolicPair::from_untypeds(t_a, t_b).unwrap()
SymbolicPair::from_untypeds(t_a, t_b).expect(&format!(
"type mismatch during translation: {:?} and {:?}",
a, b
))
}

pub fn get_local(&mut self, ident: Ident) -> &ScopeSymbolic<'ctx> {
Expand Down
80 changes: 14 additions & 66 deletions tests/loop-rules/ast-rule4.heyvl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,75 +1,23 @@
// RUN: @caesar @file
// Auto-generated by pgcl2heyvl from esc_spline_ast.pgcl
//
// HeyVL file to show that C is almost-surely terminating
// using AST rule by McIver et al. (2018) with
// invariant = true, variant = x, probability function = 1 / (v + 1), decrease function = 1
// for the pGCL program C:
//
// nat x;
// while (0 < x) {
// {
// x := 0;
// } [1 / (x + 1)] {
// x := x + 1;
// }
// }

// [I] <= \Phi_{[I]}([I])
proc I_wp_subinvariant(init_x: UInt) -> (x: UInt)
pre [true]
post [true]
proc ast_example4() -> ()
pre 1
post 1
{
var prob_choice: Bool
x = init_x
if 0 < x {
prob_choice = flip(1 / (x + 1))
var x: UInt
@ast(
/* invariant: */ true,
/* variant: */ x,
/* variable: */ v,
/* prob(v): */ 1/(v+1),
/* decrease(v): */ 1
)
while x != 0 {
var prob_choice: Bool = flip(1 / (x + 1))
if prob_choice {
x = 0
} else {
x = x + 1
}
assert [true]
assume 0
} else {}
}

// !G iff V = 0
proc termination_condition(x: UInt) -> ()
{
assert ?(!(0 < x) == (x == 0))
}

// \Phi_{V}(V) <= V
coproc V_wp_superinvariant(init_x: UInt) -> (x: UInt)
pre init_x
post x
{
var prob_choice: Bool
x = init_x
if 0 < x {
prob_choice = flip(1 / (x + 1))
if prob_choice {
x = 0
} else {
x = x + 1
}
assert x
assume 0
} else {}
}

// [I] * [G] * (p o V) <= \s. wp[P]([V < V(s) - d(V(s))])(s)
proc progress_condition(init_x: UInt) -> (x: UInt)
pre [true] * ([0 < init_x] * (1 / (init_x + 1)))
post [x <= (init_x - 1)]
{
var prob_choice: Bool
x = init_x
prob_choice = flip(1 / (x + 1))
if prob_choice {
x = 0
} else {
x = x + 1
}
}
}
Loading
Loading