33{
37 int spirc;
39 bool s_i_holds,
40 w_i_holds,
41 s_r_holds,
42 w_r_holds;
48 bool strong_implied_by,
49 weak_implied_by,
50 strong_refuted_by,
51 weak_refuted_by;
53 bool nulls[8] = {0};
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 */
66 if (spiplan == NULL)
67 elog(
ERROR,
"SPI_prepare failed for \"%s\"", query_string);
68
71 elog(
ERROR,
"failed to execute \"%s\"", query_string);
73 if (tupdesc->
natts != 2 ||
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;
80 {
83 bool isnull;
84 char c1,
85 c2;
86
87 /* Extract column values in a 3-way representation */
89 if (isnull)
90 c1 = 'n';
92 c1 = 't';
93 else
94 c1 = 'f';
95
97 if (isnull)
98 c2 = 'n';
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 */
141
143 elog(
ERROR,
"test_predtest query string must contain exactly one query");
146 elog(
ERROR,
"test_predtest query must be a SELECT");
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 */
168
171 false);
172
175 true);
176
179 false);
180
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 */
215
218 "strong_implied_by", BOOLOID, -1, 0);
220 "weak_implied_by", BOOLOID, -1, 0);
222 "strong_refuted_by", BOOLOID, -1, 0);
224 "weak_refuted_by", BOOLOID, -1, 0);
226 "s_i_holds", BOOLOID, -1, 0);
228 "w_i_holds", BOOLOID, -1, 0);
230 "s_r_holds", BOOLOID, -1, 0);
232 "w_r_holds", BOOLOID, -1, 0);
234
243
245}
static Datum values[MAXATTR]
TupleDesc BlessTupleDesc(TupleDesc tupdesc)
#define PG_GETARG_TEXT_PP(n)
#define PG_RETURN_DATUM(x)
static Datum HeapTupleGetDatum(const HeapTupleData *tuple)
Assert(PointerIsAligned(start, uint64))
HeapTuple heap_form_tuple(TupleDesc tupleDescriptor, const Datum *values, const bool *isnull)
List * make_ands_implicit(Expr *clause)
static int list_length(const List *l)
#define linitial_node(type, l)
#define lsecond_node(type, l)
static bool DatumGetBool(Datum X)
static Datum BoolGetDatum(bool X)
bool predicate_refuted_by(List *predicate_list, List *clause_list, bool weak)
bool predicate_implied_by(List *predicate_list, List *clause_list, bool weak)
SPITupleTable * SPI_tuptable
int SPI_execute_plan(SPIPlanPtr plan, Datum *Values, const char *Nulls, bool read_only, long tcount)
CachedPlan * SPI_plan_get_cached_plan(SPIPlanPtr plan)
SPIPlanPtr SPI_prepare(const char *src, int nargs, Oid *argtypes)
Datum SPI_getbinval(HeapTuple tuple, TupleDesc tupdesc, int fnumber, bool *isnull)
TupleDesc CreateTemplateTupleDesc(int natts)
void TupleDescInitEntry(TupleDesc desc, AttrNumber attributeNumber, const char *attributeName, Oid oidtypeid, int32 typmod, int attdim)
static FormData_pg_attribute * TupleDescAttr(TupleDesc tupdesc, int i)
char * text_to_cstring(const text *t)