diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 3387ec0793..afe9402e94 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -1990,12 +1990,39 @@ std::vector> ASTConverter::convertTranslationUnit() { Out.push_back(std::move(Fn)); BuiltinFunctions.clear(); + // A lifted choose is defined by its axiom, and it belongs to the function + // it is written in: that function reaches what the choose applies. + std::set ChoiceIdentities; + for (const auto &Fn : Out) + if (Fn->IsChoice) + ChoiceIdentities.insert(Fn->Identity); std::map> CallGraph; for (const auto &Fn : Out) { for (const auto &Target : Out) - if (bodyReferencesFunction(*Fn, Target->Identity)) + if (Fn->IsChoice ? llvm::any_of(Fn->Postconditions, + [&](const auto &Axiom) { + return exprReferencesSpecCall( + Axiom.get(), Target->Identity); + }) + : bodyReferencesFunction(*Fn, Target->Identity)) CallGraph[Fn->Identity].insert(Target->Identity); } + for (const auto &Fn : Out) { + if (Fn->IsChoice) + continue; + std::set &Edges = CallGraph[Fn->Identity]; + std::set Seen; + std::vector Work(Edges.begin(), Edges.end()); + while (!Work.empty()) { + const std::string Current = std::move(Work.back()); + Work.pop_back(); + if (!ChoiceIdentities.count(Current) || !Seen.insert(Current).second) + continue; + for (const std::string &Next : CallGraph[Current]) + if (Edges.insert(Next).second || ChoiceIdentities.count(Next)) + Work.push_back(Next); + } + } std::set RequiresCallDefinedness; for (auto &Fn : Out) @@ -2042,9 +2069,17 @@ std::vector> ASTConverter::convertTranslationUnit() { std::set InductiveCycles; for (const auto &Fn : Out) if (Fn->Unfolding && Reach[Fn->Identity].count(Fn->Identity)) { - Errors.push_back(Fn->Name + ": an inductive predicate applies itself " - "only in its body or through inductive " - "predicates, not through another spec"); + const bool InChoice = + llvm::any_of(Reach[Fn->Identity], [&](const std::string &Id) { + return ChoiceIdentities.count(Id) && Reach[Id].count(Fn->Identity); + }); + Errors.push_back( + Fn->Name + + (InChoice ? ": an inductive predicate occurs in the bodies of its " + "group only positively, never inside cppverify::choose" + : ": an inductive predicate applies itself only in its " + "body or through inductive predicates, not through " + "another spec")); for (const std::string &Other : Reach[Fn->Identity]) if (Reach[Other].count(Fn->Identity)) InductiveCycles.insert(Other); @@ -2082,12 +2117,13 @@ std::vector> ASTConverter::convertTranslationUnit() { } for (auto &Fn : Out) { // A rejected inductive predicate keeps a body without a measure. - if (InductiveCycles.count(Fn->Identity) || + if (Fn->IsChoice || InductiveCycles.count(Fn->Identity) || (Fn->InductiveLoc.isValid() && !Fn->Unfolding)) continue; std::set Group; for (const std::string &Other : Reach[Fn->Identity]) - if (Other != Fn->Identity && Reach[Other].count(Fn->Identity)) + if (Other != Fn->Identity && !ChoiceIdentities.count(Other) && + Reach[Other].count(Fn->Identity)) Group.insert(Other); if (!Group.empty()) { // A cycle terminates when every call within it lowers one shared diff --git a/clang/lib/Verify/Transform/SpecInline.cpp b/clang/lib/Verify/Transform/SpecInline.cpp index dc8def87bc..6cc8dc45b8 100644 --- a/clang/lib/Verify/Transform/SpecInline.cpp +++ b/clang/lib/Verify/Transform/SpecInline.cpp @@ -1488,8 +1488,29 @@ struct RecursiveSpecSite { std::vector Quantifiers; }; +/// The `exists` of a lifted choose's axiom, `!exists(k, P) || P(result)`, at +/// the arguments of \p Call; null if the axiom has another shape. +static std::unique_ptr choiceWitness(const VFunction &Choice, + const VSpecCallExpr &Call) { + if (Choice.Postconditions.empty() || Choice.Params.size() != Call.Args.size()) + return nullptr; + const VExpr *Axiom = Choice.Postconditions.front().get(); + if (Axiom->K != VExpr::BinOp) + return nullptr; + const auto *Or = static_cast(Axiom); + if (Or->Op != VBinOp::Or || Or->Lhs->K != VExpr::UnaryOp) + return nullptr; + const auto *Not = static_cast(Or->Lhs.get()); + if (Not->Op != VUnaryOp::Not || Not->Operand->K != VExpr::Exists) + return nullptr; + std::map> Arguments; + for (size_t I = 0; I < Call.Args.size(); ++I) + Arguments[Choice.Params[I].first] = cloneVExpr(Call.Args[I].get()); + return substParamsInExpr(Not->Operand.get(), Arguments); +} + static void collectRecursiveSpecCallsInExpr( - const VExpr *E, const VFunction &Fn, + const VExpr *E, const VFunction &Fn, const FunctionMap &FnMap, const std::map> &Env, const VExpr *Guard, std::vector &Sites, const std::vector &Quantifiers, @@ -1514,13 +1535,23 @@ static void collectRecursiveSpecCallsInExpr( Sites.push_back(std::move(Site)); } for (const auto &A : C->Args) - collectRecursiveSpecCallsInExpr(A.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(A.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); + // A choose is evaluated where it is written: the calls in its body, at + // every value of its binder, are the caller's. + if (auto It = FnMap.find(C->CalleeIdentity); + It != FnMap.end() && It->second->IsChoice) { + if (std::unique_ptr Witness = choiceWitness(*It->second, *C)) + collectRecursiveSpecCallsInExpr(Witness.get(), Fn, FnMap, Env, Guard, + Sites, Quantifiers, Unsupported); + else + Unsupported = true; + } return; } case VExpr::BinOp: { const auto *B = static_cast(E); - collectRecursiveSpecCallsInExpr(B->Lhs.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(B->Lhs.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); std::unique_ptr RightGuard = cloneVExpr(Guard); if (B->Op == VBinOp::And) @@ -1531,74 +1562,77 @@ static void collectRecursiveSpecCallsInExpr( std::move(RightGuard), makeDecreaseNot(substParamsInExpr(B->Lhs.get(), Env), B->Loc), B->Loc); - collectRecursiveSpecCallsInExpr(B->Rhs.get(), Fn, Env, RightGuard.get(), - Sites, Quantifiers, Unsupported); + collectRecursiveSpecCallsInExpr(B->Rhs.get(), Fn, FnMap, Env, + RightGuard.get(), Sites, Quantifiers, + Unsupported); return; } case VExpr::UnaryOp: collectRecursiveSpecCallsInExpr( - static_cast(E)->Operand.get(), Fn, Env, Guard, - Sites, Quantifiers, Unsupported); + static_cast(E)->Operand.get(), Fn, FnMap, Env, + Guard, Sites, Quantifiers, Unsupported); return; case VExpr::Cast: collectRecursiveSpecCallsInExpr( - static_cast(E)->Inner.get(), Fn, Env, Guard, Sites, - Quantifiers, Unsupported); + static_cast(E)->Inner.get(), Fn, FnMap, Env, Guard, + Sites, Quantifiers, Unsupported); return; case VExpr::Load: { const auto *Load = static_cast(E); - collectRecursiveSpecCallsInExpr(Load->Ptr.get(), Fn, Env, Guard, Sites, - Quantifiers, Unsupported); - collectRecursiveSpecCallsInExpr(Load->AccessCondition.get(), Fn, Env, Guard, + collectRecursiveSpecCallsInExpr(Load->Ptr.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); + collectRecursiveSpecCallsInExpr(Load->AccessCondition.get(), Fn, FnMap, Env, + Guard, Sites, Quantifiers, Unsupported); return; } case VExpr::Old: collectRecursiveSpecCallsInExpr( - static_cast(E)->Inner.get(), Fn, Env, Guard, Sites, - Quantifiers, Unsupported); + static_cast(E)->Inner.get(), Fn, FnMap, Env, Guard, + Sites, Quantifiers, Unsupported); return; case VExpr::Conditional: { const auto *C = static_cast(E); - collectRecursiveSpecCallsInExpr(C->Cond.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(C->Cond.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); auto Cond = substParamsInExpr(C->Cond.get(), Env); auto ThenGuard = makeDecreaseAnd(cloneVExpr(Guard), cloneVExpr(Cond.get()), C->Loc); auto ElseGuard = makeDecreaseAnd( cloneVExpr(Guard), makeDecreaseNot(std::move(Cond), C->Loc), C->Loc); - collectRecursiveSpecCallsInExpr(C->Then.get(), Fn, Env, ThenGuard.get(), - Sites, Quantifiers, Unsupported); - collectRecursiveSpecCallsInExpr(C->Else.get(), Fn, Env, ElseGuard.get(), - Sites, Quantifiers, Unsupported); + collectRecursiveSpecCallsInExpr(C->Then.get(), Fn, FnMap, Env, + ThenGuard.get(), Sites, Quantifiers, + Unsupported); + collectRecursiveSpecCallsInExpr(C->Else.get(), Fn, FnMap, Env, + ElseGuard.get(), Sites, Quantifiers, + Unsupported); return; } case VExpr::OverflowCheck: { const auto *O = static_cast(E); - collectRecursiveSpecCallsInExpr(O->Lhs.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(O->Lhs.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); - collectRecursiveSpecCallsInExpr(O->Rhs.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(O->Rhs.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); return; } case VExpr::Forall: case VExpr::Exists: { const auto *Q = static_cast(E); - collectRecursiveSpecCallsInExpr(Q->Lo.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(Q->Lo.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); - collectRecursiveSpecCallsInExpr(Q->Hi.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(Q->Hi.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); std::vector Inner = Quantifiers; Inner.push_back(Q); - collectRecursiveSpecCallsInExpr(Q->Body.get(), Fn, Env, Guard, Sites, Inner, - Unsupported); + collectRecursiveSpecCallsInExpr(Q->Body.get(), Fn, FnMap, Env, Guard, Sites, + Inner, Unsupported); return; } case VExpr::HeapStore: { const auto *H = static_cast(E); - collectRecursiveSpecCallsInExpr(H->Ptr.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(H->Ptr.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); - collectRecursiveSpecCallsInExpr(H->Val.get(), Fn, Env, Guard, Sites, + collectRecursiveSpecCallsInExpr(H->Val.get(), Fn, FnMap, Env, Guard, Sites, Quantifiers, Unsupported); return; } @@ -1607,8 +1641,8 @@ static void collectRecursiveSpecCallsInExpr( return; case VExpr::FieldAccess: collectRecursiveSpecCallsInExpr( - static_cast(E)->Base.get(), Fn, Env, Guard, - Sites, Quantifiers, Unsupported); + static_cast(E)->Base.get(), Fn, FnMap, Env, + Guard, Sites, Quantifiers, Unsupported); return; case VExpr::Literal: case VExpr::Var: @@ -1619,15 +1653,15 @@ static void collectRecursiveSpecCallsInExpr( static std::vector collectRecursiveSpecCallsInBody( const std::vector> &Stmts, const VFunction &Fn, - std::vector &Sites, std::vector States, - bool &Unsupported) { + const FunctionMap &FnMap, std::vector &Sites, + std::vector States, bool &Unsupported) { for (const auto &S : Stmts) { std::vector NextStates; for (DecreaseState &State : States) { switch (S->K) { case VStmt::Assign: { const auto &A = static_cast(*S); - collectRecursiveSpecCallsInExpr(A.Value.get(), Fn, State.Env, + collectRecursiveSpecCallsInExpr(A.Value.get(), Fn, FnMap, State.Env, State.Guard.get(), Sites, {}, Unsupported); State.Env[A.Target] = substParamsInExpr(A.Value.get(), State.Env); @@ -1636,12 +1670,12 @@ static std::vector collectRecursiveSpecCallsInBody( } case VStmt::Return: collectRecursiveSpecCallsInExpr( - static_cast(*S).Value.get(), Fn, State.Env, - State.Guard.get(), Sites, {}, Unsupported); + static_cast(*S).Value.get(), Fn, FnMap, + State.Env, State.Guard.get(), Sites, {}, Unsupported); break; case VStmt::If: { const auto &I = static_cast(*S); - collectRecursiveSpecCallsInExpr(I.Cond.get(), Fn, State.Env, + collectRecursiveSpecCallsInExpr(I.Cond.get(), Fn, FnMap, State.Env, State.Guard.get(), Sites, {}, Unsupported); auto Cond = substParamsInExpr(I.Cond.get(), State.Env); @@ -1652,7 +1686,7 @@ static std::vector collectRecursiveSpecCallsInBody( std::vector ThenStates; ThenStates.push_back(std::move(ThenState)); ThenStates = collectRecursiveSpecCallsInBody( - I.Then, Fn, Sites, std::move(ThenStates), Unsupported); + I.Then, Fn, FnMap, Sites, std::move(ThenStates), Unsupported); NextStates.insert(NextStates.end(), std::make_move_iterator(ThenStates.begin()), std::make_move_iterator(ThenStates.end())); @@ -1664,7 +1698,7 @@ static std::vector collectRecursiveSpecCallsInBody( std::vector ElseStates; ElseStates.push_back(std::move(ElseState)); ElseStates = collectRecursiveSpecCallsInBody( - I.Else, Fn, Sites, std::move(ElseStates), Unsupported); + I.Else, Fn, FnMap, Sites, std::move(ElseStates), Unsupported); NextStates.insert(NextStates.end(), std::make_move_iterator(ElseStates.begin()), std::make_move_iterator(ElseStates.end())); @@ -1715,6 +1749,57 @@ lexicographicDecrease(const std::vector> &CalleeDec, return LexLess; } +/// \p Fact, the axiom of the choose \p Call, where the calls of \p Fn's +/// recursion cycle in the choose's body lower \p Measure: the choose is part +/// of the definition it is written in, whose values are facts only there. +static std::unique_ptr +guardChoiceAxiom(std::unique_ptr Fact, const VFunction &Fn, + const FunctionMap &FnMap, const VFunction &Choice, + const VSpecCallExpr &Call, + const std::vector> &Measure) { + std::unique_ptr Witness = choiceWitness(Choice, Call); + if (!Fact || !Witness) + return Fact; + std::vector Sites; + bool Unsupported = false; + const auto True = + std::make_unique(1, VType::makeBool(), Call.Loc); + collectRecursiveSpecCallsInExpr(Witness.get(), Fn, FnMap, {}, True.get(), + Sites, {}, Unsupported); + if (Unsupported) + return Fact; + for (const RecursiveSpecSite &Site : Sites) { + const VFunction *Callee = &Fn; + if (Site.Callee != Fn.Identity) + if (auto It = FnMap.find(Site.Callee); It != FnMap.end()) + Callee = It->second; + auto ArgMap = bindParams(*Callee, Site.Args); + std::vector> CalleeDec; + bool Complete = !Measure.empty() && Callee->Identity == Site.Callee && + Callee->Decreases.size() == Measure.size(); + for (const auto &Decrease : Callee->Decreases) { + CalleeDec.push_back(substParamsInExpr(Decrease.get(), ArgMap)); + Complete = Complete && CalleeDec.back(); + } + std::unique_ptr Lower = + Complete ? lexicographicDecrease(CalleeDec, Measure, Site.Loc) + : std::make_unique(false, VType::makeBool(), + Site.Loc); + Lower = std::make_unique( + VBinOp::Or, makeDecreaseNot(cloneVExpr(Site.Guard.get()), Site.Loc), + std::move(Lower), VType::makeBool(), Site.Loc); + for (auto It = Site.Quantifiers.rbegin(); It != Site.Quantifiers.rend(); + ++It) + Lower = std::make_unique( + It->Binder, cloneVExpr(It->Lo.get()), cloneVExpr(It->Hi.get()), + std::move(Lower), Site.Loc, It->BinderType); + Fact = std::make_unique( + VBinOp::Or, makeDecreaseNot(std::move(Lower), Site.Loc), + std::move(Fact), VType::makeBool(), Site.Loc); + } + return Fact; +} + static void addSpecPostChecks(PassiveProgram &P, const VFunction &Fn, const FunctionMap &FnMap, bool PremisesDerive = false); @@ -1766,7 +1851,7 @@ PassiveProgram verify::buildDecreasesChecks(const VFunction &Fn, std::make_unique(1, VType::makeBool(), SourceLocation()); std::vector SpecStates; SpecStates.push_back(std::move(SpecInitial)); - collectRecursiveSpecCallsInBody(Fn.Body, Fn, SpecSites, + collectRecursiveSpecCallsInBody(Fn.Body, Fn, FnMap, SpecSites, std::move(SpecStates), UnsupportedSpecRecursion); } @@ -2479,6 +2564,13 @@ static void addPostApplicationFacts(PassiveProgram &P, const VFunction &Fn, for (const std::string &Member : Step->RecursionGroup) Group.insert(predicateOf(Member)); } + std::vector> Measure; + std::map> Self; + for (const auto &Param : Fn.Params) + Self[Param.first] = + std::make_unique(Param.first, Param.second, SourceLocation()); + for (const auto &Decrease : Fn.Decreases) + Measure.push_back(substParamsInExpr(Decrease.get(), Self)); std::vector> Facts; std::vector Enclosing; // The applications the check names, whose definitions the solver receives. @@ -2517,19 +2609,15 @@ static void addPostApplicationFacts(PassiveProgram &P, const VFunction &Fn, if (Fn.Cluster.count(Callee.Identity)) { Theorem = false; // Another spec of its cluster, below the measure. - std::vector> Measure; - std::map> Self; - for (const auto &Param : Fn.Params) - Self[Param.first] = std::make_unique( - Param.first, Param.second, SourceLocation()); - for (const auto &Decrease : Fn.Decreases) - Measure.push_back(substParamsInExpr(Decrease.get(), Self)); Fact = specInductionFacts(Callee, Call.Args, &Call, Call.Loc, Measure, FnMap); if (Fact && !Callee.Postconditions.empty()) P.InductivePosts.insert(Callee.Identity); } else if (!Group.count(Callee.Identity)) { Fact = specApplicationFacts(Callee, Call.Args, &Call, Call.Loc); + if (Callee.IsChoice) + Fact = + guardChoiceAxiom(std::move(Fact), Fn, FnMap, Callee, Call, Measure); if (!Callee.Postconditions.empty()) P.AssumedPosts.insert(Callee.Identity); if (Callee.Unfolding) @@ -2627,6 +2715,9 @@ static void addSpecPostChecks(PassiveProgram &P, const VFunction &Fn, continue; std::unique_ptr Fact = specApplicationFacts( *Site.Callee, Site.Args, Application.get(), Site.Loc); + if (Site.Callee->IsChoice) + Fact = guardChoiceAxiom(std::move(Fact), Fn, FnMap, *Site.Callee, + *Application, CurrentDec); if (!Fact) continue; const bool InCycle = Call.CalleeIdentity == Fn.Identity || diff --git a/clang/test/Verify/suite/choose_recursion.cpp b/clang/test/Verify/suite/choose_recursion.cpp new file mode 100644 index 0000000000..bf5eb368ca --- /dev/null +++ b/clang/test/Verify/suite/choose_recursion.cpp @@ -0,0 +1,72 @@ +// RUN: not %cpp-verify --timeout=20000 %s -- 2>&1 | FileCheck %s +// +// A call inside a choose is a call of the function the choose is in: it must +// lower the measure for every value the choice may take. + +// Every application inside the choose lowers n. +cppverify::spec int depth(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : cppverify::choose(k, k == depth(n - 1) + 1); +} +// CHECK-DAG: Verified: spec decreases: depth + +// The binder ranges over [0, n), below n. +cppverify::spec int below(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : cppverify::choose(k, 0, n, below(k) == 0); +} +// CHECK-DAG: Verified: spec decreases: below + +// The direct call lowers n, the one inside the choose does not. +cppverify::spec int stuck(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : stuck(n - 1) + cppverify::choose(k, n == 1 ? k == stuck(n) + 1 : k == 0); +} +// CHECK-DAG: error: spec decreases failed: stuck [backend=z3] [reason=counterexample] (n [type=math-i32] = 1) + +// The same with a postcondition, which is proved with termination. +cppverify::spec int stuck_post(int n) + cppverify::decreases(n) + cppverify::post(cppverify::result >= 0) +{ + return n <= 0 ? 0 : cppverify::choose(k, n == 1 ? k == stuck_post(n) + 1 : k == 0); +} +// CHECK-DAG: error: spec decreases and post failed: stuck_post [backend=z3] [reason=counterexample] (n [type=math-i32] = 1) + +// The axiom of a choose holds where its applications lower the measure, +// which places the choice in [0, n). +cppverify::spec int pick(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : pick(cppverify::choose(k, 0, n, k == 0 || pick(k) > 3)); +} +// CHECK-DAG: Verified: spec decreases: pick + +// An unbounded binder can be any value, so the call need not be lower. +cppverify::spec int unbounded(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : cppverify::choose(k, unbounded(k) == 0); +} +// CHECK-DAG: error: spec decreases failed: unbounded [backend=z3] [reason=counterexample] (n [type=math-i32] = {{[1-9][0-9]*}}) + +int forty_two(int x) + cppverify::post(cppverify::result == 42) +{ + cppverify::check(stuck(x) == stuck(x)); + if (x == 1) + return 0; + return 42; +} +// CHECK-DAG: Unresolved: forty_two [backend=z3] [reason=spec.termination] (relies on the definition of stuck, whose termination is not established) + +// A choose that does not apply its own function is unaffected. +cppverify::spec int half(int n) { return cppverify::choose(k, 2 * k == n); } +cppverify::proof void halves() + cppverify::post(half(8) == 4) +{ +} +// CHECK-DAG: Verified: halves diff --git a/clang/test/Verify/suite/choose_recursion_errors.cpp b/clang/test/Verify/suite/choose_recursion_errors.cpp new file mode 100644 index 0000000000..0ff7184f30 --- /dev/null +++ b/clang/test/Verify/suite/choose_recursion_errors.cpp @@ -0,0 +1,34 @@ +// RUN: not %cpp-verify %s -- 2>&1 | FileCheck %s +// +// A choose belongs to the function it is written in: a spec that applies +// itself inside one is recursive and needs a measure, and an inductive +// predicate may not apply its group inside one, where it is not positive. + +// f(7) would have to equal f(7) + 1. +cppverify::spec int f(int n) +{ + return cppverify::choose(k, n == 7 ? k == f(n) + 1 : k == 0); +} +// CHECK-DAG: error: f: recursive spec and proof functions require decreases + +int forty_two(int x) + cppverify::post(cppverify::result == 42) +{ + cppverify::check(f(x) == f(x)); + if (x == 7) + return 0; + return 42; +} + +cppverify::spec int ping(int n); +cppverify::spec int pong(int n) { return cppverify::choose(k, k == ping(n)); } +cppverify::spec int ping(int n) { return n <= 0 ? 0 : pong(n) + 1; } +// CHECK-DAG: error: {{ping|pong}}: mutually recursive spec functions require decreases clauses, all of the same length + +cppverify::spec bool liar(int n) + cppverify::inductive +{ + return cppverify::choose(k, 0, 2, k == (liar(n) ? 0 : 1)) == 1; +} +// CHECK-DAG: error: liar: an inductive predicate occurs in the bodies of its group only positively, never inside cppverify::choose +// CHECK-NOT: Verified diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index ee87afbf7a..7d9e90a4ca 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -166,8 +166,10 @@ ranges over all mathematical integers. A `cppverify::trigger(term)` mark is an i `Cast` flagged `IsTrigger` around the term. Each `cppverify::choose` is lifted to a synthesized uninterpreted spec function (`IsChoice`) of the values its body mentions, whose postcondition is the Hilbert axiom `!cppverify::exists(k, P) || P(cppverify::result)` -(with the range for a bounded choose). A collection operation is a `SpecCall` -whose identity is `__cppverify.`, such as `__cppverify.seq.push`. +(with the range for a bounded choose). The calls in its body are calls of the +function it is written in, for recursion and termination. A collection +operation is a `SpecCall` whose identity is `__cppverify.`, such as +`__cppverify.seq.push`. `cppverify::valid(p, n)` becomes a call of the synthesized builtin spec `__cppverify_valid(p, n)` (body `true`, marked `IsBuiltin` and never reported), so the extent marker scan treats it exactly like a user-declared @@ -817,8 +819,9 @@ check did not pass to `Unresolved` with reason `spec.reads`. termination module (its own module `spec post:` when it is not recursive): each call within the recursion cycle contributes the assumption `dec(a) < dec(x) -> post(a, f(a))` under the cycle's well-founded relation, -each call of another spec its post, and every return value must satisfy the -post. Since the facts at lower measures are the induction hypothesis, a +each call of another spec its post (a choose its axiom only where the calls +of the cycle in its body lower the measure), and every return value must +satisfy the post. Since the facts at lower measures are the induction hypothesis, a proof establishes termination and the post together. Passivization then assumes `post(t, f(t))` at every application `f(t)` in a function, the preconditions included, quantified like the application, and at every diff --git a/docs/DESIGN.md b/docs/DESIGN.md index ac1b25db13..c9b3b82086 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -362,10 +362,10 @@ cppverify::spec int fibo(int n) inside `cppverify::old(...)`, or the call-site state of a callee contract). - Can be recursive (with `cppverify::decreases`). Its termination is proved without its own definition, so every recursive call must lower the measure whatever the - spec's other calls return; a call inside `cppverify::forall` or `cppverify::exists` must lower it - for every bound value. Functions of one kind (spec, proof, or executable) - may recurse through each other when they share a measure of one length that - every call within the cycle lowers. + spec's other calls return; a call inside `cppverify::forall`, `cppverify::exists`, or + `cppverify::choose` must lower it for every bound value. Functions of one kind + (spec, proof, or executable) may recurse through each other when they share + a measure of one length that every call within the cycle lowers. - May declare `cppverify::reads(p, n)`: the cells `p[0..n)` it depends on, checked against its body (every load, and every range a heap-reading callee reads, lies inside). A write outside them leaves every application unchanged, and @@ -438,8 +438,9 @@ cppverify::spec bool reach(int a, int b) - The body returns a condition, under `if` and `else` at most, in which the predicate occurs only positively: as a conjunct or disjunct, a branch of `?:`, under `cppverify::exists`, or under a bounded `cppverify::forall`; never negated, compared, - converted, in a condition, in an argument, or under a `cppverify::forall` without - bounds. It takes no `cppverify::decreases` or `cppverify::when`, and it may read memory. + converted, in a condition, in an argument, inside `cppverify::choose`, or under a + `cppverify::forall` without bounds. It takes no `cppverify::decreases` or + `cppverify::when`, and it may read memory. Predicates that apply each other are defined together, each under the same conditions; a predicate never applies itself through a spec that is not inductive, since the conditions could not be checked there. diff --git a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst index b503716880..21a8e152b3 100644 --- a/website/source/book/part-ii/ch13-spec-and-proof-functions.rst +++ b/website/source/book/part-ii/ch13-spec-and-proof-functions.rst @@ -153,10 +153,11 @@ measure whatever the spec's other calls return: return n <= 0 ? 0 : 1 + nested(nested(n - 1)); } -A recursive call inside ``cppverify::forall`` or ``cppverify::exists`` must decrease the measure -for every value of the bound variable. Spec functions may call each other in a -cycle when they share a measure of the same length and every call within the -cycle lowers it; the termination proof treats all of them as opaque: +A recursive call inside ``cppverify::forall``, ``cppverify::exists``, or ``cppverify::choose`` must +decrease the measure for every value of the bound variable. Spec functions may +call each other in a cycle when they share a measure of the same length and +every call within the cycle lowers it; the termination proof treats all of them +as opaque: .. code-block:: cpp