sc_manual.h

Go to the documentation of this file.

#ifndef ILANG_MCM_SC_MANUAL_H__
#define ILANG_MCM_SC_MANUAL_H__

#include <ilang/mcm/inter_ila_unroller.h>
#include <ilang/mcm/memory_model.h>

namespace ilang {

class ScTraceStep : public TraceStep {
public:
  typedef std::shared_ptr<TraceStep> TraceStepPtr;
  // ------------------------- MEMBERS -------------------------------------- //
  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
  ScTraceStep(const InstrPtr& inst, ZExprVec& cstr, z3::context& ctx,
              size_t pos);
}; // class ScTraceStep

class Sc : public MemoryModel {
public:
  typedef std::shared_ptr<ScTraceStep> ScTraceStepPtr;
  typedef std::set<ScTraceStepPtr> ScTraceStepPtrSet;
  // -------------------------- TSO SELECTOR
  // -------------------------------------- //
  static InterIlaUnroller::MemoryModelCreator ScModel;

protected:
  TraceStepPtrSet WRITE_list;
  TraceStepPtrSet READ_list;

public:
  void virtual RegisterSteps(size_t regIdx, const InstrVec& _inst_seq) override;
  void virtual FinishRegisterSteps() override;
  void virtual ApplyAxioms() override;
  // HZ note: All the step should be registered through the first function:
  // RegisterSteps
  void virtual SetFinalProperty(const ExprPtr& property) override;
  Sc(z3::context& ctx, ZExprVec& _cstrlist, const StateNameSet& shared_states,
     const ILANameStateNameSetMap& private_states,
     const InstrLvlAbsPtr& global_ila_ptr)
      : MemoryModel(ctx, _cstrlist, shared_states, private_states,
                    global_ila_ptr) {}

private:
  z3::expr RF(const TraceStepPtr& w, const TraceStepPtr& r);
  z3::expr FR(const TraceStepPtr& r, const TraceStepPtr& w);
  z3::expr CO(const TraceStepPtr& w1, const TraceStepPtr& w2);

}; // class Sc

} // namespace ilang

#endif // ILANG_MCM_SC_MANUAL_H__