Valid-binary
Validate a binary expression,
given the type of the sub-expression.
- Signature
(valid-binary expr op type-arg1 type-arg2 ienv)
→
(mv erp type)
- Arguments
- expr — Guard (exprp expr).
- op — Guard (binopp op).
- type-arg1 — Guard (typep type-arg1).
- type-arg2 — Guard (typep type-arg2).
- ienv — Guard (ienvp ienv).
- Returns
- type — Type (typep type).
The * binary and / operators
require arithmetic operands [C17:6.5.5/2].
The result is the common type according to
the usual arithmetic conversions [C17:6.5.5/3].
There is no need for array-to-pointer or function-to-pointer conversions
because those never produce arithmetic types.
The % operator requires integer operands [C17:6.5.5/2].
The result is from the usual arithmetic conversions [C17:6.5.5/3].
No array-to-pointer or function-to-pointer conversions are needed.
The + binary operator requires
either two arithmetic operands
or an integer and a pointer operand
[C17:6.5.6/2].
In the first case, the result is from the usual arithmetic conversions
[C17:6.5.6/4].
In the second case, the result is the pointer type [C17:6.5.6/8].
Because of that second case, which involves pointers,
we perform array-to-pointer conversion.
We do not perform function-to-pointer conversion,
because that would result in a pointer to function,
while a pointer to complete object type is required.
The - binary operator requires
either two arithmetic operands,
or two pointer operands,
or a pointer first operand and an integer second operand
[C17:6.5.6/3].
In the first case, the result is from the usual arithmetic conversions
[C17:6.5.6/4].
In the second case, the result has type ptrdiff_t [C17:6.5.6/9],
which has an implementation-specific definition,
and so we return the unknown type in this case.
In the third case, the result has the pointer type [C17:6.5.6/8].
Because of the second and third cases, which involve pointers,
we perform array-to-pointer conversion.
We do not perform function-to-pointer conversion,
because that would result in a pointer to function,
while a pointer to complete object type is required.
The << and >> operators require integer operands [C17:6.5.7/2].
The type of the result is the type of the promoted left operand
[C17:6.5.7/3].
There is no need for
array-to-pointer or function-to-pointer conversions.
The <, >, <=, and >= operators
require real types or pointer types [C17:6.5.8/2].
The result is always signed int [C17:6.5.8/6].
Since pointers may be involved,
we perform array-to-pointer conversion.
We do not perform function-to-pointer conversion,
because that would result in a pointer to function,
while a pointer to object type is required.
The standard does not allow
a null pointer constants [C17:6.3.2.3/3] without the void * cast
to be used as an operand while the other operand has pointer type.
But we found it accepted by practical compilers,
so it is probably a GCC extensions,
and for this reason we accept it for now;
we should extend our implementation environments with
information about whether GCC extensions are allowed,
and condition acceptance under that flag.
Since we do not have code yet to recognize null pointer constants,
we accept any integer expression;
that is, we allow one pointer operand and one integer operand.
The == and != operators require
arithmetic types or pointer types [C17:6.5.9/2];
Distinctions betwen qualified and unqualified pointer types,
as well as void or non-void pointers types are ignored
since we currently approximate all of these as a single pointer type.
Since we do not yet implement evaluation of constant expressions,
all integer expressions are considered potential null pointer constants:
so we allow an operand to be a pointer and the other to be an integer,
to accommodate a null pointer constant [C17:6.3.2.3/3]
without the void * cast.
The result is always signed int [C17:6.5.9/3].
Since pointers may be involved,
we perform array-to-pointer and function-to-pointer conversions.
The &, ^, and | operators require integer operands
[C17:6.5.10/2] [C17:6.5.11/2] [C17:6.5.12/2].
The result has the type from the usual arithmetic conversions
[C17:6.5.10/3] [C17:6.5.11/3] [C17:6.5.12/3].
No array-to-pointer or function-to-pointer conversion is needed.
The && and || operators require scalar types
[C17:6.5.13/2] [C17:6.5.14/2].
The result has type signed int [C17:6.5.13/3] [C17:6.5.14/3].
Since pointers may be involved, we need to perform
array-to-pointer and function-to-pointer conversions.
The = simple assignment operator requires
an lvalue as left operand [C17:6.5.16/2],
but currently we do not check that.
In our currently approximate type system,
the requirements in [C17:6.5.16.1/1] reduce to the two operands having
both arithmetic types,
or both the structure type,
or both the union type,
or both pointer types,
or one pointer type and one integer type.
We do not perform array-to-pointer or function-to-pointer conversion
on the left operand, because the result would not be an lvalue.
In order to allow a pointer type on the left
and a null pointer constant [C17:6.3.2.3/3] without void * cast
on the right,
since we do not have code to recognize such null pointer constants yet,
we allow any integer expressions on the right
when the expression on the left has pointer type.
We also allow the left operand to be boolean
and the right operand to be a pointer;
although [C17:6.5.9/2] does not mention that,
we found it accepted by practical compiler with a strict C17 option,
and [C17:6.3.1.2/1] mentions a conversion
from scalars (which includes pointer) to booleans,
although it does not say that it happens
(it says ``When any scalar valu is converted to _Bool, ...'').
The type of the result is the type of the left operand [C17:6.5.16/3].
The *= and /= operators require arithmetic operands
[C17:6.5.16.2/2],
and the result has the type of the first operand [C17:6.5.16/3].
No array-to-pointer or function-to-pointer conversions are needed.
The %= operator requires integer operands [C17:6.5.16.2/2],
and the result has the type of the first operand [C17:6.5.16/3].
No array-to-pointer or function-to-pointer conversions are needed.
The += and -= operands require
either arithmetic operands
or a first pointer operand and a second integer operand
[C17:6.5.16.2/1].
The result has the type of the first operand [C17:6.5.16/3].
Since pointers may be involved,
we perform array-to-pointer and function-to-pointer conversions.
The <<=, >>=, &=, ^=, and |= operators
require integer operands [C17:6.5.13.2/2].
The result has the type of the first operand [C17:6.5.13/3].
No array-to-pointer or function-to-pointer conversions are needed.
Definitions and Theorems
Function: valid-binary
(defun valid-binary (expr op type-arg1 type-arg2 ienv)
(declare (xargs :guard (and (exprp expr)
(binopp op)
(typep type-arg1)
(typep type-arg2)
(ienvp ienv))))
(declare (xargs :guard (expr-case expr :binary)))
(let ((__function__ 'valid-binary))
(declare (ignorable __function__))
(b*
(((reterr) (irr-type))
((when (or (type-case type-arg1 :unknown)
(type-case type-arg2 :unknown)))
(retok (type-unknown)))
(msg
(msg
"In the binary expression ~x0, ~
the sub-expressiona have types ~x1 and ~x2."
(expr-fix expr)
(type-fix type-arg1)
(type-fix type-arg2))))
(case (binop-kind op)
((:mul :div)
(b* (((unless (and (type-arithmeticp type-arg1)
(type-arithmeticp type-arg2)))
(reterr msg)))
(retok (type-uaconvert type-arg1 type-arg2 ienv))))
(:rem (b* (((unless (and (type-arithmeticp type-arg1)
(type-arithmeticp type-arg2)))
(reterr msg)))
(retok (type-uaconvert type-arg1 type-arg2 ienv))))
(:add (b* ((type1 (type-apconvert type-arg1))
(type2 (type-apconvert type-arg2)))
(cond ((and (type-arithmeticp type1)
(type-arithmeticp type2))
(retok (type-uaconvert type1 type2 ienv)))
((or (and (type-integerp type1)
(type-case type2 :pointer))
(and (type-case type1 :pointer)
(type-integerp type2)))
(retok (type-pointer)))
(t (reterr msg)))))
(:sub (b* ((type1 (type-apconvert type-arg1))
(type2 (type-apconvert type-arg2)))
(cond ((and (type-arithmeticp type1)
(type-arithmeticp type2))
(retok (type-uaconvert type1 type2 ienv)))
((and (type-case type1 :pointer)
(type-integerp type2))
(retok (type-pointer)))
((and (type-case type1 :pointer)
(type-case type2 :pointer))
(retok (type-unknown)))
(t (reterr msg)))))
((:shl :shr)
(b* (((unless (and (type-integerp type-arg1)
(type-integerp type-arg2)))
(reterr msg)))
(retok (type-promote type-arg1 ienv))))
((:lt :gt :le :ge)
(b* ((type1 (type-apconvert type-arg1))
(type2 (type-apconvert type-arg2))
((unless (or (and (type-realp type1)
(type-realp type2))
(if (type-case type1 :pointer)
(or (type-case type2 :pointer)
(type-integerp type2))
(and (type-integerp type1)
(type-case type2 :pointer)))))
(reterr msg)))
(retok (type-sint))))
((:eq :ne)
(b* ((type1 (type-fpconvert (type-apconvert type-arg1)))
(type2 (type-fpconvert (type-apconvert type-arg2)))
((unless (or (and (type-arithmeticp type1)
(type-arithmeticp type2))
(if (type-case type1 :pointer)
(or (type-case type2 :pointer)
(type-integerp type2))
(and (type-integerp type1)
(type-case type2 :pointer)))))
(reterr msg)))
(retok (type-sint))))
((:bitand :bitxor :bitior)
(b* (((unless (and (type-integerp type-arg1)
(type-integerp type-arg2)))
(reterr msg)))
(retok (type-uaconvert type-arg1 type-arg2 ienv))))
((:logand :logor)
(b* ((type1 (type-fpconvert (type-apconvert type-arg1)))
(type2 (type-fpconvert (type-apconvert type-arg2)))
((unless (and (type-scalarp type1)
(type-scalarp type2)))
(reterr msg)))
(retok (type-sint))))
(:asg (b* ((type1 type-arg1)
(type2 (type-fpconvert (type-apconvert type-arg2)))
((unless (or (and (type-arithmeticp type1)
(type-arithmeticp type2))
(and (type-case type1 :struct)
(type-case type2 :struct))
(and (type-case type1 :union)
(type-case type2 :union))
(and (type-case type1 :bool)
(type-case type2 :pointer))
(and (type-case type1 :pointer)
(or (type-case type2 :pointer)
(type-integerp type2)))))
(reterr msg)))
(retok (type-fix type-arg1))))
((:asg-mul :asg-div)
(b* (((unless (and (type-arithmeticp type-arg1)
(type-arithmeticp type-arg2)))
(reterr msg)))
(retok (type-fix type-arg1))))
(:asg-rem (b* (((unless (and (type-integerp type-arg1)
(type-integerp type-arg2)))
(reterr msg)))
(retok (type-fix type-arg1))))
((:asg-add :asg-sub)
(b* ((type1 (type-fpconvert (type-apconvert type-arg1)))
(type2 (type-fpconvert (type-apconvert type-arg2)))
((unless (or (and (type-arithmeticp type1)
(type-arithmeticp type2))
(and (type-case type1 :pointer)
(type-integerp type2))))
(reterr msg)))
(retok (type-fix type-arg1))))
((:asg-shl :asg-shr :asg-and
:asg-xor :asg-ior)
(b* (((unless (and (type-integerp type-arg1)
(type-integerp type-arg2)))
(reterr msg)))
(retok (type-fix type-arg1))))
(t (prog2$ (impossible) (reterr t)))))))
Theorem: typep-of-valid-binary.type
(defthm typep-of-valid-binary.type
(b* (((mv acl2::?erp ?type)
(valid-binary expr op type-arg1 type-arg2 ienv)))
(typep type))
:rule-classes :rewrite)
Theorem: valid-binary-of-expr-fix-expr
(defthm valid-binary-of-expr-fix-expr
(equal (valid-binary (expr-fix expr)
op type-arg1 type-arg2 ienv)
(valid-binary expr op type-arg1 type-arg2 ienv)))
Theorem: valid-binary-expr-equiv-congruence-on-expr
(defthm valid-binary-expr-equiv-congruence-on-expr
(implies (expr-equiv expr expr-equiv)
(equal (valid-binary expr op type-arg1 type-arg2 ienv)
(valid-binary expr-equiv
op type-arg1 type-arg2 ienv)))
:rule-classes :congruence)
Theorem: valid-binary-of-binop-fix-op
(defthm valid-binary-of-binop-fix-op
(equal (valid-binary expr (binop-fix op)
type-arg1 type-arg2 ienv)
(valid-binary expr op type-arg1 type-arg2 ienv)))
Theorem: valid-binary-binop-equiv-congruence-on-op
(defthm valid-binary-binop-equiv-congruence-on-op
(implies (binop-equiv op op-equiv)
(equal (valid-binary expr op type-arg1 type-arg2 ienv)
(valid-binary expr
op-equiv type-arg1 type-arg2 ienv)))
:rule-classes :congruence)
Theorem: valid-binary-of-type-fix-type-arg1
(defthm valid-binary-of-type-fix-type-arg1
(equal (valid-binary expr op (type-fix type-arg1)
type-arg2 ienv)
(valid-binary expr op type-arg1 type-arg2 ienv)))
Theorem: valid-binary-type-equiv-congruence-on-type-arg1
(defthm valid-binary-type-equiv-congruence-on-type-arg1
(implies (type-equiv type-arg1 type-arg1-equiv)
(equal (valid-binary expr op type-arg1 type-arg2 ienv)
(valid-binary expr
op type-arg1-equiv type-arg2 ienv)))
:rule-classes :congruence)
Theorem: valid-binary-of-type-fix-type-arg2
(defthm valid-binary-of-type-fix-type-arg2
(equal (valid-binary expr op type-arg1 (type-fix type-arg2)
ienv)
(valid-binary expr op type-arg1 type-arg2 ienv)))
Theorem: valid-binary-type-equiv-congruence-on-type-arg2
(defthm valid-binary-type-equiv-congruence-on-type-arg2
(implies (type-equiv type-arg2 type-arg2-equiv)
(equal (valid-binary expr op type-arg1 type-arg2 ienv)
(valid-binary expr
op type-arg1 type-arg2-equiv ienv)))
:rule-classes :congruence)
Theorem: valid-binary-of-ienv-fix-ienv
(defthm valid-binary-of-ienv-fix-ienv
(equal (valid-binary expr
op type-arg1 type-arg2 (ienv-fix ienv))
(valid-binary expr op type-arg1 type-arg2 ienv)))
Theorem: valid-binary-ienv-equiv-congruence-on-ienv
(defthm valid-binary-ienv-equiv-congruence-on-ienv
(implies (ienv-equiv ienv ienv-equiv)
(equal (valid-binary expr op type-arg1 type-arg2 ienv)
(valid-binary expr
op type-arg1 type-arg2 ienv-equiv)))
:rule-classes :congruence)
