cbmc/src/goto-checker/single_path_symex_only_checker.h at 059fe90cb960248a1cb236697377fbedb0f50f47 · diffblue/cbmc · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
/*******************************************************************\

Module: Goto Checker using Single Path Symbolic Execution only

Author: Daniel Kroening, Peter Schrammel

\*******************************************************************/

/// \file
/// Goto Checker using Single Path Symbolic Execution only

#ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
#define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H

#include <goto-programs/unwindset.h>

#include <goto-symex/path_storage.h>

#include "incremental_goto_checker.h"

#include <chrono> // IWYU pragma: keep

class symex_bmct;

/// Uses goto-symex to generate a `symex_target_equationt` for each path.
class single_path_symex_only_checkert : public incremental_goto_checkert
{
public:
  single_path_symex_only_checkert(
    const optionst &options,
    ui_message_handlert &ui_message_handler,
    abstract_goto_modelt &goto_model);

  resultt operator()(propertiest &) override;

  virtual ~single_path_symex_only_checkert() = default;

protected:
  abstract_goto_modelt &goto_model;
  symbol_tablet symex_symbol_table;
  namespacet ns;
  guard_managert guard_manager;
  std::unique_ptr<path_storaget> worklist;
  std::chrono::duration<double> symex_runtime;
  unwindsett unwindset;

  void equation_output(
    const symex_bmct &symex,
    const symex_target_equationt &equation);

  virtual void setup_symex(symex_bmct &symex);

  /// Adds the initial goto-symex state as a path to the worklist
  virtual void initialize_worklist();

  /// Continues exploring the given \p path using goto-symex
  /// \return whether the path is ready to be checked
  virtual bool resume_path(path_storaget::patht &path);

  /// Returns whether the given \p path produced by \p symex is ready to be
  /// checked
  virtual bool
  is_ready_to_decide(const symex_bmct &symex, const path_storaget::patht &path);

  /// Returns whether we should stop exploring paths
  virtual bool has_finished_exploration(const propertiest &);

  /// Updates the \p properties from the \p equation and
  /// adds their property IDs to \p updated_properties.
  virtual void update_properties(
    propertiest &properties,
    std::unordered_set<irep_idt> &updated_properties,
    const symex_target_equationt &equation);

  /// Updates the \p properties after having finished exploration and
  /// adds their property IDs to \p updated_properties.
  virtual void final_update_properties(
    propertiest &properties,
    std::unordered_set<irep_idt> &updated_properties);
};

#endif // CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H