Fix normalization of numeric values in JSONB GIN indexes.

The default JSONB GIN opclass (jsonb_ops) converts numeric data values
to strings for storage in the index.  It must ensure that numeric values
that would compare equal (such as 12 and 12.00) produce identical strings,
else index searches would have behavior different from regular JSONB
comparisons.  Unfortunately the function charged with doing this was
completely wrong: it could reduce distinct numeric values to the same
string, or reduce equivalent numeric values to different strings.  The
former type of error would only lead to search inefficiency, but the
latter type of error would cause index entries that should be found by
a search to not be found.

Repairing this bug therefore means that it will be necessary for 9.4 beta
testers to reindex GIN jsonb_ops indexes, if they care about getting
correct results from index searches involving numeric data values within
the comparison JSONB object.

Per report from Thomas Fanghaenel.

src/backend/utils/adt/numeric.c

@@ -629,15 +629,17 @@ numeric_out_sci(Numeric num, int scale)
 /*
  * numeric_normalize() -
  *
- *	Output function for numeric data type without trailing zeroes.
+ *	Output function for numeric data type, suppressing insignificant trailing
+ *	zeroes and then any trailing decimal point.  The intent of this is to
+ *	produce strings that are equal if and only if the input numeric values
+ *	compare equal.
  */
 char *
 numeric_normalize(Numeric num)
 {
 	NumericVar	x;
 	char	   *str;
-	int			orig,
-				last;
+	int			last;
 
 	/*
 	 * Handle NaN
@@ -649,18 +651,24 @@ numeric_normalize(Numeric num)
 
 	str = get_str_from_var(&x);
 
-	orig = last = strlen(str) - 1;
-
-	for (;;)
+	/* If there's no decimal point, there's certainly nothing to remove. */
+	if (strchr(str, '.') != NULL)
 	{
-		if (last == 0 || str[last] != '0')
-			break;
+		/*
+		 * Back up over trailing fractional zeroes.  Since there is a decimal
+		 * point, this loop will terminate safely.
+		 */
+		last = strlen(str) - 1;
+		while (str[last] == '0')
+			last--;
 
-		last--;
-	}
+		/* We want to get rid of the decimal point too, if it's now last. */
+		if (str[last] == '.')
+			last--;
 
-	if (last > 0 && last != orig)
-		str[last] = '\0';
+		/* Delete whatever we backed up over. */
+		str[last + 1] = '\0';
+	}
 
 	return str;
 }