witnesses.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_SYMEX_WITNESSES_H
#define CPROVER_GOTO_SYMEX_WITNESSES_H
 
#include <boost/property_tree/xml_parser.hpp>
#include <util/symtab/namespace.h>
#include <irep2/irep2.h>
#include <langapi/language_util.h>
#include <goto-symex/trace/goto_trace.h>
#include <goto-symex/equation/symex_target_equation.h>
#include <goto-symex/waypoint.h>
#include <string>
#include <regex>
#include <vector>
#include <big-int/bigint.hh>
#include <yaml-cpp/yaml.h>
 
typedef boost::property_tree::ptree xmlnodet;
 
class nodet
{
private:
  static BigInt _id;
 
public:
  std::string id;
  bool entry = false;
  bool sink = false;
  bool violation = false;
  bool cycle_head = false;
  std::string invariant;
  std::string invariant_scope;
  std::string cwe; // comma-separated CWE list (e.g. "CWE-476, CWE-125")
  nodet(void)
  {
    id = "N" + integer2string(_id);
    _id += 1;
  }
};
 
class edget
{
private:
  static BigInt _id;
 
public:
  std::string id;
  std::string assumption;
  std::string assumption_scope;
  std::string assumption_resultfunction;
  std::string enter_function;
  std::string return_from_function;
  std::string thread_id;
  std::string create_thread;
  std::string origin_file;
  BigInt start_line = c_nonset;
  BigInt end_line = c_nonset;
  BigInt start_offset = c_nonset;
  BigInt end_offset = c_nonset;
  bool control = false;
  bool enter_loop_head = false;
  nodet *from_node;
  nodet *to_node;
  edget(void)
  {
    id = "E" + integer2string(_id);
    _id += 1;
    from_node = NULL;
    to_node = NULL;
  }
  edget(nodet *from_node, nodet *to_node)
  {
    id = "E" + integer2string(_id);
    _id += 1;
    this->from_node = from_node;
    this->to_node = to_node;
  }
};
 
class invariant
{
public:
  enum Type
  {
    loop_invariant,
    loop_transition_invariant,
    location_invariant,
    location_transition_invariant,
    unknown
  };
 
  Type type = unknown;
  std::string file;
  std::string value;
  std::string format;
  BigInt line = c_nonset;
  BigInt column = c_nonset;
  std::string function;
};
 
class grapht
{
private:
  std::vector<BigInt> threads;
  void create_initial_edge();
 
public:
  enum typet
  {
    VIOLATION,
    CORRECTNESS
  };
  typet witness_type;
  std::string verified_file;
  std::vector<edget> edges;
  grapht(typet t)
  {
    witness_type = t;
    create_initial_edge();
  }

  void generate_graphml(
    optionst &options,
    const std::string &output_path_override = "");
  void check_create_new_thread(BigInt thread_id, nodet *prev_node);
};
 
class yamlt
{
public:
  enum typet
  {
    VIOLATION,
    CORRECTNESS
  };
  typet witness_type;
  std::string verified_file;
  std::vector<waypoint> segments;
  std::vector<invariant> invariants;
 
  yamlt(typet t)
  {
    witness_type = t;
  }

  void generate_yaml(
    optionst &options,
    const std::string &output_path_override = "");
};

void create_graphml(xmlnodet &graphml);

void create_violation_graph_node(
  std::string &verifiedfile,
  optionst &options,
  xmlnodet &graphnode);

void create_correctness_graph_node(
  std::string &verifiedfile,
  optionst &options,
  xmlnodet &graphnode);
 
void create_correctness_yaml_emitter(
  std::string &verifiedfile,
  optionst &options,
  YAML::Emitter &root);
 
void create_violation_yaml_emitter(
  std::string &verifiedfile,
  optionst &options,
  YAML::Emitter &root);
 
void create_waypoint(const waypoint &wp, YAML::Emitter &waypoint);

void create_edge_node(edget &edge, xmlnodet &edgenode);

void create_node_node(nodet &node, xmlnodet &nodenode);

bool is_valid_witness_step(const namespacet &ns, const goto_trace_stept &step);

std::string get_formated_assignment(
  const namespacet &ns,
  const goto_trace_stept &step,
  bool yaml);

void check_replace_invalid_assignment(std::string &assignment);
 
bool is_valid_witness_expr(
  const namespacet &ns,
  const irep_container<expr2t> &exp);
 
BigInt get_line_number(
  const std::string &verified_file,
  BigInt relative_line_number,
  optionst &options);
 
int generate_sha256_hash_for_file(const char *path, std::string &output);
 
std::string
get_invariant(std::string verified_file, BigInt line_number, optionst &options);

bool find_nondet_in_expr(const expr2tc &expr);

void generate_testcase_metadata();
void generate_testcase(
  const std::string &file_name,
  const symex_target_equationt &target,
  smt_convt &smt_conv);

struct collected_nondet_value
{
  std::string symbol_name; // e.g., "nondet$symex::nondet3"
  expr2tc symbol_expr;     // The (renamed) symbol2tc as it appears in the SSA
  expr2tc value_expr;      // The concrete value expression
  type2tc type;            // The type
};

std::vector<collected_nondet_value> collect_nondet_values(
  const symex_target_equationt &target,
  smt_convt &smt_conv);

expr2tc make_blocking_expr(const std::vector<collected_nondet_value> &nondets);
 
#endif