Add test scaffolding for exercising optimizer's predicate-proof logic.

The predicate-proof code in predtest.c is a bit hard to test as-is:
you have to construct a query whose plan changes depending on the success
of a test, and in tests that have been around for awhile, it's always
possible that the plan shape is now being determined by some other factor.
Our existing regression tests aren't doing real well at providing full
code coverage of predtest.c, either.  So, let's add a small test module
that allows directly inspecting the results of predicate_implied_by()
and predicate_refuted_by() for arbitrary boolean expressions.

I chose the set of tests committed here in order to get reasonably
complete code coverage of predtest.c just from running this test
module, and to cover some cases called out as being interesting in
the existing comments.  We might want to add more later.  But this
set already shows a few cases where perhaps things could be improved.

Indeed, this exercise proves that predicate_refuted_by() is buggy for
the case of clause_is_check = true, though fortunately we aren't using
that case anywhere yet.  I'll look into doing something about that in
a separate commit.  For now, just memorialize the current behavior.

Discussion: https://postgr.es/m/5983.1520487191@sss.pgh.pa.us
This commit is contained in:
Tom Lane 2018-03-08 13:25:26 -05:00
parent 04e7ecadf6
commit 44468f49bb
9 changed files with 1356 additions and 0 deletions

View File

@ -13,6 +13,7 @@ SUBDIRS = \
test_extensions \
test_parser \
test_pg_dump \
test_predtest \
test_rbtree \
test_rls_hooks \
test_shm_mq \

View File

@ -0,0 +1,4 @@
# Generated subdirectories
/log/
/results/
/tmp_check/

View File

@ -0,0 +1,21 @@
# src/test/modules/test_predtest/Makefile
MODULE_big = test_predtest
OBJS = test_predtest.o $(WIN32RES)
PGFILEDESC = "test_predtest - test code for optimizer/util/predtest.c"
EXTENSION = test_predtest
DATA = test_predtest--1.0.sql
REGRESS = test_predtest
ifdef USE_PGXS
PG_CONFIG = pg_config
PGXS := $(shell $(PG_CONFIG) --pgxs)
include $(PGXS)
else
subdir = src/test/modules/test_predtest
top_builddir = ../../../..
include $(top_builddir)/src/Makefile.global
include $(top_srcdir)/contrib/contrib-global.mk
endif

View File

@ -0,0 +1,28 @@
test_predtest is a module for checking the correctness of the optimizer's
predicate-proof logic, in src/backend/optimizer/util/predtest.c.
The module provides a function that allows direct application of
predtest.c's exposed functions, predicate_implied_by() and
predicate_refuted_by(), to arbitrary boolean expressions, with direct
inspection of the results. This could be done indirectly by checking
planner results, but it can be difficult to construct end-to-end test
cases that prove that the expected results were obtained.
In general, the use of this function is like
select * from test_predtest('query string')
where the query string must be a SELECT returning two boolean
columns, for example
select * from test_predtest($$
select x, not x
from (values (false), (true), (null)) as v(x)
$$);
The function parses and plans the given query, and then applies the
predtest.c code to the two boolean expressions in the SELECT list, to see
if the first expression can be proven or refuted by the second. It also
executes the query, and checks the resulting rows to see whether any
claimed implication or refutation relationship actually holds. If the
query is designed to exercise the expressions on a full set of possible
input values, as in the example above, then this provides a mechanical
cross-check as to whether the proof code has given a correct answer.

View File

