Spec math modes

Current Behaviour

Proof modes:

1. No overflows, model everything as big ints (unsound)
2. Checked overflows (incomplete but sound)
3. Java Behaviour (sound and complete but may be hard to close)

Chosen proof mode applies to both code and specification of all contracts used within this proof.

Checked overflows

Wording in KeY: 'Arithmetic with overflow checking' also treats integers as mathematical objects, but ensures that no overflow occurs

Current behaviour e.g.:

assignmentAdditionInt {   
   \find( [ x = a + b ] post )
   \replacewith(
        { x := 
	       \if(inInt(a + b))
				\then(a + b)
				\else(javaAddIntOverflow(a, b)) 
		} post
   )
};

Observation: Current mode does not prevent all overflows, better wording would be: Checks that no overflows occur or that their result does not matter otherwise.

Wording in KeY Book: Mentions overflow being a fixed, but unspecified value.

Old KeY Book 12.4.1:

• Strengthening the precondition of the operations to ensure that the operations only act on the parts of the domain where int actually behaves like integer
• Results in additional proof obligations stating that the result of an operation does not exceed the (finite) range of the expression type

JML Ref

Math Modifiers

The modifiers java_math, safe_math and bigint_math describe what math modes are used for specifications (spec_*) and for Java code (code_*). Chalin04

These are allowed on class and method level.

1. java_math: Integral arithmetic can cause silent wrap-around of computations.
2. safe_math: Wrap-around of integral arithmetic causes exceptions.
3. bigint_math: There is no wrap-around, use bigints.

Example

/*@ public normal_behaviour
  @ requires x < Integer.MAX_VALUE;
  @ ensures \result == x + 1;
  @*/
/*@ spec_bigint_math @*/
/*@ code_safe_math @*/
public static int add_one(int x) {
	return x + 1;
}

Default here: java_math but a warning is issued when no modifier is given since this is indeed unexpected.

Problem with code_safe_math and code_bigint: Runtime exceptions and BigInts?!

Consideration

• Use different math mode for code and spec
  • This is not possible with the current taclet options
  • Proving a stronger version of the code (e.g. with checked overflows) should not change the contract in any observable way
• code_* modifiers are a proof detail and can remain a taclet option or similar
• spec_* modifiers however are not a proof detail
  • Produces inconsistencies requiring external tooling to check: Am I actually using what I proved?
  • This has to be a per method or per contract decision
  • Can vary per method, not a global decision
• code_* modelling is only for symbolic execution and makes proofs less strong
• Modes java_math and bigint_math are already implemented and remain conceptually unchanged
• All modes should be callable in specification, e.g. \java_math(\forall int x; blkjrej; x + y >= 0))
• Problem with bsum and bprod
  • Some rules assume bigints
• inInt should makes sense even without overflows, it should not translate to true, use something else for parameters that does this
• Parameters and return values should always be inInt, not matter the mode
  • Future work

Safe maths

• spec_safe_math makes no sense
  • Either we want wrapping or no wrapping, but definitely no runtime exceptions
• code_safe_math: Deviate from standard: We don't want to use runtime exceptions
• This adds a branch for every source code arithmetic operation
• It is clear why this check is necessary and where its proof obligation comes from
• Does not clutter the sequent with if-then-else formulas
• The branch has to be added to ensure the absence of all overflows being proven
• The additional overhead of this simple branch is minuscule, there is no need to split proving overflow and functional properties even for larger projects

Our proposition

• JML Modifiers for methods
  • spec_java_math and spec_bigint_math
  • spec_safe_math part of well definedness (optional)
• Default spec mode spec_bigint_math (deviation from Chalin)
• Default code mode checked overflows
• Rebuild taclet option checked overflows

assignmentAdditionInt {   
   \find(
	   [ x = a + b ] post
   )
   "Overflow check": \replacewith (
       inInt(a + b)
   );
   "Usage": \replacewith(
       { x := a + b } post
   )
};

• JML operator \java_math(x + y) (optional)