Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/proof_checker.cpp	Lines:	91	165	55.2 %
Date:	2021-11-07	Branches:	128	612	20.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of proof checker.
 */

#include "proof/proof_checker.h"

#include "expr/skolem_manager.h"
#include "options/proof_options.h"
#include "proof/proof_node.h"
#include "smt/smt_statistics_registry.h"
#include "util/rational.h"

using namespace cvc5::kind;

namespace cvc5 {

Node ProofRuleChecker::check(PfRule id,
                             const std::vector<Node>& children,
                             const std::vector<Node>& args)
{
  // call instance-specific checkInternal method
  return checkInternal(id, children, args);
}

bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
{
  // must be a non-negative integer constant that fits an unsigned int
  if (n.isConst() && n.getType().isInteger()
      && n.getConst<Rational>().sgn() >= 0
      && n.getConst<Rational>().getNumerator().fitsUnsignedInt())
  {
    i = n.getConst<Rational>().getNumerator().toUnsignedInt();
    return true;
  }
  return false;
}

bool ProofRuleChecker::getBool(TNode n, bool& b)
{
  if (n.isConst() && n.getType().isBoolean())
  {
    b = n.getConst<bool>();
    return true;
  }
  return false;
}

bool ProofRuleChecker::getKind(TNode n, Kind& k)
{
  uint32_t i;
  if (!getUInt32(n, i))
  {
    return false;
  }
  k = static_cast<Kind>(i);
  return true;
}

Node ProofRuleChecker::mkKindNode(Kind k)
{
  if (k == UNDEFINED_KIND)
  {
    // UNDEFINED_KIND is negative, hence return null to avoid cast
    return Node::null();
  }
  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k)));
}

ProofCheckerStatistics::ProofCheckerStatistics()
    : d_ruleChecks(smtStatisticsRegistry().registerHistogram<PfRule>(
          "ProofCheckerStatistics::ruleChecks")),
      d_totalRuleChecks(smtStatisticsRegistry().registerInt(
          "ProofCheckerStatistics::totalRuleChecks"))
{
}

ProofChecker::ProofChecker(bool eagerCheck,
                           uint32_t pclevel,
                           rewriter::RewriteDb* rdb)
    : d_eagerCheck(eagerCheck), d_pclevel(pclevel), d_rdb(rdb)
{
}

Node ProofChecker::check(ProofNode* pn, Node expected)
{
  return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
}

Node ProofChecker::check(
    PfRule id,
    const std::vector<std::shared_ptr<ProofNode>>& children,
    const std::vector<Node>& args,
    Node expected)
{
  // optimization: immediately return for ASSUME
  if (id == PfRule::ASSUME)
  {
    Assert(children.empty());
    Assert(args.size() == 1 && args[0].getType().isBoolean());
    Assert(expected.isNull() || expected == args[0]);
    return expected;
  }
  // record stat
  d_stats.d_ruleChecks << id;
  ++d_stats.d_totalRuleChecks;
  Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
  std::vector<Node> cchildren;
  for (const std::shared_ptr<ProofNode>& pc : children)
  {
    Assert(pc != nullptr);
    Node cres = pc->getResult();
    if (cres.isNull())
    {
      Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
      Unreachable()
          << "ProofChecker::check: child proof was invalid (null conclusion)"
          << std::endl;
      // should not have been able to create such a proof node
      return Node::null();
    }
    cchildren.push_back(cres);
    if (Trace.isOn("pfcheck"))
    {
      std::stringstream ssc;
      pc->printDebug(ssc);
      Trace("pfcheck") << "     child: " << ssc.str() << " : " << cres
                       << std::endl;
    }
  }
  Trace("pfcheck") << "      args: " << args << std::endl;
  Trace("pfcheck") << "  expected: " << expected << std::endl;
  std::stringstream out;
  // we use trusted (null) checkers here, since we want the proof generation to
  // proceed without failing here. We always enable output since a failure
  // implies that we will exit with the error message below.
  Node res = checkInternal(id, cchildren, args, expected, out, true, true);
  if (res.isNull())
  {
    Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
    Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
    // it did not match the given expectation, fail
    return Node::null();
  }
  Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
  return res;
}

