The goal of this session is to implement an interpreter matching the denotational semantic.

Implement the missing function in this (recommended but not mandatory) order :

Numerical domains

1. domains/bool_domain.ml

Implement the missing functions in the MakeConcrete functor.

• First, find a suitable type t representing boolean values.

• Second, define all booleans operations on this type.

2. domains/int_domain.ml

Implement the missing functions in the MakeConcrete functor.

The integer operations returns t add_bottom * err. The first element is the result of the operation, Nb res, or Bot if the expression is undefined (e.g. division by zero). The second element, is the set of error raised in the evaluation of the expression.

The bin and bin_bool functions are auxiliary functions used for evaluating expressions that don’t raise any errors (add, sub, …).

The other operations that you need to define are:

• unary operations uplus and uminus. They are straightforward.
• binary operations div and modulo: you have to handle possible division by zero errors.

In the int_domain boolean predicates such as less return a couple of boolean. The first one corresponds to can_be_true the second one to can_be_false. For example, less Z.zero Z.one should return true, false and less Z.one Z.zero, false, true. And the error part should be E.empty in both case.

Value Domain

3. domains/values.ml

Implement the MakeValueBasics functor. The already implemented MakeValue functor, automatically lifts all operations (add, equal) by calling the right function with the corresponding arguments in ValueBasics. So you only have to implements the following functions:

• int_bool_binary_bool: that lifts equality/inequality tests. i.e. operations of type α -> α -> bool where α is either I.t or B.t. Comparing two values of different types should raise a type error.
• int_unary: for operation of type I.t -> I.t. (e.g. uminus)
• int_binary: for operation of type I.t -> I.t -> I.t (e.g. add)
• int_binary_bool: for operation of type I.t -> I.t -> B.t (e.g. less)
• bool_unary: for operation of type B.t -> B.t (not)
• bool_binary: for operation of type B.t -> B.t -> B.t (e.g. or)

Take a look at type ival. It denotes values with an int and a bool part. For each function, apply the function given in argument to the correct part and raise errors if the values don’t match the expected type. For this domain, don’t spend too much time to ensure well-typedness of values since it will be the subject of next week.

Environment

4. domains/environment.ml

Take a look at types simple_env and env. Understand what are their goals.

You have two functions to implement here :

• eval_expr that returns the set of possible values for an expression. Feel free to define auxiliary functions.
• eval_assign that handles an assignment.

Interpreter

5. interpreter/interpreter.ml

To conclude, you will need to implement the iterator for the denotational semantic.

lfp computes the fixpoint of the function f given in argument by iteration starting from pre-fixpoint x. The cmp argument is used to compare values to test if we reached a fixpoint. Since we use, Set.Make and Map.Make functors, make sure to use the compare functions of these modules and not the default compare function. Otherwise, you may have imprecise results such as:

module ISet = Set.Make(Int)
let s1 = ISet.empty |> ISet.add 0 |> ISet.add 1
let s2 = ISet.empty |> ISet.add 1 |> ISet.add 0
(* Both sets should be equal to {0, 1} *)
let _ =
  Format.printf "compare s1 s2 = %i\n" (compare s1 s2);
  Format.printf "ISet.compare s1 s2 = %i\n" (ISet.compare s1 s2);

eval_stat computes the denotational semantic of a statement in an environment.