From 99b23f8387d9d9c0173ed4a3c5716f0d55c36074 Mon Sep 17 00:00:00 2001 From: Alex Fedotov Date: Sat, 22 Aug 2015 02:14:14 -0700 Subject: [PATCH 1/2] Fix for #204. --- .../AbstractInterpretation/Abstract Domains/Utils.cs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Microsoft.Research/AbstractInterpretation/Abstract Domains/Utils.cs b/Microsoft.Research/AbstractInterpretation/Abstract Domains/Utils.cs index 3898399a..e50e1004 100644 --- a/Microsoft.Research/AbstractInterpretation/Abstract Domains/Utils.cs +++ b/Microsoft.Research/AbstractInterpretation/Abstract Domains/Utils.cs @@ -866,6 +866,12 @@ virtual public Out VisitGreaterThan_Un(Expression left, Expression right, Expres Contract.Requires(left != null); Contract.Requires(right != null); + // the Roslyn compiler uses cgt.un for comparing references to null; while producing correct + // results at runtime, it doesn't match implicit non-null assumptions made by the static checker, + // so we detect it here and convert it to an old-style equality comparison + if (decoder.IsNull(right)) + return VisitNotEqual(left, right, original, data); + return DispatchCompare(VisitLessThan_Un, right, left, original, data); } From 4f922bffd5f22cf2453caea30e2140e33e5c05db Mon Sep 17 00:00:00 2001 From: Alex Fedotov Date: Sun, 23 Aug 2015 10:11:50 -0700 Subject: [PATCH 2/2] Improved comment for why cgt.un is treated as "not equal" for nulls on right hand side. --- .../AbstractInterpretation/Abstract Domains/Utils.cs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Microsoft.Research/AbstractInterpretation/Abstract Domains/Utils.cs b/Microsoft.Research/AbstractInterpretation/Abstract Domains/Utils.cs index e50e1004..f667d0d5 100644 --- a/Microsoft.Research/AbstractInterpretation/Abstract Domains/Utils.cs +++ b/Microsoft.Research/AbstractInterpretation/Abstract Domains/Utils.cs @@ -866,9 +866,10 @@ virtual public Out VisitGreaterThan_Un(Expression left, Expression right, Expres Contract.Requires(left != null); Contract.Requires(right != null); - // the Roslyn compiler uses cgt.un for comparing references to null; while producing correct - // results at runtime, it doesn't match implicit non-null assumptions made by the static checker, - // so we detect it here and convert it to an old-style equality comparison + // Since there is no cne instruction, ECMA-335 §III.1.5 makes a note that cgt.un may + // be used instead for the specific case where the right-hand-side is null. If the + // right side is null, we treat the instruction as a "not equal" instruction for + // improved results from the static checker. if (decoder.IsNull(right)) return VisitNotEqual(left, right, original, data);