Symbolic Model 'strcmp' (null chars)

[frediramos]

Summary of the problem

Ths symbolic model for the strcmp function (line 99) does not take into account that intermediate symbolic bytes from both strings can also be null characters. This leads to both missing and incorrect execution paths with regard to strcmp's specification.

Example

Consider, for instance, two symbolic input string composed by 3 symbolic bytes:

str1 = "| sym1 | sym2 | sym3 |x00"
str2 = "| sym4 | sym5 | sym6 |x00"

The model for this function produces the following ITE formula:
ret = ITE(sym1 ̸= sym4 , sym1 − sym4 , ITE(sym2 ̸= sym5, sym2 − sym5, ITE(sym3 ̸= sym6, sym3 − sym6, 0)))

This formula allows for missing and incorrect path as exemplified below:

Missing path

str1 = "| A | x00 | B |x00"
str2 = "| A | x00 | A |x00"
ret = 0

Wrong path

str1 = "| x00 | A | B |x00"
str2 = "| x00 | A | A |x00"
ret = 1

We agree that function models/summaries should be kept simple, but we believe that every model should either contain all correct paths, or not contain any incorrect path.