@ -0,0 +1,769 @@
CREATE EXTENSION test_predtest;
-- Make output more legible
\pset expanded on
-- Test data
-- all combinations of four boolean values
create table booleans as
select
case i%3 when 0 then true when 1 then false else null end as x,
case (i/3)%3 when 0 then true when 1 then false else null end as y,
case (i/9)%3 when 0 then true when 1 then false else null end as z,
case (i/27)%3 when 0 then true when 1 then false else null end as w
from generate_series(0, 3*3*3*3-1) i;
-- all combinations of two integers 0..9, plus null
create table integers as
select
case i%11 when 10 then null else i%11 end as x,
case (i/11)%11 when 10 then null else (i/11)%11 end as y
from generate_series(0, 11*11-1) i;
-- Basic proof rules for single boolean variables
select * from test_predtest($$
select x, x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x, not x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select not x, x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select not x, not x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x is not null, x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x is not null, x is null
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x is null, x is not null
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x is not true, x
from booleans
$$);
WARNING: weak_refuted_by result is incorrect
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | f
select * from test_predtest($$
select x, x is not true
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | t
select * from test_predtest($$
select x is false, x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x, x is false
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x is unknown, x
from booleans
$$);
WARNING: weak_refuted_by result is incorrect
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | f
select * from test_predtest($$
select x, x is unknown
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | t
s_r_holds | f
w_r_holds | t
-- XXX seems like we should be able to refute x is null here
select * from test_predtest($$
select x is null, x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | f
select * from test_predtest($$
select x, x is null
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | t
s_r_holds | f
w_r_holds | t
-- Tests involving AND/OR constructs
select * from test_predtest($$
select x, x and y
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select not x, x and y
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x, not x and y
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x or y, x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x and y, x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x and y, not x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x and y, y and x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select not y, y and x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x or y, y or x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x or y or z, x or z
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select z or w, x or y
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select z and w, x or y
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x, (x and y) or (x and z)
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select (x and y) or z, y and x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select (not x or not y) and z, y and x
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select y or x, (x or y) and z
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select not x and not y, (x or y) and z
from booleans
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
-- Tests using btree operator knowledge
select * from test_predtest($$
select x <= y, x < y
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x <= y, x > y
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x <= y, y >= x
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x <= y, y > x and y < x+2
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x <= 5, x <= 7
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x <= 5, x > 7
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x <= 5, 7 > x
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select 5 >= x, 7 > x
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select 5 >= x, x > 7
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select 5 = x, x = 7
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | t
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | t
select * from test_predtest($$
select x is not null, x > 7
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x is not null, int4lt(x,8)
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x is null, x > 7
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | f
select * from test_predtest($$
select x is null, int4lt(x,8)
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | t
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | t
w_r_holds | f
select * from test_predtest($$
select x is not null, x < 'foo'
from (values
('aaa'::varchar), ('zzz'::varchar), (null)) as v(x)
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | f
s_r_holds | f
w_r_holds | f
-- Cases using ScalarArrayOpExpr
select * from test_predtest($$
select x <= 5, x in (1,3,5)
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x <= 5, x in (1,3,5,7)
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f
-- XXX ideally, we could prove this case too
select * from test_predtest($$
select x <= 5, x in (1,3,5,null)
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | f
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x in (null,1,3,5,7), x in (1,3,5)
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x <= 5, x < all(array[1,3,5])
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | t
weak_implied_by | t
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | t
w_i_holds | t
s_r_holds | f
w_r_holds | f
select * from test_predtest($$
select x <= y, x = any(array[1,3,y])
from integers
$$);
-[ RECORD 1 ]-----+--
strong_implied_by | f
weak_implied_by | f
strong_refuted_by | f
weak_refuted_by | f
s_i_holds | f
w_i_holds | f
s_r_holds | f
w_r_holds | f

View File

@ -0,0 +1,298 @@
CREATE EXTENSION test_predtest;
-- Make output more legible
\pset expanded on
-- Test data
-- all combinations of four boolean values
create table booleans as
select
case i%3 when 0 then true when 1 then false else null end as x,
case (i/3)%3 when 0 then true when 1 then false else null end as y,
case (i/9)%3 when 0 then true when 1 then false else null end as z,
case (i/27)%3 when 0 then true when 1 then false else null end as w
from generate_series(0, 3*3*3*3-1) i;
-- all combinations of two integers 0..9, plus null
create table integers as
select
case i%11 when 10 then null else i%11 end as x,
case (i/11)%11 when 10 then null else (i/11)%11 end as y
from generate_series(0, 11*11-1) i;
-- Basic proof rules for single boolean variables
select * from test_predtest($$
select x, x
from booleans
$$);
select * from test_predtest($$
select x, not x
from booleans
$$);
select * from test_predtest($$
select not x, x
from booleans
$$);
select * from test_predtest($$
select not x, not x
from booleans
$$);
select * from test_predtest($$
select x is not null, x
from booleans
$$);
select * from test_predtest($$
select x is not null, x is null
from integers
$$);
select * from test_predtest($$
select x is null, x is not null
from integers
$$);
select * from test_predtest($$
select x is not true, x
from booleans
$$);
select * from test_predtest($$
select x, x is not true
from booleans
$$);
select * from test_predtest($$
select x is false, x
from booleans
$$);
select * from test_predtest($$
select x, x is false
from booleans
$$);
select * from test_predtest($$
select x is unknown, x
from booleans
$$);
select * from test_predtest($$
select x, x is unknown
from booleans
$$);
-- XXX seems like we should be able to refute x is null here
select * from test_predtest($$
select x is null, x
from booleans
$$);
select * from test_predtest($$
select x, x is null
from booleans
$$);
-- Tests involving AND/OR constructs
select * from test_predtest($$
select x, x and y
from booleans
$$);
select * from test_predtest($$
select not x, x and y
from booleans
$$);
select * from test_predtest($$
select x, not x and y
from booleans
$$);
select * from test_predtest($$
select x or y, x
from booleans
$$);
select * from test_predtest($$
select x and y, x
from booleans
$$);
select * from test_predtest($$
select x and y, not x
from booleans
$$);
select * from test_predtest($$
select x and y, y and x
from booleans
$$);
select * from test_predtest($$
select not y, y and x
from booleans
$$);
select * from test_predtest($$
select x or y, y or x
from booleans
$$);
select * from test_predtest($$
select x or y or z, x or z
from booleans
$$);
select * from test_predtest($$
select z or w, x or y
from booleans
$$);
select * from test_predtest($$
select z and w, x or y
from booleans
$$);
select * from test_predtest($$
select x, (x and y) or (x and z)
from booleans
$$);
select * from test_predtest($$
select (x and y) or z, y and x
from booleans
$$);
select * from test_predtest($$
select (not x or not y) and z, y and x
from booleans
$$);
select * from test_predtest($$
select y or x, (x or y) and z
from booleans
$$);
select * from test_predtest($$
select not x and not y, (x or y) and z
from booleans
$$);
-- Tests using btree operator knowledge
select * from test_predtest($$
select x <= y, x < y
from integers
$$);
select * from test_predtest($$
select x <= y, x > y
from integers
$$);
select * from test_predtest($$
select x <= y, y >= x
from integers
$$);
select * from test_predtest($$
select x <= y, y > x and y < x+2
from integers
$$);
select * from test_predtest($$
select x <= 5, x <= 7
from integers
$$);
select * from test_predtest($$
select x <= 5, x > 7
from integers
$$);
select * from test_predtest($$
select x <= 5, 7 > x
from integers
$$);
select * from test_predtest($$
select 5 >= x, 7 > x
from integers
$$);
select * from test_predtest($$
select 5 >= x, x > 7
from integers
$$);
select * from test_predtest($$
select 5 = x, x = 7
from integers
$$);
select * from test_predtest($$
select x is not null, x > 7
from integers
$$);
select * from test_predtest($$
select x is not null, int4lt(x,8)
from integers
$$);
select * from test_predtest($$
select x is null, x > 7
from integers
$$);
select * from test_predtest($$
select x is null, int4lt(x,8)
from integers
$$);
select * from test_predtest($$
select x is not null, x < 'foo'
from (values
('aaa'::varchar), ('zzz'::varchar), (null)) as v(x)
$$);
-- Cases using ScalarArrayOpExpr
select * from test_predtest($$
select x <= 5, x in (1,3,5)
from integers
$$);
select * from test_predtest($$
select x <= 5, x in (1,3,5,7)
from integers
$$);
-- XXX ideally, we could prove this case too
select * from test_predtest($$
select x <= 5, x in (1,3,5,null)
from integers
$$);
select * from test_predtest($$
select x in (null,1,3,5,7), x in (1,3,5)
from integers
$$);
select * from test_predtest($$
select x <= 5, x < all(array[1,3,5])
from integers
$$);
select * from test_predtest($$
select x <= y, x = any(array[1,3,y])
from integers
$$);

View File

@ -0,0 +1,16 @@
/* src/test/modules/test_predtest/test_predtest--1.0.sql */
-- complain if script is sourced in psql, rather than via CREATE EXTENSION
\echo Use "CREATE EXTENSION test_predtest" to load this file. \quit
CREATE FUNCTION test_predtest(query text,
OUT strong_implied_by bool,
OUT weak_implied_by bool,
OUT strong_refuted_by bool,
OUT weak_refuted_by bool,
OUT s_i_holds bool,
OUT w_i_holds bool,
OUT s_r_holds bool,
OUT w_r_holds bool)
STRICT
AS 'MODULE_PATHNAME' LANGUAGE C;

View File

@ -0,0 +1,215 @@
/*--------------------------------------------------------------------------
*
* test_predtest.c
* Test correctness of optimizer's predicate proof logic.
*
* Copyright (c) 2018, PostgreSQL Global Development Group
*
* IDENTIFICATION
* src/test/modules/test_predtest/test_predtest.c
*
* -------------------------------------------------------------------------
*/
#include "postgres.h"
#include "access/htup_details.h"
#include "catalog/pg_type.h"
#include "executor/spi.h"
#include "funcapi.h"
#include "optimizer/clauses.h"
#include "optimizer/predtest.h"
#include "optimizer/prep.h"
#include "utils/builtins.h"
PG_MODULE_MAGIC;
/*
* test_predtest(query text) returns record
*/
PG_FUNCTION_INFO_V1(test_predtest);
Datum
test_predtest(PG_FUNCTION_ARGS)
{
text *txt = PG_GETARG_TEXT_PP(0);
char *query_string = text_to_cstring(txt);
SPIPlanPtr spiplan;
int spirc;
TupleDesc tupdesc;
bool s_i_holds,
w_i_holds,
s_r_holds,
w_r_holds;
CachedPlan *cplan;
PlannedStmt *stmt;
Plan *plan;
Expr *clause1;
Expr *clause2;
bool strong_implied_by,
weak_implied_by,
strong_refuted_by,
weak_refuted_by;
Datum values[8];
bool nulls[8];
int i;
/* We use SPI to parse, plan, and execute the test query */
if (SPI_connect() != SPI_OK_CONNECT)
elog(ERROR, "SPI_connect failed");
/*
* First, plan and execute the query, and inspect the results. To the
* extent that the query fully exercises the two expressions, this
* provides an experimental indication of whether implication or
* refutation holds.
*/
spiplan = SPI_prepare(query_string, 0, NULL);
if (spiplan == NULL)
elog(ERROR, "SPI_prepare failed for \"%s\"", query_string);
spirc = SPI_execute_plan(spiplan, NULL, NULL, true, 0);
if (spirc != SPI_OK_SELECT)
elog(ERROR, "failed to execute \"%s\"", query_string);
tupdesc = SPI_tuptable->tupdesc;
if (tupdesc->natts != 2 ||
TupleDescAttr(tupdesc, 0)->atttypid != BOOLOID ||
TupleDescAttr(tupdesc, 1)->atttypid != BOOLOID)
elog(ERROR, "query must yield two boolean columns");
s_i_holds = w_i_holds = s_r_holds = w_r_holds = true;
for (i = 0; i < SPI_processed; i++)
{
HeapTuple tup = SPI_tuptable->vals[i];
Datum dat;
bool isnull;
char c1,
c2;
/* Extract column values in a 3-way representation */
dat = SPI_getbinval(tup, tupdesc, 1, &isnull);
if (isnull)
c1 = 'n';
else if (DatumGetBool(dat))
c1 = 't';
else
c1 = 'f';
dat = SPI_getbinval(tup, tupdesc, 2, &isnull);
if (isnull)
c2 = 'n';
else if (DatumGetBool(dat))
c2 = 't';
else
c2 = 'f';
/* Check for violations of various proof conditions */
if (c2 == 't' && c1 != 't')
s_i_holds = false;
if (c2 != 'f' && c1 == 'f')
w_i_holds = false;
if (c2 == 't' && c1 != 'f')
s_r_holds = false;
/* XXX is this the correct definition for weak refutation? */
if (c2 != 'f' && c1 == 't')
w_r_holds = false;
}
/*
* Now, dig the clause querytrees out of the plan, and see what predtest.c
* does with them.
*/
cplan = SPI_plan_get_cached_plan(spiplan);
if (list_length(cplan->stmt_list) != 1)
elog(ERROR, "failed to decipher query plan");
stmt = linitial_node(PlannedStmt, cplan->stmt_list);
if (stmt->commandType != CMD_SELECT)
elog(ERROR, "failed to decipher query plan");
plan = stmt->planTree;
Assert(list_length(plan->targetlist) >= 2);
clause1 = castNode(TargetEntry, linitial(plan->targetlist))->expr;
clause2 = castNode(TargetEntry, lsecond(plan->targetlist))->expr;
/*
* Because the clauses are in the SELECT list, preprocess_expression did
* not pass them through canonicalize_qual nor make_ands_implicit. We can
* do that here, though, and should do so to match the planner's normal
* usage of the predicate proof functions.
*
* This still does not exactly duplicate the normal usage of the proof
* functions, in that they are often given qual clauses containing
* RestrictInfo nodes. But since predtest.c just looks through those
* anyway, it seems OK to not worry about that point.
*/
clause1 = canonicalize_qual(clause1);
clause2 = canonicalize_qual(clause2);
clause1 = (Expr *) make_ands_implicit(clause1);
clause2 = (Expr *) make_ands_implicit(clause2);
strong_implied_by = predicate_implied_by((List *) clause1,
(List *) clause2,
false);
weak_implied_by = predicate_implied_by((List *) clause1,
(List *) clause2,
true);
strong_refuted_by = predicate_refuted_by((List *) clause1,
(List *) clause2,
false);
weak_refuted_by = predicate_refuted_by((List *) clause1,
(List *) clause2,
true);
/*
* Issue warning if any proof is demonstrably incorrect.
*/
if (strong_implied_by && !s_i_holds)
elog(WARNING, "strong_implied_by result is incorrect");
if (weak_implied_by && !w_i_holds)
elog(WARNING, "weak_implied_by result is incorrect");
if (strong_refuted_by && !s_r_holds)
elog(WARNING, "strong_refuted_by result is incorrect");
if (weak_refuted_by && !w_r_holds)
elog(WARNING, "weak_refuted_by result is incorrect");
/*
* Clean up and return a record of the results.
*/
if (SPI_finish() != SPI_OK_FINISH)
elog(ERROR, "SPI_finish failed");
tupdesc = CreateTemplateTupleDesc(8, false);
TupleDescInitEntry(tupdesc, (AttrNumber) 1,
"strong_implied_by", BOOLOID, -1, 0);
TupleDescInitEntry(tupdesc, (AttrNumber) 2,
"weak_implied_by", BOOLOID, -1, 0);
TupleDescInitEntry(tupdesc, (AttrNumber) 3,
"strong_refuted_by", BOOLOID, -1, 0);
TupleDescInitEntry(tupdesc, (AttrNumber) 4,
"weak_refuted_by", BOOLOID, -1, 0);
TupleDescInitEntry(tupdesc, (AttrNumber) 5,
"s_i_holds", BOOLOID, -1, 0);
TupleDescInitEntry(tupdesc, (AttrNumber) 6,
"w_i_holds", BOOLOID, -1, 0);
TupleDescInitEntry(tupdesc, (AttrNumber) 7,
"s_r_holds", BOOLOID, -1, 0);
TupleDescInitEntry(tupdesc, (AttrNumber) 8,
"w_r_holds", BOOLOID, -1, 0);
tupdesc = BlessTupleDesc(tupdesc);
MemSet(nulls, 0, sizeof(nulls));
values[0] = BoolGetDatum(strong_implied_by);
values[1] = BoolGetDatum(weak_implied_by);
values[2] = BoolGetDatum(strong_refuted_by);
values[3] = BoolGetDatum(weak_refuted_by);
values[4] = BoolGetDatum(s_i_holds);
values[5] = BoolGetDatum(w_i_holds);
values[6] = BoolGetDatum(s_r_holds);
values[7] = BoolGetDatum(w_r_holds);
PG_RETURN_DATUM(HeapTupleGetDatum(heap_form_tuple(tupdesc, values, nulls)));
}

View File

@ -0,0 +1,4 @@
comment = 'Test code for optimizer/util/predtest.c'
default_version = '1.0'
module_pathname = '$libdir/test_predtest'
relocatable = true