CBMC
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 
17 class code_assignt;
18 class exprt;
19 class goto_tracet;
20 class namespacet;
22 
24 {
25 public:
26  explicit graphml_witnesst(const namespacet &_ns)
27  : ns(_ns)
28  {
29  }
30 
31  void operator()(const goto_tracet &goto_trace);
32  void operator()(const symex_target_equationt &equation);
33 
34  const graphmlt &graph()
35  {
36  return graphml;
37  }
38 
39 protected:
40  const namespacet &ns;
42 
43  void remove_l0_l1(exprt &expr);
44  std::string convert_assign_rec(
45  const irep_idt &identifier,
46  const code_assignt &assign);
47 
48  template <typename T>
49  static void hash_combine(std::size_t &seed, const T &v)
50  {
51  std::hash<T> hasher;
52  seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
53  }
54 
55  template <typename S, typename T>
56  struct pair_hash // NOLINT(readability/identifiers)
57  {
58  std::size_t operator()(const std::pair<S, T> &v) const
59  {
60  std::size_t seed = 0;
61  hash_combine(seed, v.first);
62  hash_combine(seed, v.second);
63  return seed;
64  }
65  };
66  std::unordered_map<
67  std::pair<unsigned int, const irept::dt *>,
68  std::string,
69  pair_hash<unsigned int, const irept::dt *>>
71 };
72 
73 #endif // CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
A goto_instruction_codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
Trace of a GOTO program.
Definition: goto_trace.h:177
const namespacet & ns
const graphmlt & graph()
static void hash_combine(std::size_t &seed, const T &v)
void operator()(const goto_tracet &goto_trace)
counterexample witness
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
graphml_witnesst(const namespacet &_ns)
void remove_l0_l1(exprt &expr)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Read/write graphs as GraphML.
std::size_t operator()(const std::pair< S, T > &v) const