cprover
graphml_witness.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Witnesses for Traces and Proofs
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
13 #define CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
14 
15 #include <xmllang/graphml.h>
16 
18 
19 #include "goto_trace.h"
20 
22 {
23 public:
24  explicit graphml_witnesst(const namespacet &_ns)
25  : ns(_ns)
26  {
27  }
28 
29  void operator()(const goto_tracet &goto_trace);
30  void operator()(const symex_target_equationt &equation);
31 
32  const graphmlt &graph()
33  {
34  return graphml;
35  }
36 
37 protected:
38  const namespacet &ns;
40 
41  void remove_l0_l1(exprt &expr);
42  std::string convert_assign_rec(
43  const irep_idt &identifier,
44  const code_assignt &assign);
45 
46  template <typename T>
47  static void hash_combine(std::size_t &seed, const T &v)
48  {
49  std::hash<T> hasher;
50  seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
51  }
52 
53  template <typename S, typename T>
54  struct pair_hash // NOLINT(readability/identifiers)
55  {
56  std::size_t operator()(const std::pair<S, T> &v) const
57  {
58  std::size_t seed = 0;
59  hash_combine(seed, v.first);
60  hash_combine(seed, v.second);
61  return seed;
62  }
63  };
64  std::unordered_map<
65  std::pair<unsigned int, const irept::dt *>,
66  std::string,
67  pair_hash<unsigned int, const irept::dt *>>
69 };
70 
71 #endif // CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
graphml_witnesst::graph
const graphmlt & graph()
Definition: graphml_witness.h:32
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_target_equation.h
Generate Equation using Symbolic Execution.
exprt
Base class for all expressions.
Definition: expr.h:53
graphml_witnesst::remove_l0_l1
void remove_l0_l1(exprt &expr)
Definition: graphml_witness.cpp:39
graphml.h
Read/write graphs as GraphML.
graphml_witnesst::cache
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
Definition: graphml_witness.h:68
goto_trace.h
Traces of GOTO Programs.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
graphml_witnesst::pair_hash
Definition: graphml_witness.h:55
graphml_witnesst::graphml_witnesst
graphml_witnesst(const namespacet &_ns)
Definition: graphml_witness.h:24
graphml_witnesst::graphml
graphmlt graphml
Definition: graphml_witness.h:39
graphml_witnesst::hash_combine
static void hash_combine(std::size_t &seed, const T &v)
Definition: graphml_witness.h:47
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
graphml_witnesst::operator()
void operator()(const goto_tracet &goto_trace)
counterexample witness
Definition: graphml_witness.cpp:279
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
graphml_witnesst::convert_assign_rec
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
Definition: graphml_witness.cpp:65
graphml_witnesst::ns
const namespacet & ns
Definition: graphml_witness.h:38
graphml_witnesst
Definition: graphml_witness.h:22
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
graphml_witnesst::pair_hash::operator()
std::size_t operator()(const std::pair< S, T > &v) const
Definition: graphml_witness.h:56
graphmlt
Definition: graphml.h:42