Andrewmwells/python missing extrinsic handling

[andrewmwells-amazon]

Add initial implementation for handling unmodeled functions

Suppose we need to analyze Python code that looks like this:

def foo(l: List[str]):
    a : int = 0
    b : int = 0
    if(len(l) > 0):
      a = unmodeled_fun(l) # line 5
      return modeled_fun(l[0])
    else:
      b = -1
    return modeled_fun_int(b)

What we should do for modeled_fun seems clear— we use the model we have. The question is what we should do for unmodeled_fun.

We propose dividing unmodeled functions into three categories (for now we ignore aliasing):

Category A (havocAll)

An unmodeled function in Category A is assumed to havoc all globals. This is the safest option, but will let us prove the least about the code. In our example, at line 5 we would havoc a, l and b.

Category B (havocArgsAndRet)

An unmodeled function in Category B is assumed to havoc only it’s parameters. This strikes a balance between safety and expressive power. In our example, at line 5 we would havoc a and l[0].

Category C (havocRet)

An unmodeled function in Category C is assumed to havoc neither it’s parameters nor other variables. This is the least safe option, but lets us prove the most. In our example, at line 5 we would havoc a.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.