Add code to analyse function return types

For ASL parser, we have code that can add additional constraints to a
function if they are required by functions it calls, but for more
general range analysis we need to restrict the return types of various
ASL functions that return int. To do this we can write some code that
walks over the type-checked AST for a function body and tries to infer
a more restrictive return type at each function exit point. Then we
try to union those types together if possible to infer a more
restricted return type.

For example, for the highest_set_bit function

val highest_set_bit : forall ('n : Int), 'n >= 0. bits('n) -> int

function highest_set_bit x = {
  foreach (i from ('n - 1) to 0 by 1 in dec) {
    print_int("idx = ", i);
    if [x[i]] == 0b1 then return(i) else ()
  };
  return(negate(1))
}

Which is annotated as returning any int, we can synthesise a return
type of

{'m, ('m = -1 | (0 <= 'm & 'm <= ('n - 1))). int('m)}

Currently I have this code in Sail as it's likely also useful as a
optimisation/lint but it could also live in the asl_parser repository.

0 files changed, 0 insertions, 0 deletions