From 10e1ef1ca614f5236f854d3c7edcb91e375d03b2 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 25 Feb 2019 06:48:42 -0800 Subject: [PATCH] [sledge] Update TODO Reviewed By: mbouaziz Differential Revision: D14075521 fbshipit-source-id: d1f3a52d3 --- sledge/TODO.org | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/sledge/TODO.org b/sledge/TODO.org index 39be37d74..5f59b045d 100644 --- a/sledge/TODO.org +++ b/sledge/TODO.org @@ -16,6 +16,7 @@ rather than nearest enclosing ** revise spec of strlen to account for non-max length strings ** convert strlen inst into a primitive to return the end of the block containing a pointer, and model strlen in code * llair +** simplify "greater-than" exps to "less-than" in reverse order ** when Xor exps have types, simplify e xor e to 0 ** normalize polynomial equations by dividing coefficients by their gcd ** treat Typ.ptr as an integer of some particular size (i.e. ptr = intptr) @@ -221,7 +222,6 @@ us and xs, or just fv? since they (could) have the same domain ** optimize: can identity mappings in lkp be removed? * symbolic heap -** NEXT normalize conditional exps to disjunction ** Congruence should handle equalities of equalities to integers currently handled by Sh.pure ** normalize exps in terms of reps @@ -419,3 +419,5 @@ It seems possible that two edges will be distinct only due to differences betwee ** start-anywhere/bottom-up analysis ** non-dnf solver ** arithmetic constraints +** overflow analysis +- Currently expressions are shared between the IR for code and the analyzer's formulas. In order to strengthen the analyzer to detect overflow, it will likely be necessary to distinguish these, letting the analyzer normalize with polynomials, while keeping the same order of operations as the source for the IR. Plus another level of transformers for the IR expressions where their abstract values could be checked for being in range, etc.