Line data Source code
1 : /*--------------------------------------------------------------------------
2 : *
3 : * test_predtest.c
4 : * Test correctness of optimizer's predicate proof logic.
5 : *
6 : * Copyright (c) 2018-2026, PostgreSQL Global Development Group
7 : *
8 : * IDENTIFICATION
9 : * src/test/modules/test_predtest/test_predtest.c
10 : *
11 : * -------------------------------------------------------------------------
12 : */
13 :
14 : #include "postgres.h"
15 :
16 : #include "access/htup_details.h"
17 : #include "catalog/pg_type.h"
18 : #include "executor/spi.h"
19 : #include "funcapi.h"
20 : #include "nodes/makefuncs.h"
21 : #include "optimizer/optimizer.h"
22 : #include "utils/builtins.h"
23 :
24 0 : PG_MODULE_MAGIC;
25 :
26 : /*
27 : * test_predtest(query text) returns record
28 : */
29 0 : PG_FUNCTION_INFO_V1(test_predtest);
30 :
31 : Datum
32 0 : test_predtest(PG_FUNCTION_ARGS)
33 : {
34 0 : text *txt = PG_GETARG_TEXT_PP(0);
35 0 : char *query_string = text_to_cstring(txt);
36 0 : SPIPlanPtr spiplan;
37 0 : int spirc;
38 0 : TupleDesc tupdesc;
39 0 : bool s_i_holds,
40 : w_i_holds,
41 : s_r_holds,
42 : w_r_holds;
43 0 : CachedPlan *cplan;
44 0 : PlannedStmt *stmt;
45 0 : Plan *plan;
46 0 : Expr *clause1;
47 0 : Expr *clause2;
48 0 : bool strong_implied_by,
49 : weak_implied_by,
50 : strong_refuted_by,
51 : weak_refuted_by;
52 0 : Datum values[8];
53 0 : bool nulls[8] = {0};
54 0 : int i;
55 :
56 : /* We use SPI to parse, plan, and execute the test query */
57 0 : SPI_connect();
58 :
59 : /*
60 : * First, plan and execute the query, and inspect the results. To the
61 : * extent that the query fully exercises the two expressions, this
62 : * provides an experimental indication of whether implication or
63 : * refutation holds.
64 : */
65 0 : spiplan = SPI_prepare(query_string, 0, NULL);
66 0 : if (spiplan == NULL)
67 0 : elog(ERROR, "SPI_prepare failed for \"%s\"", query_string);
68 :
69 0 : spirc = SPI_execute_plan(spiplan, NULL, NULL, true, 0);
70 0 : if (spirc != SPI_OK_SELECT)
71 0 : elog(ERROR, "failed to execute \"%s\"", query_string);
72 0 : tupdesc = SPI_tuptable->tupdesc;
73 0 : if (tupdesc->natts != 2 ||
74 0 : TupleDescAttr(tupdesc, 0)->atttypid != BOOLOID ||
75 0 : TupleDescAttr(tupdesc, 1)->atttypid != BOOLOID)
76 0 : elog(ERROR, "test_predtest query must yield two boolean columns");
77 :
78 0 : s_i_holds = w_i_holds = s_r_holds = w_r_holds = true;
79 0 : for (i = 0; i < SPI_processed; i++)
80 : {
81 0 : HeapTuple tup = SPI_tuptable->vals[i];
82 0 : Datum dat;
83 0 : bool isnull;
84 0 : char c1,
85 : c2;
86 :
87 : /* Extract column values in a 3-way representation */
88 0 : dat = SPI_getbinval(tup, tupdesc, 1, &isnull);
89 0 : if (isnull)
90 0 : c1 = 'n';
91 0 : else if (DatumGetBool(dat))
92 0 : c1 = 't';
93 : else
94 0 : c1 = 'f';
95 :
96 0 : dat = SPI_getbinval(tup, tupdesc, 2, &isnull);
97 0 : if (isnull)
98 0 : c2 = 'n';
99 0 : else if (DatumGetBool(dat))
100 0 : c2 = 't';
101 : else
102 0 : c2 = 'f';
103 :
104 : /* Check for violations of various proof conditions */
105 :
106 : /* strong implication: truth of c2 implies truth of c1 */
107 0 : if (c2 == 't' && c1 != 't')
108 0 : s_i_holds = false;
109 : /* weak implication: non-falsity of c2 implies non-falsity of c1 */
110 0 : if (c2 != 'f' && c1 == 'f')
111 0 : w_i_holds = false;
112 : /* strong refutation: truth of c2 implies falsity of c1 */
113 0 : if (c2 == 't' && c1 != 'f')
114 0 : s_r_holds = false;
115 : /* weak refutation: truth of c2 implies non-truth of c1 */
116 0 : if (c2 == 't' && c1 == 't')
117 0 : w_r_holds = false;
118 0 : }
119 :
120 : /*
121 : * Strong refutation implies weak refutation, so we should never observe
122 : * s_r_holds = true with w_r_holds = false.
123 : *
124 : * We can't make a comparable assertion for implication since moving from
125 : * strong to weak implication expands the allowed values of "A" from true
126 : * to either true or NULL.
127 : *
128 : * If this fails it constitutes a bug not with the proofs but with either
129 : * this test module or a more core part of expression evaluation since we
130 : * are validating the logical correctness of the observed result rather
131 : * than the proof.
132 : */
133 0 : if (s_r_holds && !w_r_holds)
134 0 : elog(WARNING, "s_r_holds was true; w_r_holds must not be false");
135 :
136 : /*
137 : * Now, dig the clause querytrees out of the plan, and see what predtest.c
138 : * does with them.
139 : */
140 0 : cplan = SPI_plan_get_cached_plan(spiplan);
141 :
142 0 : if (cplan == NULL || list_length(cplan->stmt_list) != 1)
143 0 : elog(ERROR, "test_predtest query string must contain exactly one query");
144 0 : stmt = linitial_node(PlannedStmt, cplan->stmt_list);
145 0 : if (stmt->commandType != CMD_SELECT)
146 0 : elog(ERROR, "test_predtest query must be a SELECT");
147 0 : plan = stmt->planTree;
148 0 : Assert(list_length(plan->targetlist) >= 2);
149 0 : clause1 = linitial_node(TargetEntry, plan->targetlist)->expr;
150 0 : clause2 = lsecond_node(TargetEntry, plan->targetlist)->expr;
151 :
152 : /*
153 : * Because the clauses are in the SELECT list, preprocess_expression did
154 : * not pass them through canonicalize_qual nor make_ands_implicit.
155 : *
156 : * We can't do canonicalize_qual here, since it's unclear whether the
157 : * expressions ought to be treated as WHERE or CHECK clauses. Fortunately,
158 : * useful test expressions wouldn't be affected by those transformations
159 : * anyway. We should do make_ands_implicit, though.
160 : *
161 : * Another way in which this does not exactly duplicate the normal usage
162 : * of the proof functions is that they are often given qual clauses
163 : * containing RestrictInfo nodes. But since predtest.c just looks through
164 : * those anyway, it seems OK to not worry about that point.
165 : */
166 0 : clause1 = (Expr *) make_ands_implicit(clause1);
167 0 : clause2 = (Expr *) make_ands_implicit(clause2);
168 :
169 0 : strong_implied_by = predicate_implied_by((List *) clause1,
170 0 : (List *) clause2,
171 : false);
172 :
173 0 : weak_implied_by = predicate_implied_by((List *) clause1,
174 0 : (List *) clause2,
175 : true);
176 :
177 0 : strong_refuted_by = predicate_refuted_by((List *) clause1,
178 0 : (List *) clause2,
179 : false);
180 :
181 0 : weak_refuted_by = predicate_refuted_by((List *) clause1,
182 0 : (List *) clause2,
183 : true);
184 :
185 : /*
186 : * Issue warning if any proof is demonstrably incorrect.
187 : */
188 0 : if (strong_implied_by && !s_i_holds)
189 0 : elog(WARNING, "strong_implied_by result is incorrect");
190 0 : if (weak_implied_by && !w_i_holds)
191 0 : elog(WARNING, "weak_implied_by result is incorrect");
192 0 : if (strong_refuted_by && !s_r_holds)
193 0 : elog(WARNING, "strong_refuted_by result is incorrect");
194 0 : if (weak_refuted_by && !w_r_holds)
195 0 : elog(WARNING, "weak_refuted_by result is incorrect");
196 :
197 : /*
198 : * As with our earlier check of the logical consistency of whether strong
199 : * and weak refutation hold, we ought never prove strong refutation
200 : * without also proving weak refutation.
201 : *
202 : * Also as earlier we cannot make the same guarantee about implication
203 : * proofs.
204 : *
205 : * A warning here suggests a bug in the proof code.
206 : */
207 0 : if (strong_refuted_by && !weak_refuted_by)
208 0 : elog(WARNING, "strong_refuted_by was proven; weak_refuted_by should also be proven");
209 :
210 : /*
211 : * Clean up and return a record of the results.
212 : */
213 0 : if (SPI_finish() != SPI_OK_FINISH)
214 0 : elog(ERROR, "SPI_finish failed");
215 :
216 0 : tupdesc = CreateTemplateTupleDesc(8);
217 0 : TupleDescInitEntry(tupdesc, (AttrNumber) 1,
218 : "strong_implied_by", BOOLOID, -1, 0);
219 0 : TupleDescInitEntry(tupdesc, (AttrNumber) 2,
220 : "weak_implied_by", BOOLOID, -1, 0);
221 0 : TupleDescInitEntry(tupdesc, (AttrNumber) 3,
222 : "strong_refuted_by", BOOLOID, -1, 0);
223 0 : TupleDescInitEntry(tupdesc, (AttrNumber) 4,
224 : "weak_refuted_by", BOOLOID, -1, 0);
225 0 : TupleDescInitEntry(tupdesc, (AttrNumber) 5,
226 : "s_i_holds", BOOLOID, -1, 0);
227 0 : TupleDescInitEntry(tupdesc, (AttrNumber) 6,
228 : "w_i_holds", BOOLOID, -1, 0);
229 0 : TupleDescInitEntry(tupdesc, (AttrNumber) 7,
230 : "s_r_holds", BOOLOID, -1, 0);
231 0 : TupleDescInitEntry(tupdesc, (AttrNumber) 8,
232 : "w_r_holds", BOOLOID, -1, 0);
233 0 : tupdesc = BlessTupleDesc(tupdesc);
234 :
235 0 : values[0] = BoolGetDatum(strong_implied_by);
236 0 : values[1] = BoolGetDatum(weak_implied_by);
237 0 : values[2] = BoolGetDatum(strong_refuted_by);
238 0 : values[3] = BoolGetDatum(weak_refuted_by);
239 0 : values[4] = BoolGetDatum(s_i_holds);
240 0 : values[5] = BoolGetDatum(w_i_holds);
241 0 : values[6] = BoolGetDatum(s_r_holds);
242 0 : values[7] = BoolGetDatum(w_r_holds);
243 :
244 0 : PG_RETURN_DATUM(HeapTupleGetDatum(heap_form_tuple(tupdesc, values, nulls)));
245 0 : }
|
