Feature request: ensure literals have the correct size to prevent unexpected behavior

[beurdouche]

let r : UInt64.t = UInt64.of_string "0xFFFFff80" is accepted by F*. While this is valid in C we have examples when this is causing trouble for instance with CVE-2019-8741 in Apple's core crypto library because the code was meant as 0xFFFFFFFFFFFFff80 and I think we should always enforce that literals have the correct size in F* code.

[mtzguido]

Hi Benjamin, that's an interesting one. We looked at this locally and have some ideas:

• First, looking at val of_string : string -> Tot UInt64.t, it clearly has a problem: the string may fail to be parsed as an integer, and this raises an exception, so it's not Tot. Some alternatives are:

  1. returning an option, which is easy to do, but requires users of this function to consider the None case.
  2. encoding some predicate for valid strings and it add as a precondition of this function. Maybe this predicate can be abstract and with some native support so literals would work, but we don't expect that to work well with SMT.

• However... it turns out these of_string functions are never used in any of our projects, so they could also be removed. Are you using them?

• In any case, we mostly write literals as 0xFFFFff80L, and the same problem arises. We can definitely check these things in the parser. And raise a warning, maybe? Failing seems too harsh for me... Also I could see someone writing 0x0L, and that's perfectly OK, so maybe a zero at left allows the literal to not be full-width?

I think my preference would be to change of_string to return options, and raising a warning on hex literals that are shorter than full and do not have a leftmost zero. What do you think?

Thanks!