Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/proof_checker.cpp	Lines:	89	159	56.0 %
Date:	2021-05-24	Branches:	127	620	20.5 %


/******************************************************************************
 * 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 "expr/proof_checker.h"

#include "expr/proof_node.h"
#include "expr/skolem_manager.h"
#include "options/proof_options.h"
#include "smt/smt_statistics_registry.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"))
{
}

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)
    {
      Notice() << "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 (options::proofEagerChecking())
  {
    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
    Notice() << "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())
  {
    Notice() << "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;
}

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