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