Non-monotonic recursion: typeSize -!-> typeSize

[Lslightly]

I want to calculate the size of type defined in Golang programs and I fail to find libraries to do that. Therefore I try to do it myself.

There exists types whose size can be unknown, so I mark them as -1 to indicate they are unknown. But problem occurs when I meet struct type. I first check its fields to see if the size is unknown. If it is, I will set result = -1 which indicates the size of struct is unknown. But then the error Non-monotonic recursion: typeSize -!-> typeSize appears!

The program is as follows:

language[monotonicAggregates]
int typeSize(Type type) {
    exists(Type t | type.getUnderlyingType() = t |
        ...
        else if t instanceof StructType then
            if exists(Field f| f = t.getField(_) and -1 = typeSize(f.getType())) then
                result = -1
            else
                result = sum(Field f| f = t.getField(_)|typeSize(f.getType()))
        ...
    )

I add language[monotonicAggregates] to the function(or predicate with result) but it does not work. I think if codeql agrees to analyze the code, then the type the analyzer read must be valid type whose size can be infered and the tree of type is monotonicAggregates.

[intrigus-lgtm]

Can you give the full code for typeSize and all the predicates it depends on?

[Lslightly]

import go

language[monotonicAggregates]
int typeSize(Type type) {
    exists(Type t | type.getUnderlyingType() = t |
        if t instanceof BoolType then
            result = 8
        else if t instanceof IntegerType then
            result = 8
        else if t instanceof UintptrType then
            result = 8
        else if t instanceof NumericType then
            result = t.(NumericType).getASize() / 8
        else if t instanceof StringType then
            /*
            * struct {
            *  header  unsafe.Pointer
            *  len     unsafe.Pointer
            * }
            */
            result = 16
        else if t instanceof ArrayType then
            result = forwardUnknown(t.(ArrayType).getLength() * typeSize(t.(ArrayType).getElementType()), typeSize(t.(ArrayType).getElementType()))
        else if t instanceof SliceType then
            /*
            * struct {
            *  header  unsafe.Pointer
            *  len     unsafe.Pointer
            *  cap     unsafe.Pointer
            * }
            */
            result = 24
        else if t instanceof StructType then
            if exists(Field f| f = t.getField(_) and -1 = typeSize(f.getType())) then
                result = -1
            else
                result = sum(Field f| f = t.getField(_)|typeSize(f.getType()))
        else if t instanceof PointerType then
            result = 8
        else if t instanceof SignatureType then
            result = 16
        else if t instanceof InterfaceType then
            /*
             * type descriptor
             * data
             */
            result = 16
        else
            result = -1 // -1 means unknown
    )
}
bindingset[ok, err]
int forwardUnknown(int ok, int err) {
    if err = -1 then
        result = -1
    else
        result = ok
}

[owen-mc]

I think your problem is caused by the use of if A then B else C. That desugars to A and B or not A and C. This introduces lots of nots, and I guess an odd number of them are getting into the recursion. It's a bit nicer to rewrite it without if then else, since most of your conditions are mutually exclusive. This works for me:

language[monotonicAggregates]
int typeSize(Type type) {
  exists(Type t | type.getUnderlyingType() = t |
    t instanceof BoolType and
    result = 8
    or
    t instanceof IntegerType and
    result = 8
    or
    t instanceof UintptrType and
    result = 8
    or
    t instanceof NumericType and
    not t instanceof IntegerType and
    result = t.(NumericType).getASize() / 8
    or
    t instanceof StringType and
    /*
     * struct {
     *  header  unsafe.Pointer
     *  len     unsafe.Pointer
     * }
     */

    result = 16
    or
    t instanceof ArrayType and
    result =
      forwardUnknown(t.(ArrayType).getLength() * typeSize(t.(ArrayType).getElementType()),
        typeSize(t.(ArrayType).getElementType()))
    or
    t instanceof SliceType and
    /*
     * struct {
     *  header  unsafe.Pointer
     *  len     unsafe.Pointer
     *  cap     unsafe.Pointer
     * }
     */

    result = 24
    or
    t instanceof PointerType and
    result = 8
    or
    t instanceof SignatureType and
    result = 16
    or
    t instanceof InterfaceType and
    /*
     * type descriptor
     * data
     */

    result = 16
    or
    t instanceof StructType and
    (
      exists(Field f | f = t.getField(_) and -1 = typeSize(f.getType())) and
      result = -1
      or
      forall(Field f | f = t.getField(_) | typeSize(f.getType()) != -1) and
      result = sum(Field f | f = t.getField(_) | typeSize(f.getType()))
    )
    or
    not (
      t instanceof BoolType or
      t instanceof IntegerType or
      t instanceof UintptrType or
      t instanceof NumericType or
      t instanceof StringType or
      t instanceof ArrayType or
      t instanceof SliceType or
      t instanceof StructType or
      t instanceof PointerType or
      t instanceof SignatureType or
      t instanceof InterfaceType
    ) and
    result = -1 // -1 means unknown
  )
}

[owen-mc]

Another note: a more idiomatic way of representing "unknown" is to have the predicate not hold in those cases. Like this:

language[monotonicAggregates]
int typeSize2(Type type) {
  exists(Type t | type.getUnderlyingType() = t |
    t instanceof BoolType and
    result = 8
    or
    t instanceof IntegerType and
    result = 8
    or
    t instanceof UintptrType and
    result = 8
    or
    t instanceof NumericType and
    not t instanceof IntegerType and
    result = t.(NumericType).getASize() / 8
    or
    t instanceof StringType and
    /*
     * struct {
     *  header  unsafe.Pointer
     *  len     unsafe.Pointer
     * }
     */

    result = 16
    or
    t instanceof ArrayType and
    exists(typeSize(t.(ArrayType).getElementType())) and
    result = t.(ArrayType).getLength() * typeSize(t.(ArrayType).getElementType())
    or
    t instanceof SliceType and
    /*
     * struct {
     *  header  unsafe.Pointer
     *  len     unsafe.Pointer
     *  cap     unsafe.Pointer
     * }
     */

    result = 24
    or
    t instanceof PointerType and
    result = 8
    or
    t instanceof SignatureType and
    result = 16
    or
    t instanceof InterfaceType and
    /*
     * type descriptor
     * data
     */

    result = 16
    or
    t instanceof StructType and
    forall(Field f | f = t.getField(_) | exists(typeSize(f.getType()))) and
    result = sum(Field f | f = t.getField(_) | typeSize(f.getType()))
  )
}

[Lslightly]

Thanks for your advice. If I understand correctly, having the predicate not hold for unknown means that I need another judging predicate, such as isTypeSizeKnown, right?

[Lslightly]

Besides, I have a statement to be checked:

If the variable t is not instance of any classes appear in typeSize2, i.e. t is unknown type, then typeSize2 will be evaluated as false. Therefore, if the size of the element type of an array type ArrTy is unknown, then exists(typeSize2(t.(ArrayType).getElementType())) will be evaluated as exists(false) and then false. typeSize2(ArrTy) will be evaluated as false since no branch in exists(Type t|...|...) is true.

Is this statement correct?

[owen-mc]

You could have a judging predicate isTypeSizeKnown, which just contains if exists(typeSize2(t)) then result = true else result = false. But often this kind of logic is better expressed inline rather than calling a predicate.

false isn't quite the right word. More like (empty set). We normally talk about a predicate not holding. It really helps to remember that predicates aren't functions, most notably because they can have multiple values. Consider typeSize of int. You could make the result 32 or 64 to represent the possible values on different widespread architectures. What's happening behind the scenes is that each predicate is evaluated once before it's used, and the results are put in a table, we're looking for rows where the first column is t and then the result is whatever the second column is. There might be no rows like that, or more than one.

If t is some other type that isn't checked for in typeSize2, and ArrTy is the type of an array of t things, then typeSize2(t.(ArrayType).getElementType()) will not have any results, so exists(typeSize2(t.(ArrayType).getElementType())) will evaluate to false. So yes, typeSize2(ArrTy) will not hold, and you don't have to use a judging predicate like isTypeSizeKnown you mentioned earlier. This is an example where having a predicate not hold instead of returning a special unknown value makes things more natural. But note that for StructType I did have to assert that typeSize2 exists for all fields, otherwise sum(Field f | f = t.getField(_) | typeSize(f.getType())) will silently ignore the fields where typeSize2 doesn't have a value.