Node ProofChecker::checkDebug(PfRule id,
                              const std::vector<Node>& cchildren,
                              const std::vector<Node>& args,
                              Node expected,
                              const char* traceTag)
{
  std::stringstream out;
  bool traceEnabled = Trace.isOn(traceTag);
  // Since we are debugging, we want to treat trusted (null) checkers as
  // a failure. We only enable output if the trace is enabled for efficiency.
  Node res =
      checkInternal(id, cchildren, args, expected, out, false, traceEnabled);
  if (traceEnabled)
  {
    Trace(traceTag) << "ProofChecker::checkDebug: " << id;
    if (res.isNull())
    {
      Trace(traceTag) << " failed, " << out.str() << std::endl;
    }
    else
    {
      Trace(traceTag) << " success" << std::endl;
    }
    Trace(traceTag) << "cchildren: " << cchildren << std::endl;
    Trace(traceTag) << "     args: " << args << std::endl;
  }
  return res;
}

Node ProofChecker::checkInternal(PfRule id,
                                 const std::vector<Node>& cchildren,
                                 const std::vector<Node>& args,
                                 Node expected,
                                 std::stringstream& out,
                                 bool useTrustedChecker,
                                 bool enableOutput)
{
  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
  if (it == d_checker.end())
  {
    // no checker for the rule
    if (enableOutput)
    {
      out << "no checker for rule " << id << std::endl;
    }
    return Node::null();
  }
  else if (it->second == nullptr)
  {
    if (useTrustedChecker)
    {
      out << "ProofChecker::check: trusting PfRule " << id << std::endl;
      // trusted checker
      return expected;
    }
    else
    {
      if (enableOutput)
      {
        out << "trusted checker for rule " << id << std::endl;
      }
      return Node::null();
    }
  }
  // check it with the corresponding checker
  Node res = it->second->check(id, cchildren, args);
  if (!expected.isNull())
  {
    Node expectedw = expected;
    if (res != expectedw)
    {
      if (enableOutput)
      {
        out << "result does not match expected value." << std::endl
            << "    PfRule: " << id << std::endl;
        for (const Node& c : cchildren)
        {
          out << "     child: " << c << std::endl;
        }
        for (const Node& a : args)
        {
          out << "       arg: " << a << std::endl;
        }
        out << "    result: " << res << std::endl
            << "  expected: " << expected << std::endl;
      }
      // it did not match the given expectation, fail
      return Node::null();
    }
  }
  // fails if pedantic level is not met
  if (d_eagerCheck)
  {
    std::stringstream serr;
    if (isPedanticFailure(id, serr, enableOutput))
    {
      if (enableOutput)
      {
        out << serr.str() << std::endl;
        if (Trace.isOn("proof-pedantic"))
        {
          Trace("proof-pedantic")
              << "Failed pedantic check for " << id << std::endl;
          Trace("proof-pedantic") << "Expected: " << expected << std::endl;
          out << "Expected: " << expected << std::endl;
        }
      }
      return Node::null();
    }
  }
  return res;
}

void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
{
  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
  if (it != d_checker.end())
  {
    // checker is already provided
    Trace("pfcheck")
        << "ProofChecker::registerChecker: checker already exists for " << id
        << std::endl;
    return;
  }
  d_checker[id] = psc;
}

void ProofChecker::registerTrustedChecker(PfRule id,
                                          ProofRuleChecker* psc,
                                          uint32_t plevel)
{
  AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: "
                                "pedantic level must be 0-10, got "
                             << plevel << " for " << id;
  registerChecker(id, psc);
  // overwrites if already there
  if (d_plevel.find(id) != d_plevel.end())
  {
    Trace("proof-pedantic")
        << "ProofChecker::registerTrustedRule: already provided pedantic "
           "level for "
        << id << std::endl;
  }
  d_plevel[id] = plevel;
}

ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
{
  std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id);
  if (it == d_checker.end())
  {
    return nullptr;
  }
  return it->second;
}

