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-2023, 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 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];
53 GNC 74 : bool nulls[8] = {0};
54 : int i;
55 :
56 : /* We use SPI to parse, plan, and execute the test query */
57 CBC 74 : if (SPI_connect() != SPI_OK_CONNECT)
58 UBC 0 : elog(ERROR, "SPI_connect failed");
59 :
60 : /*
61 : * First, plan and execute the query, and inspect the results. To the
62 : * extent that the query fully exercises the two expressions, this
63 : * provides an experimental indication of whether implication or
64 : * refutation holds.
65 : */
66 CBC 74 : spiplan = SPI_prepare(query_string, 0, NULL);
67 74 : if (spiplan == NULL)
68 UBC 0 : elog(ERROR, "SPI_prepare failed for \"%s\"", query_string);
69 :
70 CBC 74 : spirc = SPI_execute_plan(spiplan, NULL, NULL, true, 0);
71 74 : if (spirc != SPI_OK_SELECT)
72 UBC 0 : elog(ERROR, "failed to execute \"%s\"", query_string);
73 CBC 74 : tupdesc = SPI_tuptable->tupdesc;
74 74 : if (tupdesc->natts != 2 ||
75 74 : TupleDescAttr(tupdesc, 0)->atttypid != BOOLOID ||
76 74 : TupleDescAttr(tupdesc, 1)->atttypid != BOOLOID)
77 UBC 0 : elog(ERROR, "query must yield two boolean columns");
78 :
79 CBC 74 : s_i_holds = w_i_holds = s_r_holds = w_r_holds = true;
80 7550 : for (i = 0; i < SPI_processed; i++)
81 : {
82 7476 : HeapTuple tup = SPI_tuptable->vals[i];
83 : Datum dat;
84 : bool isnull;
85 : char c1,
86 : c2;
87 :
88 : /* Extract column values in a 3-way representation */
89 7476 : dat = SPI_getbinval(tup, tupdesc, 1, &isnull);
90 7476 : if (isnull)
91 1154 : c1 = 'n';
92 6322 : else if (DatumGetBool(dat))
93 3126 : c1 = 't';
94 : else
95 3196 : c1 = 'f';
96 :
97 7476 : dat = SPI_getbinval(tup, tupdesc, 2, &isnull);
98 7476 : if (isnull)
99 1192 : c2 = 'n';
100 6284 : else if (DatumGetBool(dat))
101 2620 : c2 = 't';
102 : else
103 3664 : c2 = 'f';
104 :
105 : /* Check for violations of various proof conditions */
106 :
107 : /* strong implication: truth of c2 implies truth of c1 */
108 7476 : if (c2 == 't' && c1 != 't')
109 1366 : s_i_holds = false;
110 : /* weak implication: non-falsity of c2 implies non-falsity of c1 */
111 7476 : if (c2 != 'f' && c1 == 'f')
112 1420 : w_i_holds = false;
113 : /* strong refutation: truth of c2 implies falsity of c1 */
114 7476 : if (c2 == 't' && c1 != 'f')
115 1452 : s_r_holds = false;
116 : /* weak refutation: truth of c2 implies non-truth of c1 */
117 7476 : if (c2 == 't' && c1 == 't')
118 1254 : w_r_holds = false;
119 : }
120 :
121 : /*
122 : * Now, dig the clause querytrees out of the plan, and see what predtest.c
123 : * does with them.
124 : */
125 74 : cplan = SPI_plan_get_cached_plan(spiplan);
126 :
127 74 : if (list_length(cplan->stmt_list) != 1)
128 UBC 0 : elog(ERROR, "failed to decipher query plan");
129 CBC 74 : stmt = linitial_node(PlannedStmt, cplan->stmt_list);
130 74 : if (stmt->commandType != CMD_SELECT)
131 UBC 0 : elog(ERROR, "failed to decipher query plan");
132 CBC 74 : plan = stmt->planTree;
133 74 : Assert(list_length(plan->targetlist) >= 2);
134 74 : clause1 = linitial_node(TargetEntry, plan->targetlist)->expr;
135 74 : clause2 = lsecond_node(TargetEntry, plan->targetlist)->expr;
136 :
137 : /*
138 : * Because the clauses are in the SELECT list, preprocess_expression did
139 : * not pass them through canonicalize_qual nor make_ands_implicit.
140 : *
141 : * We can't do canonicalize_qual here, since it's unclear whether the
142 : * expressions ought to be treated as WHERE or CHECK clauses. Fortunately,
143 : * useful test expressions wouldn't be affected by those transformations
144 : * anyway. We should do make_ands_implicit, though.
145 : *
146 : * Another way in which this does not exactly duplicate the normal usage
147 : * of the proof functions is that they are often given qual clauses
148 : * containing RestrictInfo nodes. But since predtest.c just looks through
149 : * those anyway, it seems OK to not worry about that point.
150 : */
151 74 : clause1 = (Expr *) make_ands_implicit(clause1);
152 74 : clause2 = (Expr *) make_ands_implicit(clause2);
153 :
154 74 : strong_implied_by = predicate_implied_by((List *) clause1,
155 : (List *) clause2,
156 : false);
157 :
158 74 : weak_implied_by = predicate_implied_by((List *) clause1,
159 : (List *) clause2,
160 : true);
161 :
162 74 : strong_refuted_by = predicate_refuted_by((List *) clause1,
163 : (List *) clause2,
164 : false);
165 :
166 74 : weak_refuted_by = predicate_refuted_by((List *) clause1,
167 : (List *) clause2,
168 : true);
169 :
170 : /*
171 : * Issue warning if any proof is demonstrably incorrect.
172 : */
173 74 : if (strong_implied_by && !s_i_holds)
174 UBC 0 : elog(WARNING, "strong_implied_by result is incorrect");
175 CBC 74 : if (weak_implied_by && !w_i_holds)
176 UBC 0 : elog(WARNING, "weak_implied_by result is incorrect");
177 CBC 74 : if (strong_refuted_by && !s_r_holds)
178 UBC 0 : elog(WARNING, "strong_refuted_by result is incorrect");
179 CBC 74 : if (weak_refuted_by && !w_r_holds)
180 UBC 0 : elog(WARNING, "weak_refuted_by result is incorrect");
181 :
182 : /*
183 : * Clean up and return a record of the results.
184 : */
185 CBC 74 : if (SPI_finish() != SPI_OK_FINISH)
186 UBC 0 : elog(ERROR, "SPI_finish failed");
187 :
188 CBC 74 : tupdesc = CreateTemplateTupleDesc(8);
189 74 : TupleDescInitEntry(tupdesc, (AttrNumber) 1,
190 : "strong_implied_by", BOOLOID, -1, 0);
191 74 : TupleDescInitEntry(tupdesc, (AttrNumber) 2,
192 : "weak_implied_by", BOOLOID, -1, 0);
193 74 : TupleDescInitEntry(tupdesc, (AttrNumber) 3,
194 : "strong_refuted_by", BOOLOID, -1, 0);
195 74 : TupleDescInitEntry(tupdesc, (AttrNumber) 4,
196 : "weak_refuted_by", BOOLOID, -1, 0);
197 74 : TupleDescInitEntry(tupdesc, (AttrNumber) 5,
198 : "s_i_holds", BOOLOID, -1, 0);
199 74 : TupleDescInitEntry(tupdesc, (AttrNumber) 6,
200 : "w_i_holds", BOOLOID, -1, 0);
201 74 : TupleDescInitEntry(tupdesc, (AttrNumber) 7,
202 : "s_r_holds", BOOLOID, -1, 0);
203 74 : TupleDescInitEntry(tupdesc, (AttrNumber) 8,
204 : "w_r_holds", BOOLOID, -1, 0);
205 74 : tupdesc = BlessTupleDesc(tupdesc);
206 :
207 74 : values[0] = BoolGetDatum(strong_implied_by);
208 74 : values[1] = BoolGetDatum(weak_implied_by);
209 74 : values[2] = BoolGetDatum(strong_refuted_by);
210 74 : values[3] = BoolGetDatum(weak_refuted_by);
211 74 : values[4] = BoolGetDatum(s_i_holds);
212 74 : values[5] = BoolGetDatum(w_i_holds);
213 74 : values[6] = BoolGetDatum(s_r_holds);
214 GIC 74 : values[7] = BoolGetDatum(w_r_holds);
215 ECB :
216 GIC 74 : PG_RETURN_DATUM(HeapTupleGetDatum(heap_form_tuple(tupdesc, values, nulls)));
217 : }
|
