verification_result.cpp

// Copyright (c) 2023 Fotis Koutoulakis for Diffblue Ltd.

/// \file
/// Interface for the various verification engines providing results
//  in a structured form.

#include "verification_result.h"

#include <util/exit_codes.h>
#include <util/invariant.h>

#include <goto-checker/properties.h>

#include <algorithm>
#include <string>
#include <vector>

class verification_resultt::verification_result_implt
{
  propertiest _properties;
  resultt _verifier_result;

public:
  verification_result_implt() = default;
  verification_result_implt(const verification_result_implt &other) = default;
  ~verification_result_implt() = default;

  void set_properties(propertiest &properties);
  void set_result(resultt &verification_result);

  resultt get_result();
  const propertiest &get_properties();
};

// Impl

void verification_resultt::verification_result_implt::set_properties(
  propertiest &properties)
{
  _properties = properties;
}

void verification_resultt::verification_result_implt::set_result(
  resultt &result)
{
  _verifier_result = result;
}

resultt verification_resultt::verification_result_implt::get_result()
{
  return _verifier_result;
}

const propertiest &
verification_resultt::verification_result_implt::get_properties()
{
  return _properties;
}

// Verification_result

verification_resultt::verification_resultt()
  : _impl(std::make_unique<verification_resultt::verification_result_implt>())
{
}

verification_resultt::~verification_resultt()
{
}

verification_resultt::verification_resultt(const verification_resultt &other)
  : _impl(std::make_unique<verification_result_implt>(*other._impl))
{
}

verification_resultt &
verification_resultt::operator=(verification_resultt &&) = default;
verification_resultt &
verification_resultt::operator=(const verification_resultt &other)
{
  *_impl = *other._impl;
  return *this;
}

void verification_resultt::set_properties(propertiest &properties)
{
  _impl->set_properties(properties);
}

void verification_resultt::set_result(resultt &result)
{
  _impl->set_result(result);
}

verifier_resultt verification_resultt::final_result() const
{
  switch(_impl->get_result())
  {
  case resultt::ERROR:
    return verifier_resultt::ERROR;
  case resultt::FAIL:
    return verifier_resultt::FAIL;
  case resultt::PASS:
    return verifier_resultt::PASS;
  case resultt::UNKNOWN:
    return verifier_resultt::UNKNOWN;
  }
  // Required to silence compiler warnings that are promoted as errors!
  UNREACHABLE;
}

std::vector<std::string> verification_resultt::get_property_ids() const
{
  std::vector<std::string> result;
  for(const auto &props : _impl->get_properties())
  {
    result.push_back(id2string(props.first));
  }
  return result;
}

std::string verification_resultt::get_property_description(
  const std::string &property_id) const
{
  auto irepidt_property = irep_idt(property_id);
  const auto description =
    _impl->get_properties().at(irepidt_property).description;
  return description;
}

prop_statust
verification_resultt::get_property_status(const std::string &property_id) const
{
  auto irepidt_property = irep_idt(property_id);
  switch(_impl->get_properties().at(irepidt_property).status)
  {
  case property_statust::ERROR:
    return prop_statust::ERROR;
  case property_statust::FAIL:
    return prop_statust::FAIL;
  case property_statust::NOT_CHECKED:
    return prop_statust::NOT_CHECKED;
  case property_statust::NOT_REACHABLE:
    return prop_statust::NOT_REACHABLE;
  case property_statust::PASS:
    return prop_statust::PASS;
  case property_statust::UNKNOWN:
    return prop_statust::UNKNOWN;
  }
  UNREACHABLE;
}

// FOTIS' note: Modelled after `result_to_exit_code` in
// `src/goto-checker/properties.cpp`.
int verifier_result_to_exit_code(verifier_resultt result)
{
  switch(result)
  {
  case verifier_resultt::PASS:
    return CPROVER_EXIT_VERIFICATION_SAFE;
  case verifier_resultt::FAIL:
    return CPROVER_EXIT_VERIFICATION_UNSAFE;
  case verifier_resultt::ERROR:
    return CPROVER_EXIT_INTERNAL_ERROR;
  case verifier_resultt::UNKNOWN:
    return CPROVER_EXIT_VERIFICATION_INCONCLUSIVE;
  }
  UNREACHABLE;
}