Do not evaluate programs on stuck terms (#110)

Modifies our definition so that unapplied literal operators, programs
and oracles are considered "evaluatable".

Modifies the evaluator to not execute programs that have stuck terms.

This leads to better error messages, in particular for users passing
evaluatable functions as higher-order arguments, which is not currently
supported.

After my latest commit on this PR (to undo an oversimplification to the
code), I have verified that the current signature in cvc5 is not
impacted by this change.

NEWS.md

@@ -3,6 +3,8 @@ This file contains a summary of important user-visible changes.
 ethos 0.1.2 prerelease
 ======================
 
+- Change the execution semantics when a program takes an unevalated term as an argument. In particular, we do not call user provided programs and oracles when at least argument could not be evaluated. This change was made to make errors more intuitive. Note this changes the semantics of programs that previously relied on being called on unevaluated terms.
+- User programs, user oracles, and builtin operators that are unapplied are now considered unevaluated. This makes the type checker more strict and disallows passing them as arguments to other programs, which previously led to undefined behavior.
 - Adds support for the SMT-LIB `as` annotations for ambiguous datatype constructors, i.e. those whose return type cannot be inferred from its argument types. Following SMT-LIB convention, ambiguous datatype constructors are expected to be annotated with their *return* type using `as`, which internally is treated as a type argument to the constructor.
 - The semantics for `eo::dt_constructors` is extended for instantiated parametric datatypes. For example calling `eo::dt_constructors` on `(List Int)` returns the list containing `cons` and `(as nil (List Int))`.
 - The semantics for `eo::dt_selectors` is extended for annotated constructors. For example calling `eo::dt_selectors` on `(as nil (List Int))` returns the empty list.

src/cmd_parser.cpp

@@ -748,7 +748,8 @@ bool CmdParser::parseNextCommand()
           Expr rhs = p[1];
           d_eparser.ensureBound(rhs, bvs);
           // TODO: allow variable or default case?
-          for (size_t i = 0, nchildren = pc.getNumChildren(); i < nchildren; i++)
+          for (size_t i = 1, nchildren = pc.getNumChildren(); i < nchildren;
+               i++)
           {
             Expr ecc = pc[i];
             if (ecc.isEvaluatable())

src/expr.cpp

@@ -67,8 +67,9 @@ void ExprValue::computeFlags()
     std::vector<ExprValue*>& children = cur->d_children;
     if (children.empty())
     {
+      bool isEval = (ck == Kind::PROGRAM_CONST || ck == Kind::ORACLE);
       bool isNonGround = (ck==Kind::PARAM);
-      cur->setFlag(Flag::IS_EVAL, false);
+      cur->setFlag(Flag::IS_EVAL, isEval);
       cur->setFlag(Flag::IS_NON_GROUND, isNonGround);
       visit.pop_back();
     }
@@ -86,34 +87,15 @@ void ExprValue::computeFlags()
     else
     {
       visit.pop_back();
-      if (ck==Kind::APPLY)
+      if (isLiteralOp(ck))
       {
-        Kind cck = children[0]->getKind();
-        if (cck==Kind::PROGRAM_CONST || cck==Kind::ORACLE)
-        {
-          cur->setFlag(Flag::IS_PROG_EVAL, true);
-          cur->setFlag(Flag::IS_EVAL, true);
-        }
-      }
-      else if (isLiteralOp(ck))
-      {
-        // requires type and literal operator kinds evaluate
+        // literal operator kinds are evaluatable
         cur->setFlag(Flag::IS_EVAL, true);
       }
+      // flags are a union of the flags of the children
       for (ExprValue* c : children)
       {
-        if (c->getFlag(Flag::IS_NON_GROUND))
-        {
-          cur->setFlag(Flag::IS_NON_GROUND, true);
-        }
-        if (c->getFlag(Flag::IS_EVAL))
-        {
-          cur->setFlag(Flag::IS_EVAL, true);
-        }
-        if (c->getFlag(Flag::IS_PROG_EVAL))
-        {
-          cur->setFlag(Flag::IS_PROG_EVAL, true);
-        }
+        cur->d_flags |= static_cast<uint8_t>(c->d_flags);
       }
     }
   }
@@ -131,18 +113,6 @@ bool ExprValue::isGround()
   return !getFlag(ExprValue::Flag::IS_NON_GROUND);
 }
 
