This pull request completely rewrites the overflow handling for the analyses lin2vareq and affeq.
Old overflow handling
Before, the oveflow handling happened in texpr1_expr_of_cil_exp, meet_tcons_one_var_eq and also in other places. This was not very maintainable and it was not completely sound. Now all of this is solely handled by the no_ov flag.
New overflow handling
A query MaySignedOverflow was added to base.ml. It checks for each subexpression if there is an overflow, and it returns false for unsigned subexpressions. It uses EvalInt to find out if there was an overflow or not.
This query is used by the function no_overflow, which sets the no_ov flag, which is used in texpr1_expr_of_cil_exp, where the overflow handling takes place.
Overflow checking for Apron domains
The apron domains (e.g. polyhedra) are not compatible with the new overflow checking method. They handle overflow differently than affeq and they rely on the bounds check that was made in texpr1_expr_of_cil_exp before I removed it.
They cannot rely only on the no_ov flag to calculate the overflow, partly because they also store inequalities and because
the MaySignedOverflow query is not suitable for finding overflow for unsigned expressions.
Therefore the old overflow check in texpr1_expr_of_cil_exp was kept as it is, and it can be turned on or off by a flag set in the module OverflowCheck. It is turned on for the apron domains and off for affeq and lin2vareq.
Other changes
The function assert_cons was renames to assert_constraint for better readability.
The calculation of the bounds of an expression was moved to a function eval_interval.
This pull request completely rewrites the overflow handling for the analyses
lin2vareqandaffeq.Old overflow handling
Before, the oveflow handling happened in
texpr1_expr_of_cil_exp,meet_tcons_one_var_eqand also in other places. This was not very maintainable and it was not completely sound. Now all of this is solely handled by theno_ovflag.New overflow handling
A query
MaySignedOverflowwas added tobase.ml. It checks for each subexpression if there is an overflow, and it returnsfalsefor unsigned subexpressions. It usesEvalIntto find out if there was an overflow or not.This query is used by the function
no_overflow, which sets theno_ovflag, which is used intexpr1_expr_of_cil_exp, where the overflow handling takes place.Overflow checking for Apron domains
The apron domains (e.g.
polyhedra) are not compatible with the new overflow checking method. They handle overflow differently thanaffeqand they rely on the bounds check that was made intexpr1_expr_of_cil_expbefore I removed it. They cannot rely only on theno_ovflag to calculate the overflow, partly because they also store inequalities and because theMaySignedOverflowquery is not suitable for finding overflow for unsigned expressions. Therefore the old overflow check intexpr1_expr_of_cil_expwas kept as it is, and it can be turned on or off by a flag set in the moduleOverflowCheck. It is turned on for theaprondomains and off foraffeqandlin2vareq.Other changes
The function
assert_conswas renames toassert_constraintfor better readability.The calculation of the bounds of an expression was moved to a function
eval_interval.