PostgreSQL Source Code  git master
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 */
57  if (SPI_connect() != SPI_OK_CONNECT)
58  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  spiplan = SPI_prepare(query_string, 0, NULL);
67  if (spiplan == NULL)
68  elog(ERROR, "SPI_prepare failed for \"%s\"", query_string);
69 
70  spirc = SPI_execute_plan(spiplan, NULL, NULL, true, 0);
71  if (spirc != SPI_OK_SELECT)
72  elog(ERROR, "failed to execute \"%s\"", query_string);
73  tupdesc = SPI_tuptable->tupdesc;
74  if (tupdesc->natts != 2 ||
75  TupleDescAttr(tupdesc, 0)->atttypid != BOOLOID ||
76  TupleDescAttr(tupdesc, 1)->atttypid != BOOLOID)
77  elog(ERROR, "test_predtest query must yield two boolean columns");
78 
79  s_i_holds = w_i_holds = s_r_holds = w_r_holds = true;
80  for (i = 0; i < SPI_processed; i++)
81  {
82  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  dat = SPI_getbinval(tup, tupdesc, 1, &isnull);
90  if (isnull)
91  c1 = 'n';
92  else if (DatumGetBool(dat))
93  c1 = 't';
94  else
95  c1 = 'f';
96 
97  dat = SPI_getbinval(tup, tupdesc, 2, &isnull);
98  if (isnull)
99  c2 = 'n';
100  else if (DatumGetBool(dat))
101  c2 = 't';
102  else
103  c2 = 'f';
104 
105  /* Check for violations of various proof conditions */
106 
107  /* strong implication: truth of c2 implies truth of c1 */
108  if (c2 == 't' && c1 != 't')
109  s_i_holds = false;
110  /* weak implication: non-falsity of c2 implies non-falsity of c1 */
111  if (c2 != 'f' && c1 == 'f')
112  w_i_holds = false;
113  /* strong refutation: truth of c2 implies falsity of c1 */
114  if (c2 == 't' && c1 != 'f')
115  s_r_holds = false;
116  /* weak refutation: truth of c2 implies non-truth of c1 */
117  if (c2 == 't' && c1 == 't')
118  w_r_holds = false;
119  }
120 
121  /*
122  * Strong refutation implies weak refutation, so we should never observe
123  * s_r_holds = true with w_r_holds = false.
124  *
125  * We can't make a comparable assertion for implication since moving from
126  * strong to weak implication expands the allowed values of "A" from true
127  * to either true or NULL.
128  *
129  * If this fails it constitutes a bug not with the proofs but with either
130  * this test module or a more core part of expression evaluation since we
131  * are validating the logical correctness of the observed result rather
132  * than the proof.
133  */
134  if (s_r_holds && !w_r_holds)
135  elog(WARNING, "s_r_holds was true; w_r_holds must not be false");
136 
137  /*
138  * Now, dig the clause querytrees out of the plan, and see what predtest.c
139  * does with them.
140  */
141  cplan = SPI_plan_get_cached_plan(spiplan);
142 
143  if (cplan == NULL || list_length(cplan->stmt_list) != 1)
144  elog(ERROR, "test_predtest query string must contain exactly one query");
146  if (stmt->commandType != CMD_SELECT)
147  elog(ERROR, "test_predtest query must be a SELECT");
148  plan = stmt->planTree;
149  Assert(list_length(plan->targetlist) >= 2);
150  clause1 = linitial_node(TargetEntry, plan->targetlist)->expr;
151  clause2 = lsecond_node(TargetEntry, plan->targetlist)->expr;
152 
153  /*
154  * Because the clauses are in the SELECT list, preprocess_expression did
155  * not pass them through canonicalize_qual nor make_ands_implicit.
156  *
157  * We can't do canonicalize_qual here, since it's unclear whether the
158  * expressions ought to be treated as WHERE or CHECK clauses. Fortunately,
159  * useful test expressions wouldn't be affected by those transformations
160  * anyway. We should do make_ands_implicit, though.
161  *
162  * Another way in which this does not exactly duplicate the normal usage
163  * of the proof functions is that they are often given qual clauses
164  * containing RestrictInfo nodes. But since predtest.c just looks through
165  * those anyway, it seems OK to not worry about that point.
166  */
167  clause1 = (Expr *) make_ands_implicit(clause1);
168  clause2 = (Expr *) make_ands_implicit(clause2);
169 
170  strong_implied_by = predicate_implied_by((List *) clause1,
171  (List *) clause2,
172  false);
173 
174  weak_implied_by = predicate_implied_by((List *) clause1,
175  (List *) clause2,
176  true);
177 
178  strong_refuted_by = predicate_refuted_by((List *) clause1,
179  (List *) clause2,
180  false);
181 
182  weak_refuted_by = predicate_refuted_by((List *) clause1,
183  (List *) clause2,
184  true);
185 
186  /*
187  * Issue warning if any proof is demonstrably incorrect.
188  */
189  if (strong_implied_by && !s_i_holds)
190  elog(WARNING, "strong_implied_by result is incorrect");
191  if (weak_implied_by && !w_i_holds)
192  elog(WARNING, "weak_implied_by result is incorrect");
193  if (strong_refuted_by && !s_r_holds)
194  elog(WARNING, "strong_refuted_by result is incorrect");
195  if (weak_refuted_by && !w_r_holds)
196  elog(WARNING, "weak_refuted_by result is incorrect");
197 
198  /*
199  * As with our earlier check of the logical consistency of whether strong
200  * and weak refutation hold, we ought never prove strong refutation
201  * without also proving weak refutation.
202  *
203  * Also as earlier we cannot make the same guarantee about implication
204  * proofs.
205  *
206  * A warning here suggests a bug in the proof code.
207  */
208  if (strong_refuted_by && !weak_refuted_by)
209  elog(WARNING, "strong_refuted_by was proven; weak_refuted_by should also be proven");
210 
211  /*
212  * Clean up and return a record of the results.
213  */
214  if (SPI_finish() != SPI_OK_FINISH)
215  elog(ERROR, "SPI_finish failed");
216 
217  tupdesc = CreateTemplateTupleDesc(8);
218  TupleDescInitEntry(tupdesc, (AttrNumber) 1,
219  "strong_implied_by", BOOLOID, -1, 0);
220  TupleDescInitEntry(tupdesc, (AttrNumber) 2,
221  "weak_implied_by", BOOLOID, -1, 0);
222  TupleDescInitEntry(tupdesc, (AttrNumber) 3,
223  "strong_refuted_by", BOOLOID, -1, 0);
224  TupleDescInitEntry(tupdesc, (AttrNumber) 4,
225  "weak_refuted_by", BOOLOID, -1, 0);
226  TupleDescInitEntry(tupdesc, (AttrNumber) 5,
227  "s_i_holds", BOOLOID, -1, 0);
228  TupleDescInitEntry(tupdesc, (AttrNumber) 6,
229  "w_i_holds", BOOLOID, -1, 0);
230  TupleDescInitEntry(tupdesc, (AttrNumber) 7,
231  "s_r_holds", BOOLOID, -1, 0);
232  TupleDescInitEntry(tupdesc, (AttrNumber) 8,
233  "w_r_holds", BOOLOID, -1, 0);
234  tupdesc = BlessTupleDesc(tupdesc);
235 
236  values[0] = BoolGetDatum(strong_implied_by);
237  values[1] = BoolGetDatum(weak_implied_by);
238  values[2] = BoolGetDatum(strong_refuted_by);
239  values[3] = BoolGetDatum(weak_refuted_by);
240  values[4] = BoolGetDatum(s_i_holds);
241  values[5] = BoolGetDatum(w_i_holds);
242  values[6] = BoolGetDatum(s_r_holds);
243  values[7] = BoolGetDatum(w_r_holds);
244 
246 }
int16 AttrNumber
Definition: attnum.h:21
static Datum values[MAXATTR]
Definition: bootstrap.c:152
#define Assert(condition)
Definition: c.h:858
#define WARNING
Definition: elog.h:36
#define ERROR
Definition: elog.h:39
#define elog(elevel,...)
Definition: elog.h:224
TupleDesc BlessTupleDesc(TupleDesc tupdesc)
Definition: execTuples.c:2158
#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:1116
#define stmt
Definition: indent_codes.h:59
int i
Definition: isn.c:73
List * make_ands_implicit(Expr *clause)
Definition: makefuncs.c:737
@ 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:162
static bool DatumGetBool(Datum X)
Definition: postgres.h:90
uintptr_t Datum
Definition: postgres.h:64
static Datum BoolGetDatum(bool X)
Definition: postgres.h:102
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
CachedPlan * SPI_plan_get_cached_plan(SPIPlanPtr plan)
Definition: spi.c:2071
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:669
SPIPlanPtr SPI_prepare(const char *src, int nargs, Oid *argtypes)
Definition: spi.c:857
Datum SPI_getbinval(HeapTuple tuple, TupleDesc tupdesc, int fnumber, bool *isnull)
Definition: spi.c:1249
#define SPI_OK_CONNECT
Definition: spi.h:82
#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:687
TupleDesc CreateTemplateTupleDesc(int natts)
Definition: tupdesc.c:67
void TupleDescInitEntry(TupleDesc desc, AttrNumber attributeNumber, const char *attributeName, Oid oidtypeid, int32 typmod, int attdim)
Definition: tupdesc.c:651
#define TupleDescAttr(tupdesc, i)
Definition: tupdesc.h:92
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_CONNECT, 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.