-bool ExprValue::isProgEvaluatable()
-{
-  computeFlags();
-  return getFlag(ExprValue::Flag::IS_PROG_EVAL);
-}
-
-bool ExprValue::isCompiled()
-{
-  // this is set manually
-  return getFlag(ExprValue::Flag::IS_COMPILED);
-}
-
 void ExprValue::dec()
 {
   d_rc--;
@@ -188,12 +158,6 @@ Expr::~Expr()
 bool Expr::isNull() const { return d_value->isNull(); }
 bool Expr::isEvaluatable() const { return d_value->isEvaluatable(); }
 bool Expr::isGround() const { return d_value->isGround(); }
-bool Expr::isProgEvaluatable() const { return d_value->isProgEvaluatable(); }
-bool Expr::isCompiled() const { return d_value->isCompiled(); }
-void Expr::setCompiled()
-{
-  return d_value->setFlag(ExprValue::Flag::IS_COMPILED, true);
-}
 std::string Expr::getSymbol() const
 {
   const Literal * l = d_value->asLiteral();

src/expr.h

@@ -57,24 +57,28 @@ class ExprValue
   bool isEvaluatable();
   /** Has variable */
   bool isGround();
-  /** Has program variable */
-  bool isProgEvaluatable();
-  /** Is part of compiled code */
-  bool isCompiled();
  protected:
   /** The kind */
   Kind d_kind;
   /** The children of this expression */
   std::vector<ExprValue*> d_children;
-  /** flags */
+  /**
+   * Flags, indicating properties of the term.
+   */
   enum class Flag
   {
     NONE = 0,
+    /** Have we computed the flags for this term? */
     IS_FLAGS_COMPUTED = (1 << 0),
+    /**
+     * Is the term "evaluatable", i.e. contains a literal op, program or oracle
+     * as a subterm?
+     */
     IS_EVAL = (1 << 1),
-    IS_PROG_EVAL = (1 << 2),
-    IS_NON_GROUND = (1 << 3),
-    IS_COMPILED = (1 << 4)
+    /**
+     * Is the term non-ground, i.e. contains a parameter as a subterm?
+     */
+    IS_NON_GROUND = (1 << 2),
   };
   char d_flags;
   /** */
@@ -147,12 +151,6 @@ class Expr
   bool isEvaluatable() const;
   /** Has variable */
   bool isGround() const;
-  /** Has program variable */
-  bool isProgEvaluatable() const;
-  /** Is part of compiled code */
-  bool isCompiled() const;
-  /** Set compiled */
-  void setCompiled();
   /** Get symbol */
   std::string getSymbol() const;
   /** Get underlying value */

src/type_checker.cpp

@@ -934,13 +934,24 @@ Expr TypeChecker::evaluateProgramInternal(
         if (nargs != hchildren.size())
         {
           // TODO: catch this during weak type checking of program bodies
-          Warning() << "*** Bad number of arguments provided in function call to " << hd << std::endl;
+          Warning() << "*** Bad number of arguments provided in function call to " << Expr(hd) << std::endl;
           Warning() << "  Arguments: " << children << std::endl;
           return d_null;
         }
         bool matchSuccess = true;
         for (size_t i=1; i<nargs; i++)
         {
+          // Note we abort here, which changed in Ethos versions >=0.1.2.
+          // The motivation is to disallow unintuitive behaviors of Ethos,
+          // which includes:
+          // - Passing (unapplied) user programs, user oracles or builtin
+          // operators, which we do not support in this current version.
+          // - Passing stuck terms, where we chose to propagate the failure,
+          // e.g. (<program> t) is also stuck if t is stuck.
+          if (children[i]->isEvaluatable())
+          {
+            return d_null;
+          }
           if (!match(hchildren[i], children[i], newCtx))
           {
             matchSuccess = false;

tests/CMakeLists.txt

@@ -133,6 +133,8 @@ set(ethos_test_file_list
     simul-overload.eo
     bang-lex.eo
     segfault-98.eo
+    eo-add-non-first-class.eo
+    unstuck-eval-bv-example.eo
     param-dt-parse.eo
     param-dt-parse-amb-fun.eo
     datatypes-split-rule-param.eo

tests/Strings-programs.eo

@@ -84,10 +84,10 @@
 (define string_rev ((U Type) (rev Bool) (t (Seq U))) (eo::ite rev ($string_rev t) t))
 
 ; Returns true if the length of s evaluates to one, false otherwise.
-(define check_length_one ((s String)) (check_true (eo::is_eq (eo::len s) 1)))
+(define check_length_one ((s String)) (eo::is_eq (eo::len s) 1))
 
 ; Returns true if the length of s evaluates to greater than one, false otherwise.
-(define check_length_gt_one ((s String)) (check_true (eo::is_neg (eo::add 1 (eo::neg (eo::len s))))))
+(define check_length_gt_one ((s String)) (eo::is_eq (eo::is_neg (eo::add 1 (eo::neg (eo::len s)))) true))
 
 ; Flatten constants in str.++ application s. Notice that the rewritten form
 ; of strings in cvc5 are such that constants are grouped into constants of

tests/eo-add-non-first-class.eo

@@ -0,0 +1,34 @@
+(declare-type Int ())
+(declare-consts <numeral> Int)
+
+(declare-const g (-> Int Int Int))
+
+(program dummy ((f (-> Int Int Int)) (n1 Int) (n2 Int))
+    (Int Int (-> Int Int Int)) Int
+
+    (((dummy n1 n2 f) (f n1 n2)))
+)
+
+; this should work
+(define tmp1 () (dummy 1 1 g))
+(declare-const c1 (eo::requires tmp1 (g 1 1) Int))
+(define test1 () c1 :type Int)
+
+
+(program foo ((n1 Int) (n2 Int))
+    (Int Int) Int
+
+    (((foo n1 n2) n1))
+)
+
+
+; this should not work
+;(define tmp2 () (dummy 1 1 foo))
+;(declare-const c2 (eo::requires tmp2 1 Int))
+;(define test1 () c2 :type Int)
+
+
+; this should not work
+;(define tmp3 () (dummy 1 1 eo::add))
+;(declare-const c3 (eo::requires tmp3 2 Int))
+;(define test2 () c3 :type Int)

tests/unstuck-eval-bv-example.eo

@@ -0,0 +1,52 @@
+; ethos gave a spurious error on this example in cvc5 regressions when the
+; definition of evaluatable was oversimplified to not check literalOp kinds.
+
+(declare-type Int ())
+(declare-consts <numeral> Int)
+
+(declare-const = (-> (! Type :var A :implicit) A A Bool))
+(declare-const < (-> Int Int Bool))
+(declare-const - (-> Int Int Int))
+
+; note: We do not currently check that the index of this sort is positive.
+(declare-const BitVec (-> Int Type))
+(declare-consts <binary> (BitVec (eo::len eo::self)))
+
+; bvsize
+(declare-const @bvsize (-> (! Int :var m :implicit) (BitVec m) Int))
+
+; define: @bv_empty
+; return: The empty bitvector.
+(define @bv_empty () (eo::to_bin 0 0))
+
+(declare-const concat (->
+  (! Int :var n :implicit)
+  (! Int :var m :implicit)
+  (BitVec n)
+  (BitVec m)
+  (BitVec (eo::add n m))) :right-assoc-nil @bv_empty
+)
+
+(declare-const extract (->
+  (! Int :var n :implicit)
+  (! Int :var h)
+  (! Int :var l)
+  (BitVec n)
+  (BitVec (eo::add h (eo::neg l) 1))
+  )
+)
+(declare-rule bv-extract-concat-4 ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (xs1 (BitVec @n2) :list) (i1 Int) (j1 Int))
+  :premises ((= (< j1 (- (@bvsize (concat x1 xs1 y1)) (@bvsize x1))) true))
+  :args (x1 y1 xs1 i1 j1)
+  :conclusion (= (extract j1 i1 (concat x1 xs1 y1)) (extract j1 i1 (concat xs1 y1)))
+)
+
+(declare-const a (_ BitVec 4))
+(declare-const b (_ BitVec 4))
+(declare-const c (_ BitVec 4))
+(declare-const d (_ BitVec 4))
+
+(assume @p30210 (= (< 2 (- (@bvsize (concat a b c d)) (@bvsize a))) true))
+(step @p30211 :rule bv-extract-concat-4 :premises (@p30210) :args (a d (concat b c) 0 2))
+
+

user_manual.md

@@ -1491,6 +1491,10 @@ If no such term can be found, then the application does not evaluate.
 > __Note:__ If a case is provided `(si ri)` in the definition of program `f` where `si` is not an application of `f`, an error is thrown.
 Furthermore, if `si` contains any computational operators (i.e. those with `eo::` prefix), then an error is thrown.
 
+> __Note:__ Programs are *not* invoked on terms that fail to evaluate. For example, if a function `f : Int -> Int` is applied to `(eo::add "A" "B")`, we return `(f (eo::add "A" "B"))`.
+
+> __Note:__ Programs are *not* invoked when applied to other programs in this version of Ethos. For example, the application of a program `f : (Int -> Int) -> Int` to another user defined program `g : Int -> Int` will be unevaluated, i.e. `(f g)`. Similarly, programs are not invoked when applied to builtin operators `eo::` and oracle functions. In contrast, `f` is invoked when `g` is an ordinary term e.g. one defined by `declare-const`.
+
 ### Example: Finding a child in an `or` term
 
 The following program (recursively) computes whether a formula `l` is contained as the direct child of an application of `or`: