[Question][Hw4] What's `cmp` and `filter` for numerical domains?

[yusungsim]

In my understanding, cmp and filter are for compare and filter functions in the abstract semantics, which are used for partitioning abstract memories when encountering branches.

According to the hw4 document, abstract filter is defined as a function from abstract memory to abstract memory.
And although it is not specified in the same document, I think abstract compare should be a part of eval function that takes two expressions and one abstract memory that returns an abstract memory.

However, in domain.ml in hw4, cmp and filter functions should be defined for numerical domains, which types are as follows.

val cmp : Llvm.Icmp.t -> t -> t -> t
val filter : Llvm.Icmp.t -> t -> t -> t

I think these cmp and filter functions are not really neccesary, instead one can use filter function in semantics.ml file in abstract semantics to partition the given state.

Is my understanding correct? What are the purpose (ie. informal semantic meaning) of cmp and filter functions in numerical domains?

[yusungsim]

I just read the readme in github page... sorry!

• for anyone with similar question

3. Implementing Numerical Domains and Memory Domain

In this homework, you will implement the sign domain and the interval domain in the corresponding modules. Both of the modules are required to implement sound abstract semantic functions declared in module type NUMERICAL_DOMAIN. For the interval domain, you have to implement the widening and narrowing operators introduced in the lecture. For the sign domain, assume that the widening oprator will be the same as its join. Assume that all integers are signed and ignore integer-overflow effects. The output of the abstract semantics of div is defined as top when the divisor can be potentially zero.

To achieve precise static analysis result, use of the filter funtion for each domain (e.g., Sign.filter or Interval.filter) at conditional branches is important. Function call filter pred v1 v2 will return a sound refinement of abstract numerical value v1 with respect to predicate pred and abstract numerical value v2. If no refinment is possible, it will soundly return v1 as it is. In case of the interval domain, filter < [1, 10] [3, 5] will soundly refine the left interval to [1, 4], but filter < [1, 10] [1, 10] will return [1, 10] because no refinement is possible.

You will define the filter function for memories (Semantics.Make.filter) using the ones for values. The first argument of the function represents whether the condition (i.e., the second argument) is true or not. For example, filter (x < 10) true mem will return an abstract memory that satisfies condition x < 10. On the other hand, filter (x < 10) false mem will return an abstract memory that does not satisfy condition x < 10.

The domains for memories will be defined with the choice of numerical domain in src/main.ml. See modules SignMemory and IntervalMemory.