rewriter::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; }

uint32_t ProofChecker::getPedanticLevel(PfRule id) const
{
  std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
  if (itp != d_plevel.end())
  {
    return itp->second;
  }
  return 0;
}

bool ProofChecker::isPedanticFailure(PfRule id,
                                     std::ostream& out,
                                     bool enableOutput) const
{
  if (d_pclevel == 0)
  {
    return false;
  }
  std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
  if (itp != d_plevel.end())
  {
    if (itp->second <= d_pclevel)
    {
      if (enableOutput)
      {
        out << "pedantic level for " << id << " not met (rule level is "
            << itp->second << " which is at or below the pedantic level "
            << d_pclevel << ")";
        bool pedanticTraceEnabled = Trace.isOn("proof-pedantic");
        if (!pedanticTraceEnabled)
        {
          out << ", use -t proof-pedantic for details";
        }
      }
      return true;
    }
  }
  return false;
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of proof checker.
14		*/
15
16		#include "proof/proof_checker.h"
17
18		#include "expr/skolem_manager.h"
19		#include "options/proof_options.h"
20		#include "proof/proof_node.h"
21		#include "smt/smt_statistics_registry.h"
22		#include "util/rational.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27
28	6183619	Node ProofRuleChecker::check(PfRule id,
29		const std::vector<Node>& children,
30		const std::vector<Node>& args)
31		{
32		// call instance-specific checkInternal method
33	6183619	return checkInternal(id, children, args);
34		}
35
36	1193376	bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
37		{
38		// must be a non-negative integer constant that fits an unsigned int
39	3580128	if (n.isConst() && n.getType().isInteger()
40	1193376	&& n.getConst<Rational>().sgn() >= 0
41	3580128	&& n.getConst<Rational>().getNumerator().fitsUnsignedInt())
42		{
43	1193376	i = n.getConst<Rational>().getNumerator().toUnsignedInt();
44	1193376	return true;
45		}
46		return false;
47		}
48
49	1690	bool ProofRuleChecker::getBool(TNode n, bool& b)
50		{
51	1690	if (n.isConst() && n.getType().isBoolean())
52		{
53	1690	b = n.getConst<bool>();
54	1690	return true;
55		}
56		return false;
57		}
58
59	385122	bool ProofRuleChecker::getKind(TNode n, Kind& k)
60		{
61		uint32_t i;
62	385122	if (!getUInt32(n, i))
63		{
64		return false;
65		}
66	385122	k = static_cast<Kind>(i);
67	385122	return true;
68		}
69
70	549719	Node ProofRuleChecker::mkKindNode(Kind k)
71		{
72	549719	if (k == UNDEFINED_KIND)
73		{
74		// UNDEFINED_KIND is negative, hence return null to avoid cast
75		return Node::null();
76		}
77	549719	return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k)));
78		}
79
80	7989	ProofCheckerStatistics::ProofCheckerStatistics()
81	7989	: d_ruleChecks(smtStatisticsRegistry().registerHistogram<PfRule>(
82	15978	"ProofCheckerStatistics::ruleChecks")),
83	7989	d_totalRuleChecks(smtStatisticsRegistry().registerInt(
84	15978	"ProofCheckerStatistics::totalRuleChecks"))
85		{
86	7989	}
87
88	7989	ProofChecker::ProofChecker(bool eagerCheck,
89		uint32_t pclevel,
90	7989	rewriter::RewriteDb* rdb)
91	7989	: d_eagerCheck(eagerCheck), d_pclevel(pclevel), d_rdb(rdb)
92		{
93	7989	}
94
95	5096331	Node ProofChecker::check(ProofNode* pn, Node expected)
96		{
97	5096331	return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
98		}
99
100	6231691	Node ProofChecker::check(
101		PfRule id,
102		const std::vector<std::shared_ptr<ProofNode>>& children,
103		const std::vector<Node>& args,
104		Node expected)
105		{
106		// optimization: immediately return for ASSUME
107	6231691	if (id == PfRule::ASSUME)
108		{
109	648180	Assert(children.empty());
110	648180	Assert(args.size() == 1 && args[0].getType().isBoolean());
111	648180	Assert(expected.isNull() \|\| expected == args[0]);
112	648180	return expected;
113		}
114		// record stat
115	5583511	d_stats.d_ruleChecks << id;
116	5583511	++d_stats.d_totalRuleChecks;
117	5583511	Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
118	11167022	std::vector<Node> cchildren;
119	24078999	for (const std::shared_ptr<ProofNode>& pc : children)
120		{
121	18495488	Assert(pc != nullptr);
122	36990976	Node cres = pc->getResult();
123	18495488	if (cres.isNull())
124		{
125		Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
126		Unreachable()
127		<< "ProofChecker::check: child proof was invalid (null conclusion)"
128		<< std::endl;
129		// should not have been able to create such a proof node
130		return Node::null();
131		}
132	18495488	cchildren.push_back(cres);
133	18495488	if (Trace.isOn("pfcheck"))
134		{
135		std::stringstream ssc;
136		pc->printDebug(ssc);
137		Trace("pfcheck") << " child: " << ssc.str() << " : " << cres
138		<< std::endl;
139		}
140		}
141	5583511	Trace("pfcheck") << " args: " << args << std::endl;
142	5583511	Trace("pfcheck") << " expected: " << expected << std::endl;
143	11167022	std::stringstream out;
144		// we use trusted (null) checkers here, since we want the proof generation to
145		// proceed without failing here. We always enable output since a failure
146		// implies that we will exit with the error message below.
147	11167022	Node res = checkInternal(id, cchildren, args, expected, out, true, true);
148	5583511	if (res.isNull())
149		{
150		Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
151		Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
152		// it did not match the given expectation, fail
153		return Node::null();
154		}
155	5583511	Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
156	5583511	return res;
157		}
158
159	600108	Node ProofChecker::checkDebug(PfRule id,
160		const std::vector<Node>& cchildren,
161		const std::vector<Node>& args,
162		Node expected,
163		const char* traceTag)
164		{
165	1200216	std::stringstream out;
166	600108	bool traceEnabled = Trace.isOn(traceTag);
167		// Since we are debugging, we want to treat trusted (null) checkers as
168		// a failure. We only enable output if the trace is enabled for efficiency.
169		Node res =
170	600108	checkInternal(id, cchildren, args, expected, out, false, traceEnabled);
171	600108	if (traceEnabled)
172		{
173		Trace(traceTag) << "ProofChecker::checkDebug: " << id;
174		if (res.isNull())
175		{
176		Trace(traceTag) << " failed, " << out.str() << std::endl;
177		}
178		else
179		{
180		Trace(traceTag) << " success" << std::endl;
181		}
182		Trace(traceTag) << "cchildren: " << cchildren << std::endl;
183		Trace(traceTag) << " args: " << args << std::endl;
184		}
185	1200216	return res;
186		}
187
188	6183619	Node ProofChecker::checkInternal(PfRule id,
189		const std::vector<Node>& cchildren,
190		const std::vector<Node>& args,
191		Node expected,
192		std::stringstream& out,
193		bool useTrustedChecker,
194		bool enableOutput)
195		{
196	6183619	std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
197	6183619	if (it == d_checker.end())
198		{
199		// no checker for the rule
200		if (enableOutput)
201		{
202		out << "no checker for rule " << id << std::endl;
203		}
204		return Node::null();
205		}
206	6183619	else if (it->second == nullptr)
207		{
208		if (useTrustedChecker)
209		{
210		out << "ProofChecker::check: trusting PfRule " << id << std::endl;
211		// trusted checker
212		return expected;
213		}
214		else
215		{
216		if (enableOutput)
217		{
218		out << "trusted checker for rule " << id << std::endl;
219		}
220		return Node::null();
221		}
222		}
223		// check it with the corresponding checker
224	12367238	Node res = it->second->check(id, cchildren, args);
225	6183619	if (!expected.isNull())
226		{
227	8901926	Node expectedw = expected;
228	4450963	if (res != expectedw)
229		{
230		if (enableOutput)
231		{
232		out << "result does not match expected value." << std::endl
233		<< " PfRule: " << id << std::endl;
234		for (const Node& c : cchildren)
235		{
236		out << " child: " << c << std::endl;
237		}
238		for (const Node& a : args)
239		{
240		out << " arg: " << a << std::endl;
241		}
242		out << " result: " << res << std::endl
243		<< " expected: " << expected << std::endl;
244		}
245		// it did not match the given expectation, fail
246		return Node::null();
247		}
248		}
249		// fails if pedantic level is not met
250	6183619	if (d_eagerCheck)
251		{
252	4492	std::stringstream serr;
253	2246	if (isPedanticFailure(id, serr, enableOutput))
254		{
255		if (enableOutput)
256		{
257		out << serr.str() << std::endl;
258		if (Trace.isOn("proof-pedantic"))
259		{
260		Trace("proof-pedantic")
261		<< "Failed pedantic check for " << id << std::endl;
262		Trace("proof-pedantic") << "Expected: " << expected << std::endl;
263		out << "Expected: " << expected << std::endl;
264		}
265		}
266		return Node::null();
267		}
268		}
269	6183619	return res;
270		}
271
272	1168788	void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
273		{
274	1168788	std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
275	1168788	if (it != d_checker.end())
276		{
277		// checker is already provided
278		Trace("pfcheck")
279		<< "ProofChecker::registerChecker: checker already exists for " << id
280		<< std::endl;
281		return;
282		}
283	1168788	d_checker[id] = psc;
284		}
285
286	137186	void ProofChecker::registerTrustedChecker(PfRule id,
287		ProofRuleChecker* psc,
288		uint32_t plevel)
289		{
290	137186	AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: "
291		"pedantic level must be 0-10, got "
292		<< plevel << " for " << id;
293	137186	registerChecker(id, psc);
294		// overwrites if already there
295	137186	if (d_plevel.find(id) != d_plevel.end())
296		{
297		Trace("proof-pedantic")
298		<< "ProofChecker::registerTrustedRule: already provided pedantic "
299		"level for "
300		<< id << std::endl;
301		}
302	137186	d_plevel[id] = plevel;
303	137186	}
304
305		ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
306		{
307		std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id);
308		if (it == d_checker.end())
309		{
310		return nullptr;
311		}
312		return it->second;
313		}
314
315		rewriter::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; }
316
317	2491412	uint32_t ProofChecker::getPedanticLevel(PfRule id) const
318		{
319	2491412	std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
320	2491412	if (itp != d_plevel.end())
321		{
322	5691	return itp->second;
323		}
324	2485721	return 0;
325		}
326
327	2493487	bool ProofChecker::isPedanticFailure(PfRule id,
328		std::ostream& out,
329		bool enableOutput) const
330		{
331	2493487	if (d_pclevel == 0)
332		{
333	2493487	return false;
334		}
335		std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
336		if (itp != d_plevel.end())
337		{
338		if (itp->second <= d_pclevel)
339		{
340		if (enableOutput)
341		{
342		out << "pedantic level for " << id << " not met (rule level is "
343		<< itp->second << " which is at or below the pedantic level "
344		<< d_pclevel << ")";
345		bool pedanticTraceEnabled = Trace.isOn("proof-pedantic");
346		if (!pedanticTraceEnabled)
347		{
348		out << ", use -t proof-pedantic for details";
349		}
350		}
351		return true;
352		}
353		}
354		return false;
355		}
356
357	31137	} // namespace cvc5