-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathLogiqlDebugSolver.tex
140 lines (118 loc) · 7.85 KB
/
LogiqlDebugSolver.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{parskip}
\usepackage{listings}
\title{test}
\author{jianchuli0624 }
\date{February 2015}
\usepackage{natbib}
\usepackage{graphicx}
\begin{document}
%\maketitle
%\section{Introduction}
\section{encoding}
\subsection{Introduction}
For the type system that contains "Ostrusted" and "Osuntrusted" two types, every slot could be annotated either one of these two types. After running a program with checker-framework-inference we could get the constraints between two or three slots. In order to get the actual annotation for each slot, we can encode these derived constraints in Logiql queries, and the database will compute the every slot's annotation.
In the following part, we will introduce how to encode all these constrains, and in the end we will show you an example.
\subsection{Basic encoding}
In order to encode every constraint appropriately, we need to create some auxiliary predicates for slots and annotations.
First, a predicate called "Variable" is created for every slots.
\begin{lstlisting}
Variable(v),hasVariableName(v:i)->int(i).
\end{lstlisting}
This statement means that predicate Variable is entity type, and hasVariableName is a refmode predicate for it. Every slot has exactly one name, and the name is represented by a integer.
Then we create a predicate called AnnotationOf.
\begin{lstlisting}
AnnotationOf[v] = a ->Variable(v),string(a).
\end{lstlisting}
This statement means if the annotation of v is a, then v is a variable and a is a string. This predicate will store the final result we want, if we use the statement
\begin{lstlisting}
print AnnotationOf
\end{lstlisting}
we can see all slots' annotation.
Next, we will show another predicate called isAnnotatedTrusted:
\begin{lstlisting}
isAnnotatedTrusted[v]=i->Variable(v),boolean(i).
\end{lstlisting}
For every slot, if the annotation of it is Ostrusted, the boolean value i will be true, if the annotation of it is Osuntrusted, the boolean value i will be false.
So in predicate isAnnotatedTrusted, we can get the "boolean form" of every variable's annotation, then we need to transform the "boolean form" to "string form", which is the final result we want. The following statements can perform this transformation.
\begin{lstlisting}
AnnotationOf[v]="Ostrusted"<-isAnnotatedTrusted[v]=true.
AnnotationOf[v]="Osuntrusted"<-isAnnotatedTrusted[v]=false.
\end{lstlisting}
These two statements mean if a variable's boolean value in predicate isAnnotatedTrusted is true (false), then the annotation of this variable is "Ostrusted"("Osuntrusted").
The last auxiliary predicate is called SpecialVariable:
\begin{lstlisting}
SpecialVariable[v]=sv->Variable(v),string(sv).
\end{lstlisting}
Here, we set two special -1 and -2, and at the beginning, we need insert the two special variables to this predicate:
\begin{lstlisting}
+Variable(-1).
+Variable(-2).
+SpecialVariable[-1]="Ostrusted".
+SpecialVariable[-2]="Osuntrusted".
\end{lstlisting}
We use -1 denote the annotation "Ostrusted", and use -2 denote "Osuntrusted".
Meanwhile the below assignment is also necessary:
\begin{lstlisting}
isAnnotatedTrusted[v]=true <- hasVariableName(v:-1).
isAnnotatedTrusted[v]=false <- hasVariableName(v:-2).
\end{lstlisting}
The reason of we do this is that for the output from checker-framework-inference, there may be some outputs like:
\begin{lstlisting}[breaklines=true]
EqualityConstraint:[@ostrusted.quals.OsTrusted,VariableSlot(1)]
\end{lstlisting}
That means for variable 1, we need to set the annotation of it be "Ostrusted" first of all. Together with the encoding of equality constraint, which will be introduced below, we can use the special variable to set the annotation of variable 1 be "Ostrusted":
\begin{lstlisting}
+Equality[1,-1]=true.
\end{lstlisting}
And if we want to set annotation of variable 1 be false, we can use the statement:
\begin{lstlisting}
+Equality[1,-2]=true.
\end{lstlisting}
\subsection{Equality constraint}
Now, we can focus on every constraint. First we will look at equality constraint.
If the output from checker-framework-inference contains statement like:
\begin{lstlisting}
EqualityConstraint:[VariableSlot(0),VariableSlot(1)]
\end{lstlisting}
This means the annotation of variable 0 and variable 1 are the same.
We can encode this constraint to logiql in this way:
\begin{lstlisting}[breaklines=true]
EqualityConstraint[v1,v2]=e-> Variable(v1),Variable(v2),boolean(e).
isAnnotatedTrusted[v2]=true <- isAnnotatedTrusted[v1]=true, EqualityConstraint[v1,v2]=true.
isAnnotatedTrusted[v2]=false <- isAnnotatedTrusted[v1]=false, EqualityConstraint[v1,v2]=true.
isAnnotatedTrusted[v2]=true <- isAnnotatedTrusted[v1]=true, EqualityConstraint[v2,v1]=true.
isAnnotatedTrusted[v2]=false <- isAnnotatedTrusted[v1]=false, EqualityConstraint[v2,v1]=true.
\end{lstlisting}
The first statement means that if the annotation of variable v1 is equal to the annotation of variable v2, then the boolean value e would be set true. And the following four statements ensure that if the annotation of two variables are same, and if we have already know one variable's annotation, we can get another variable's annotation, and save the result into predicate isAnnotatedTrusted.
\subsection{Inequality constraint}
In this part, we will consider about inequality constraint. If there are some outputs from checker-framework-inference like
\begin{lstlisting}
InequalityConstraint: [VariableSlot(0),VariableSlot(1)]
\end{lstlisting}
This means the annotation of variable 0 and variable 1 are different.
We can encode this constraint to logiql in this way:
\begin{lstlisting}[breaklines=true]
InequalityConstraint[v1,v2]=n->Variable(v1),Variable(v2),boolean(n).
isAnnotatedTrusted[v2]=false <- isAnnotatedTrusted[v1]=true, InequalityConstraint[v1,v2]=true.
isAnnotatedTrusted[v2]=true <- isAnnotatedTrusted[v1]=false, InequalityConstraint[v1,v2]=true.
isAnnotatedTrusted[v2]=false <- isAnnotatedTrusted[v1]=true, InequalityConstraint[v2,v1]=true.
isAnnotatedTrusted[v2]=true <- isAnnotatedTrusted[v1]=false, InequalityConstraint[v2,v1]=true.
\end{lstlisting}
The first statement means that if the annotation of variable v1 is not equal to the annotation of variable v2, then the boolean value e would be set true. And the following four statements ensure that if the annotation of two variables are different, and if we have already known one variable's annotation, we can get another variable's annotation, and save the result into predicate isAnnotatedTrusted.
\subsection{Subtype constraint}
There is another constraint called subtype constraint, the form of this constraint output by checker-framework-inference is
\begin{lstlisting}
SubtypeConstraint: [VariableSlot(0),VariableSlot(1)]
\end{lstlisting}
This means that the annotation of variable 0 is the subtype of the annotation of variable 1. The encoding is shown below:
\begin{lstlisting}[breaklines=true]
SubtypeConstraint[v2,v1] = s -> Variable(v1),Variable(v2),boolean(s).
isAnnotatedTrusted[v2]=true <- isAnnotatedTrusted[v1]=true, SubtypeConstraint[v2,v1]=true.
isAnnotatedTrusted[v2]=false <- isAnnotatedTrusted[v1]=false, SubtypeConstraint[v1,v2]=true.
\end{lstlisting}
The first statement says that if the annotation of variable v2 is the subtype of annotation of variable v1, then the boolean value s would be set true.
And the following two statement ensure that if the annotation of variable v2 is the subtype of the annotation of variable v1, and the annotation of variable v1 is Ostrusted, then the annotation of variable v2 is also Ostrusted. Another condition is that if the annotation of variable v1 is the subtype of the annotation of variable v2, and the annotation of variable v1 is Osuntrusted, then the annotation of variable v2 is also Osuntrusted. The reason we encode the constaint in this way is that in this type system, the subtype of Ostrusted could only be Ostrusted, and the supertype of Osuntrusted could only be Osuntrusted.
\subsection{example}
\end{document}