An if-then-else checked against an expected type is never compared with it: ill-typed properties and constants are accepted

[daniel-larraz]

When an if-then-else is checked against a known type, the type checker never compares the branches with that type. As a result, an if-then-else of the wrong type is accepted in a property, a contract, or a typed constant. Depending on where it appears, it is then silently accepted, it fails in the SMT solver, it fails with an internal error, or it leads to contradictory properties both being reported valid. Observed on main at 4549b45 (Report a bad set element or map key instead of crashing (#1457)).

Contradictory properties both reported valid

const k: int = if true then 1.5 else 2.5;
node N() returns (y: int);
let
  y = k;
  check "y = 1" y = 1;
  check "y = 2" y = 2;
tel

<Success> Property y = 2 is valid by property directed reachability (IA) after 0.014s.
<Success> Property y = 1 is valid by inductive step after 0.014s.

The assumptions are not simply inconsistent: check false in the same node is correctly reported falsified at k=0. Without the if-then-else, const k: int = 1.5; is rejected with Cannot unify type int with inferred type real.

Other symptoms

A bool property whose branches are integers passes type checking and fails in the solver:

node N(c: bool) returns (y: int);
let
  y = 0;
  check if c then 1 else 2;
tel

<Error> Runtime failure in inductive step: SMT solver failed: "line 25 column 33: Sort mismatch at argument #2 for function (declare-fun => (Bool Bool) Bool) supplied sort is Int"

The same happens for guarantee if c then 1 else 0; in a contract, and for a const k: bool = if true then 1 else 2; used in check k;. If k is never used, the program is accepted without any error.

Using the int constant above in an expression, y = x + k, fails with an internal error instead:

<Error> Error opening input file 'vacuous_input.lus': LustreExpr.Type_mismatch

Cause

In check_type_expr (src/lustre/lustreTypeChecker.ml), the TernaryOp arm checks that the condition is bool and that the two branches have the same type. It never compares that type with exp_ty:

| LA.TernaryOp (pos, ite, con, e1, e2) ->
  let* ty, con, warnings1 = infer_type_expr ctx nname con in (
  match ty with
      | Bool _ ->
        let* ty1, e1, warnings2 = infer_type_expr ctx nname e1 in
        let* ty2, e2, warnings3 = infer_type_expr ctx nname e2 in
        R.ifM (eq_lustre_type ctx ty1 ty2)
          (R.ok (LA.TernaryOp (pos, ite, con, e1, e2), (warnings1 @ warnings2 @ warnings3)))
          (type_error pos (UnificationFailed (ty1, ty2)))
      | ty  -> type_error pos (ExpectedType ((Bool pos), ty))
  )

Every other arm of check_type_expr ends with a comparison against exp_ty. check_type_expr is used where the expected type is known from context: properties and contract items (bool), typed constants, and the arguments of some constructs. An equation such as x = if c then 1 else 2 goes through infer_type_expr and the check on the left-hand side, so it is not affected.

Suggested fix

Compare the branch type with exp_ty, as the other arms do. Either check each branch with check_type_expr ... exp_ty, or add an eq_lustre_type ctx ty1 exp_ty guard that reports UnificationFailed (exp_ty, ty1). The first also gives each branch its own error position.