Fix #382

[delcypher]

Fix #382

There are numerous changes here which removes the assumption that
STP is the core solver.

• -write-cvcs has been renamed to -write-core-solver-queries
• LogType::STP has been renamed to LogType::CORE_SOLVER_LANG
• Interpreter::getConstraintLog() and Executor::getConstraintLog()
  now have a fileExtension parameter which returns the file extension
  for constraint language requested.
• The Solver::getConstraintLog() and SolverImpl::getConstraintLog()
  methods (and all their descendants) now have a fileExtension
  parameter which will be set (if requested by the client) to the file
  extension for the core solver's constraint language.

[andreamattavelli]

@delcypher metaSTM is going to give you a lot of fun.

[ccadar]

We really need to think whether such a change is worth it, as many things would become more confusing. The assumption that STP is the core solver is not that terrible in my opinion, even though other solvers are equally supported directly or via metaSMT.

[delcypher]

@ccadar

We really need to think whether such a change is worth it, as many things would become more confusing.

Can you be more concrete? I can't think of anything that is made more confusing by this change. If anything this greatly improves things because STP being the core solver is not true anymore.
In fact I don't even use STP anymore. My work needs floating point constraint solving support which STP will likely never have given that it isn't being actively developed anymore.

The cost is having to make the API change but if KLEE is to make progress as a project we should not be resisting sensible API changes. This PR doesn't change anything related to LLVM versions so it should not conflict with the outstanding PRs that add support for newer LLVM versions (I consider these to be important PRs that we should try to avoid conflicting with).
I should note though I'm not sure if the API change I've made is the best design and I'm happy to debate that.

The assumption that STP is the core solver is not that terrible in my opinion, even though other solvers are equally supported directly or via metaSMT.

I really don't like this assumption because it makes things confusing when STP is not the core example. For example when using Z3 as the core solver the -write-cvcs option is confusing because the outputted file will actually be SMT-LIBv2 not CVC.

[ccadar]

What I mean is that there are other ways to solve this, which would not break backward-compatibility unnecessarily, and might be in fact easier to use. For instance, we could only enable write-cvcs when STP/CVC4/etc. are used and add similar options for other solvers. Given that the number of solvers will always be quite small, this might be preferable. Note that the generic --write-core-solver-queries would have the same problem, as one would need to specify and understand what files are generated for each solver, which I find more confusing. In any case, the right way with such API changes is to first discuss them, rather than write code.

[delcypher]

What I mean is that there are other ways to solve this, which would not break backward-compatibility unnecessarily, and might be in fact easier to use.

For instance, we could only enable write-cvcs when STP/CVC4/etc. are used and add similar options for other solvers.

That isn't a great solution. We don't know what the core solver will be until runtime which means we will be showing -write-cvcs in the output of -help even though it might not actually work. Sure we could provide an error if someone tries to use it in the wrong situation but I favour just having a general option.

In the case of Z3 as the core solver the existing -write-smt2s would become ambiguous. Does it mean log the core solver's format or use the ExprSMTLIBPrinter ?

This solution also requires that the Exectuor know about the internal details of the core solver which is an unnecessary coupling in my opinion.

Given that the number of solvers will always be quite small, this might be preferable. Note that the generic --write-core-solver-queries would have the same problem, as one would need to specify and understand what files are generated for each solver, which I find more confusing. In any case, the right way with such API changes is to first discuss them, rather than write code.

I don't think it's particularly confusing. For each test case we get a file called testXXXXX.core_solver.??? where ??? is the file extension appropriate for the core solver's language. It's easy to see which files are for the core solver and the file extension tells you what the language is.

[ccadar]

I'm still not convinced that this is worth breaking the API. The -help text can just explain when each option is applicable, that's what it's for. The different ways to print Z3 constraints are certainly confusing if they're using the same SMTLibv2 format, so having a more descriptive option would actually make things clear to the user.

Finally, the notion of core solver is blurred when a portfolio of solvers is used (something almost supported via metaSMT), which is another argument against this change.

I find your proposed API reasonable, but I see both pros and cons when compared to the existing API, in which case I'd prefer to preserve backward compatibility.

[delcypher]

I'm still not convinced that this is worth breaking the API.

We have already broken KLEE's API. My fork of KLEE is only a few months away from current master and there were API breaking changes that I had to deal with when writing this PR.

I find your proposed API reasonable, but I see both pros and cons when compared to the existing API, in which case I'd prefer to preserve backward compatibility.

Who are we preserving backward compatibility for? If it's for unmaintained forks then I'd argue we shouldn't be maintaining backward compatibility for them.

[delcypher]

Just note having played with this a bit, the API isn't that great. In my fork I hit a scenario where I needed to the file extension for the core solver's native language without actually needing the printed constraints. The current API forces me to do this.

    // FIXME: Kind of gross. Should probably have method on solver
    // that just gives us the file extension.
    // Create dummy query to determine file extension
    const char* fileExtension = NULL;
    ConstraintManager cm;
    Query q(cm, ConstantExpr::alloc(0, Expr::Bool));
    char* dummy = solver->getConstraintLog(q, &fileExtension);
    free(dummy);

[delcypher]

@ccadar

Finally, the notion of core solver is blurred when a portfolio of solvers is used (something almost supported via metaSMT), which is another argument against this change.

That is true but this not something supported in the code today. In fact getConstraintLog() doesn't do anything useful when metaSMT is the core solver. This would require an API change. An API to query what constraint languages the core solver supports and then an additional parameter to getConstraintLog() to say what format is required.

[delcypher]

I should also note a motivation behind this work is to extend the -use-query-log= option so we can log constraints in the core solver's query language just like we can do with the KQueryLoggingSolver and the SMTLIBLoggingSolver. I have this working in my fork with a CoreSolverLangLoggingSolver that I have added that calls getConstraingLog() to log queries.

[delcypher]

Update on how the API is progressing in my fork. This is what I'm currently using in my fork.

    /// getConstraintLog - Get constraints in the solver's native query
    /// language.
    ///
    /// \param query - The Query to output
    /// \param fileExtension - If not set to NULL the passed in pointer is
    ///                        modified to point to a C string containing the
    ///                        file extension appropriate for the constraints.
    /// \param ConstraintLogConfig - if not set to NULL sets options
    ///                        for constraint logging.
    /// \return Constraints in the solver's native query language.
    ///         Clients must free this.
    virtual char *getConstraintLog(const Query &query,
                                   const char **fileExtension = NULL,
                                   const ConstraintLogConfig * = NULL);

and ConstraintLogConfig currently looks like this. It implements LLVM style RTTI so that solvers can do dyn_cast<>() on pointers to it. This design would probably be beneficial for metaSMT because it means we can pass logging config options specific to metaSMT through the solver chain if we wanted to. I'm using it to pass through options specific to Z3 here.

//===-- ConstraintLogConfig.h -----------------------------------*- C++ -*-===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#ifndef CONSTRAINT_LOG_CONFIG_H
#define CONSTRAINT_LOG_CONFIG_H
#include "klee/Config/config.h"
#include "llvm/Support/Casting.h"

namespace klee {

class ConstraintLogConfig {
public:
  enum ConstraintLogConfigKind { CLCK_Z3 };

private:
  const ConstraintLogConfigKind kind;

public:
  ConstraintLogConfigKind getKind() const { return kind; }
  // Allocate memory for a copy of this configuration.
  // Clients must free using `delete`.
  virtual ConstraintLogConfig *alloc() const = 0;
  virtual ~ConstraintLogConfig() {}

protected:
  ConstraintLogConfig(ConstraintLogConfigKind k) : kind(k) {}
};

class Z3ConstraintLogConfig : public ConstraintLogConfig {
public:
  // Configuration settings
  bool ackermannizeArrays;

  Z3ConstraintLogConfig()
      : ConstraintLogConfig(CLCK_Z3), ackermannizeArrays(false) {}
  static bool classof(const ConstraintLogConfig *clc) {
    return clc->getKind() == CLCK_Z3;
  }

  virtual ConstraintLogConfig *alloc() const {
    ConstraintLogConfig *clc = new Z3ConstraintLogConfig(*this);
    return clc;
  }
};
}

#endif /* CONSTRAINT_LOG_CONFIG_H */

[delcypher]

@ccadar Have you had a chance to think about this some more?

After using it for a while I've come to the conclusion that having a ConstraintLogConfig is a good idea (not necessarily with API used above). I used this in my own fork to have fine grained control over how Z3 writes its constraints. In the public version of KLEE one thing this could be used for is telling Z3 whether or not to simplify constraints before logging.

For metaSMT this would also be useful if it ever supported logging because the options could be used to control any aspect of its logging facility.

I'm not so sure about the fileExtension argument. I feel that either needs to be generalised to a data structure that the core solver can give back to clients that can detail anything about the query (e.g. what logic it is using) or change the return type of getConstraintLog() to return an object that

• contains the query string and does reference counting on it
• contains the file extension associated with the query

[ccadar]

Hi Dan, your recent comments about getConstraintLog are orthogonal to our early discussion in this PR, as you could use the enhanced getConstraintLog API regardless of whether we have the notion of core solver or not. I would be happy to evolve the API of getConstraintLog as you suggest, if you find it useful. But how configurable are solvers with respect to logging?

[delcypher]

Hi Dan, your recent comments about getConstraintLog are orthogonal to our early discussion in this PR, as you could use the enhanced getConstraintLog API regardless of whether we have the notion of core solver or not.

They are orthogonal in concept but not in implementation. Both require changing the getConstraintLog() API which is why I brought this up. Your objection seemed to be focused on not wanting to change the API which I don't agree with.

They are also related because a ConstraintLogConfig option could potentially change the file extension if the core solver supports multiple formats.

I would be happy to evolve the API of getConstraintLog as you suggest, if you find it useful. But how configurable are solvers with respect to logging?

Z3 has a very powerful API so there are many things that could be done to the expressions before printing. The use case I imagine is an option to control if simplification of expressions is done before printing this can be done with Z3 but STP also supports this (see vc_printQueryStateToBuffer()) but is not currently done in KLEE.

[ccadar]

Since this PR is over 3 years old and it's resolution is unclear, I'll close this.