// Metaprogram's revision differentiator structure
// Copyright 2023  Nguyễn Gia Phong
//
// This file is distributed under the University of Illinois
// Open Source License.  See LICENSE.TXT for details.

#ifndef KLEE_DIFFERENTIATOR_H
#define KLEE_DIFFERENTIATOR_H

#include "ExecutionState.h"

#include "klee/Expr/ArrayCache.h"
#include "klee/Expr/Expr.h"
#include "klee/Expr/ExprVisitor.h"
#include "klee/System/Time.h"

#include <cstdint>
#include <map>
#include <set>
#include <string>

namespace klee {

struct ExprCmbnVisitor : ExprVisitor {
  ExprCmbnVisitor(char, ArrayCache&);
  Action visitExprPost(const Expr& e) override;

  /// Recorded output variables
  std::map<std::string, std::map<ref<Expr>, ref<ReadExpr>>> outVars;
private:
  char revision;
  ArrayCache& arrayCache;
};

struct Differentiator {
  /// Buffer of bytes
  typedef std::vector<unsigned char> Bytes;
  /// argv stdin
  typedef std::pair<std::vector<Bytes>, Bytes> TestInps;
  /// :rev (:var val) stdout
  typedef std::map<std::uint64_t,
                   std::pair<std::map<std::string, Bytes>,
                             Bytes>>
          TestOuts;
  typedef std::map<Bytes, std::set<std::uint64_t>> Clusters;

  /// Extract revision number from given condition if any
  static std::pair<bool, std::uint64_t> extractPatchNumber(ref<Expr> e);

  Differentiator(std::unique_ptr<TimingSolver>*, time::Span&, ArrayCache&);
  /// Extract differential test from concrete execution
  void extract(ExecutionState*, ExecutionState*,
               const std::vector<const Array*>&,
               const std::vector<Bytes>&);
  /// Compare with other exit states for possible differential tests
  void search(ExecutionState*);
  /// Log patch differentiation result
  void log();

  /// Program revision numbers
  std::set<std::uint64_t> revisions;
  /// Differentiated pairs
  std::map<std::pair<std::uint64_t, std::uint64_t>, TestOuts*> done;
private:
  /// Program path for concrete execution.
  const char* prog;
  /// Exit states
  std::map<std::uint64_t,
           std::set<ExecutionState*,
                    ExecutionStatePathCondCompare>> exits;
  /// Differential tests
  std::map<TestInps, TestOuts> tests;
  /// SMT solver "borrowed" from Executor
  std::unique_ptr<TimingSolver>* solver;
  /// SMT solving timeout
  time::Span solverTimeout;
  /// Symbolic memory array
  ArrayCache& arrayCache;
  /// Symbolic output renamers
  ExprCmbnVisitor visitorA, visitorB;
};

} // namespace klee

#endif // KLEE_DIFFERENTIATOR_H