PostgreSQL Source Code git master
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Macros Pages
test_predtest.c File Reference
#include "postgres.h"
#include "access/htup_details.h"
#include "catalog/pg_type.h"
#include "executor/spi.h"
#include "funcapi.h"
#include "nodes/makefuncs.h"
#include "optimizer/optimizer.h"
#include "utils/builtins.h"
Include dependency graph for test_predtest.c:

Go to the source code of this file.

Functions

 PG_FUNCTION_INFO_V1 (test_predtest)
 
Datum test_predtest (PG_FUNCTION_ARGS)
 

Variables

 PG_MODULE_MAGIC
 

Function Documentation

◆ PG_FUNCTION_INFO_V1()

PG_FUNCTION_INFO_V1 ( test_predtest  )

◆ test_predtest()

Datum test_predtest ( PG_FUNCTION_ARGS  )

Definition at line 32 of file test_predtest.c.

33{
34 text *txt = PG_GETARG_TEXT_PP(0);
35 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;
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 bool nulls[8] = {0};
54 int i;
55
56 /* We use SPI to parse, plan, and execute the test query */
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 spiplan = SPI_prepare(query_string, 0, NULL);
66 if (spiplan == NULL)
67 elog(ERROR, "SPI_prepare failed for \"%s\"", query_string);
68
69 spirc = SPI_execute_plan(spiplan, NULL, NULL, true, 0);
70 if (spirc != SPI_OK_SELECT)
71 elog(ERROR, "failed to execute \"%s\"", query_string);
72 tupdesc = SPI_tuptable->tupdesc;
73 if (tupdesc->natts != 2 ||
74 TupleDescAttr(tupdesc, 0)->atttypid != BOOLOID ||
75 TupleDescAttr(tupdesc, 1)->atttypid != BOOLOID)
76 elog(ERROR, "test_predtest query must yield two boolean columns");
77
78 s_i_holds = w_i_holds = s_r_holds = w_r_holds = true;
79 for (i = 0; i < SPI_processed; i++)
80 {
82 Datum dat;
83 bool isnull;
84 char c1,
85 c2;
86
87 /* Extract column values in a 3-way representation */
88 dat = SPI_getbinval(tup, tupdesc, 1, &isnull);
89 if (isnull)
90 c1 = 'n';
91 else if (DatumGetBool(dat))
92 c1 = 't';
93 else
94 c1 = 'f';
95
96 dat = SPI_getbinval(tup, tupdesc, 2, &isnull);
97 if (isnull)
98 c2 = 'n';
99 else if (DatumGetBool(dat))
100 c2 = 't';
101 else
102 c2 = 'f';
103
104 /* Check for violations of various proof conditions */
105
106 /* strong implication: truth of c2 implies truth of c1 */
107 if (c2 == 't' && c1 != 't')
108 s_i_holds = false;
109 /* weak implication: non-falsity of c2 implies non-falsity of c1 */
110 if (c2 != 'f' && c1 == 'f')
111 w_i_holds = false;
112 /* strong refutation: truth of c2 implies falsity of c1 */
113 if (c2 == 't' && c1 != 'f')
114 s_r_holds = false;
115 /* weak refutation: truth of c2 implies non-truth of c1 */
116 if (c2 == 't' && c1 == 't')
117 w_r_holds = false;
118 }
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 if (s_r_holds && !w_r_holds)
134 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 cplan = SPI_plan_get_cached_plan(spiplan);
141
142 if (cplan == NULL || list_length(cplan->stmt_list) != 1)
143 elog(ERROR, "test_predtest query string must contain exactly one query");
145 if (stmt->commandType != CMD_SELECT)
146 elog(ERROR, "test_predtest query must be a SELECT");
147 plan = stmt->planTree;
148 Assert(list_length(plan->targetlist) >= 2);
149 clause1 = linitial_node(TargetEntry, plan->targetlist)->expr;
150 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 clause1 = (Expr *) make_ands_implicit(clause1);
167 clause2 = (Expr *) make_ands_implicit(clause2);
168
169 strong_implied_by = predicate_implied_by((List *) clause1,
170 (List *) clause2,
171 false);
172
173 weak_implied_by = predicate_implied_by((List *) clause1,
174 (List *) clause2,
175 true);
176
177 strong_refuted_by = predicate_refuted_by((List *) clause1,
178 (List *) clause2,
179 false);
180
181 weak_refuted_by = predicate_refuted_by((List *) clause1,
182 (List *) clause2,
183 true);
184
185 /*
186 * Issue warning if any proof is demonstrably incorrect.
187 */
188 if (strong_implied_by && !s_i_holds)
189 elog(WARNING, "strong_implied_by result is incorrect");
190 if (weak_implied_by && !w_i_holds)
191 elog(WARNING, "weak_implied_by result is incorrect");
192 if (strong_refuted_by && !s_r_holds)
193 elog(WARNING, "strong_refuted_by result is incorrect");
194 if (weak_refuted_by && !w_r_holds)
195 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 if (strong_refuted_by && !weak_refuted_by)
208 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 if (SPI_finish() != SPI_OK_FINISH)
214 elog(ERROR, "SPI_finish failed");
215
216 tupdesc = CreateTemplateTupleDesc(8);
217 TupleDescInitEntry(tupdesc, (AttrNumber) 1,
218 "strong_implied_by", BOOLOID, -1, 0);
219 TupleDescInitEntry(tupdesc, (AttrNumber) 2,
220 "weak_implied_by", BOOLOID, -1, 0);
221 TupleDescInitEntry(tupdesc, (AttrNumber) 3,
222 "strong_refuted_by", BOOLOID, -1, 0);
223 TupleDescInitEntry(tupdesc, (AttrNumber) 4,
224 "weak_refuted_by", BOOLOID, -1, 0);
225 TupleDescInitEntry(tupdesc, (AttrNumber) 5,
226 "s_i_holds", BOOLOID, -1, 0);
227 TupleDescInitEntry(tupdesc, (AttrNumber) 6,
228 "w_i_holds", BOOLOID, -1, 0);
229 TupleDescInitEntry(tupdesc, (AttrNumber) 7,
230 "s_r_holds", BOOLOID, -1, 0);
231 TupleDescInitEntry(tupdesc, (AttrNumber) 8,
232 "w_r_holds", BOOLOID, -1, 0);
233 tupdesc = BlessTupleDesc(tupdesc);
234
235 values[0] = BoolGetDatum(strong_implied_by);
236 values[1] = BoolGetDatum(weak_implied_by);
237 values[2] = BoolGetDatum(strong_refuted_by);
238 values[3] = BoolGetDatum(weak_refuted_by);
239 values[4] = BoolGetDatum(s_i_holds);
240 values[5] = BoolGetDatum(w_i_holds);
241 values[6] = BoolGetDatum(s_r_holds);
242 values[7] = BoolGetDatum(w_r_holds);
243
245}
int16 AttrNumber
Definition: attnum.h:21
static Datum values[MAXATTR]
Definition: bootstrap.c:151
#define Assert(condition)
Definition: c.h:815
#define WARNING
Definition: elog.h:36
#define ERROR
Definition: elog.h:39
#define elog(elevel,...)
Definition: elog.h:225
TupleDesc BlessTupleDesc(TupleDesc tupdesc)
Definition: execTuples.c:2258
#define PG_GETARG_TEXT_PP(n)
Definition: fmgr.h:309
#define PG_RETURN_DATUM(x)
Definition: fmgr.h:353
static Datum HeapTupleGetDatum(const HeapTupleData *tuple)
Definition: funcapi.h:230
HeapTuple heap_form_tuple(TupleDesc tupleDescriptor, const Datum *values, const bool *isnull)
Definition: heaptuple.c:1117
#define stmt
Definition: indent_codes.h:59
int i
Definition: isn.c:72
List * make_ands_implicit(Expr *clause)
Definition: makefuncs.c:763
@ CMD_SELECT
Definition: nodes.h:265
static int list_length(const List *l)
Definition: pg_list.h:152
#define linitial_node(type, l)
Definition: pg_list.h:181
#define lsecond_node(type, l)
Definition: pg_list.h:186
#define plan(x)
Definition: pg_regress.c:161
static bool DatumGetBool(Datum X)
Definition: postgres.h:95
uintptr_t Datum
Definition: postgres.h:69
static Datum BoolGetDatum(bool X)
Definition: postgres.h:107
bool predicate_refuted_by(List *predicate_list, List *clause_list, bool weak)
Definition: predtest.c:222
bool predicate_implied_by(List *predicate_list, List *clause_list, bool weak)
Definition: predtest.c:152
uint64 SPI_processed
Definition: spi.c:44
SPITupleTable * SPI_tuptable
Definition: spi.c:45
int SPI_connect(void)
Definition: spi.c:94
int SPI_finish(void)
Definition: spi.c:182
int SPI_execute_plan(SPIPlanPtr plan, Datum *Values, const char *Nulls, bool read_only, long tcount)
Definition: spi.c:672
CachedPlan * SPI_plan_get_cached_plan(SPIPlanPtr plan)
Definition: spi.c:2076
SPIPlanPtr SPI_prepare(const char *src, int nargs, Oid *argtypes)
Definition: spi.c:860
Datum SPI_getbinval(HeapTuple tuple, TupleDesc tupdesc, int fnumber, bool *isnull)
Definition: spi.c:1252
#define SPI_OK_FINISH
Definition: spi.h:83
#define SPI_OK_SELECT
Definition: spi.h:86
List * stmt_list
Definition: plancache.h:150
Definition: pg_list.h:54
TupleDesc tupdesc
Definition: spi.h:25
HeapTuple * vals
Definition: spi.h:26
Definition: c.h:644
TupleDesc CreateTemplateTupleDesc(int natts)
Definition: tupdesc.c:164
void TupleDescInitEntry(TupleDesc desc, AttrNumber attributeNumber, const char *attributeName, Oid oidtypeid, int32 typmod, int attdim)
Definition: tupdesc.c:798
static FormData_pg_attribute * TupleDescAttr(TupleDesc tupdesc, int i)
Definition: tupdesc.h:153
char * text_to_cstring(const text *t)
Definition: varlena.c:217

References Assert, BlessTupleDesc(), BoolGetDatum(), CMD_SELECT, CreateTemplateTupleDesc(), DatumGetBool(), elog, ERROR, heap_form_tuple(), HeapTupleGetDatum(), i, linitial_node, list_length(), lsecond_node, make_ands_implicit(), TupleDescData::natts, PG_GETARG_TEXT_PP, PG_RETURN_DATUM, plan, predicate_implied_by(), predicate_refuted_by(), SPI_connect(), SPI_execute_plan(), SPI_finish(), SPI_getbinval(), SPI_OK_FINISH, SPI_OK_SELECT, SPI_plan_get_cached_plan(), SPI_prepare(), SPI_processed, SPI_tuptable, stmt, CachedPlan::stmt_list, text_to_cstring(), SPITupleTable::tupdesc, TupleDescAttr(), TupleDescInitEntry(), SPITupleTable::vals, values, and WARNING.

Variable Documentation

◆ PG_MODULE_MAGIC

PG_MODULE_MAGIC

Definition at line 24 of file test_predtest.c.