Skip to content

Commit 97c6274

Browse files
Roman-ManevichRoman-Manevich
authored
Merge pull request #1756 from herd/aslspec-stronger-subsumption-test
[aslspec][asl reference] stronger subsumption test for function types
2 parents 0dc63ad + ebb2632 commit 97c6274

File tree

5 files changed

+76
-141
lines changed

5 files changed

+76
-141
lines changed

‎asllib/aslspec/spec.ml‎

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1237,20 +1237,21 @@ module Check = struct
12371237
(fun { term = sub_term; _ } { term = super_term; _ } ->
12381238
subsumed_rec spec expanded_types sub_term super_term)
12391239
sub_fields super_fields
1240-
| ( Function { from_type = _, sub_from_term; to_type = _, sub_to_term },
1240+
| ( Function
1241+
{
1242+
from_type = _, sub_from_term;
1243+
to_type = _, sub_to_term;
1244+
total = sub_total;
1245+
},
12411246
Function
1242-
{ from_type = _, super_from_term; to_type = _, super_to_term } )
1243-
->
1244-
(* Functions can be partial or total, which require different subsumption tests.
1245-
To make this simple, we require equivalence of the from-terms and to-terms,
1246-
which is sufficient for our needs.
1247-
*)
1248-
let equivalence_test term term' =
1249-
subsumed_rec spec expanded_types term term'
1250-
&& subsumed_rec spec expanded_types term' term
1251-
in
1252-
equivalence_test sub_from_term super_from_term
1253-
&& equivalence_test sub_to_term super_to_term
1247+
{
1248+
from_type = _, super_from_term;
1249+
to_type = _, super_to_term;
1250+
total = super_total;
1251+
} ) ->
1252+
((not sub_total) || super_total) (* sub_total implies super_total *)
1253+
&& subsumed_rec spec expanded_types super_from_term sub_from_term
1254+
&& subsumed_rec spec expanded_types sub_to_term super_to_term
12541255
| ConstantsSet sub_names, ConstantsSet super_names ->
12551256
List.for_all (fun name -> List.mem name super_names) sub_names
12561257
| _ ->

‎asllib/doc/StaticEvaluation.tex‎

Lines changed: 1 addition & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -53,25 +53,4 @@ \chapter{Static Evaluation\label{chap:StaticEvaluation}}
5353
\{ \dynamicenvsG: \{\vHALFWORDSIZE \mapsto \nvint(32)\}, \dynamicenvsL: \emptyfunc \} \enspace.
5454
\]
5555

56-
\ProseParagraph
57-
\AllApply
58-
\begin{itemize}
59-
\item define the global dynamic environment $\vglobal$ as the map that binds
60-
each $\id$ in the domain of $\tenv.\staticenvsG.\constantvalues$ to $\NVLiteral(\vl)$
61-
if
62-
$\tenv.\staticenvsG.\constantvalues(\id) = \vl$;
63-
\item define the local dynamic environment $\vlocal$ as the empty map;
64-
\item define the environment $\env$ to have the static component $\tenv$ and the dynamic
65-
environment $\{\dynamicenvsG: \vglobal, \dynamicenvsL: \vlocal\}$;
66-
\end{itemize}
67-
\FormallyParagraph
68-
\begin{mathpar}
69-
\inferrule{
70-
\vglobal \eqdef [\id \mapsto \NVLiteral(\vl) \;|\; \tenv.\staticenvsG.\constantvalues(\id) = \vl]\\
71-
\vlocal \eqdef \emptyfunc
72-
}{
73-
\staticenvtoenv(\tenv) \typearrow \overname{(\tenv, \{\dynamicenvsG: \vglobal, \dynamicenvsL: \vlocal\})}{\env}
74-
}
75-
\end{mathpar}
76-
% TODO: re-translate once empty_func has been introduced.
77-
% \RenderProseAndFormally{static_env_to_env}
56+
\RenderProseAndFormally{static_env_to_env}

‎asllib/doc/SymbolicSubsumptionTesting.tex‎

Lines changed: 1 addition & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -479,101 +479,7 @@ \section{Symbolic Reasoning\label{sec:Symbolic Reasoning}}
479479
for cases where a binary operation involves two \rangeconstraintsterm.
480480
\ASLListing{Generating constraints for binary operations}{ApplyBinopExtremities}{\typingtests/TypingRule.ApplyBinopExtremities.asl}
481481

482-
\ProseParagraph
483-
\OneApplies
484-
\begin{itemize}
485-
\item \AllApplyCase{exact\_exact}
486-
\begin{itemize}
487-
\item $\vcone$ is a constraint for the expression $\va$;
488-
\item $\vctwo$ is a constraint for the expression $\vc$;
489-
\item define $\newcs$ as the list containing the constraint for the \binopexpressionterm{} $\AbbrevEBinop{\op}{\va}{\vc}$.
490-
\end{itemize}
491-
492-
\item \AllApplyCase{range\_exact}
493-
\begin{itemize}
494-
\item $\vcone$ is a range constraint for the expressions $\va$ and $\vb$;
495-
\item $\vctwo$ is a constraint for the expression $\vc$;
496-
\item applying $\possibleextremitiesleft$ to $\op$, $\va$, and $\vb$ yields $\extpairs$;
497-
\item define $\newcs$ as the list containing a constraint $\AbbrevConstraintRange{\AbbrevEBinop{\op}{\vap}{\vc}}{\AbbrevEBinop{\op}{\vbp}{\vc}}$
498-
for each pair of expressions $(\vap, \vbp)$ in $\extpairs$.
499-
\end{itemize}
500-
501-
\item \AllApplyCase{exact\_range}
502-
\begin{itemize}
503-
\item $\vcone$ is a constraint for the expression $\va$;
504-
\item $\vctwo$ is a range constraint for the expressions $\vc$ and $\vd$;
505-
\item applying $\possibleextremitiesright$ to $\op$, $\vc$, and $\vd$ yields $\extpairs$;
506-
\item define $\newcs$ as the list containing a constraint $\AbbrevConstraintRange{\AbbrevEBinop{\op}{\va}{\vcp}}{\AbbrevEBinop{\op}{\va}{\vdp}}$
507-
for each pair of expressions $(\vcp, \vdp)$ in $\extpairs$.
508-
\end{itemize}
509-
510-
\item \AllApplyCase{range\_range}
511-
\begin{itemize}
512-
\item $\vcone$ is a range constraint for the expressions $\va$ and $\vb$;
513-
\item $\vctwo$ is a range constraint for the expressions $\vc$ and $\vd$;
514-
\item applying $\possibleextremitiesleft$ to $\op$, $\va$, and $\vb$ yields $\extpairsab$;
515-
\item applying $\possibleextremitiesright$ to $\op$, $\vc$, and $\vd$ yields $\extpairscd$;
516-
\item define $\newcs$ as the list containing a constraint $\AbbrevConstraintRange{\AbbrevEBinop{\op}{\vap}{\vcp}}{\AbbrevEBinop{\op}{\vbp}{\vdp}}$
517-
for each pair of expressions
518-
$(\vap, \vbp)$ in $\extpairsab$
519-
and each pair of expressions
520-
$(\vcp, \vdp)$ in $\extpairscd$.
521-
\end{itemize}
522-
\end{itemize}
523-
524-
\FormallyParagraph
525-
\begin{mathpar}
526-
\inferrule[exact\_exact]{
527-
\vcone = \ConstraintExact(\va)\\
528-
\vctwo = \ConstraintExact(\vc)
529-
}{
530-
{
531-
\begin{array}{r}
532-
\applybinopextremities(\op, \vcone, \vctwo) \typearrow \\
533-
\overname{[ \ConstraintExact(\AbbrevEBinop{\op}{\va}{\vc}) ]}{\newcs}
534-
\end{array}
535-
}
536-
}
537-
\end{mathpar}
538-
539-
\begin{mathpar}
540-
\inferrule[range\_exact]{
541-
\vcone = \ConstraintRange(\va, \vb)\\
542-
\vctwo = \ConstraintExact(\vc)\hva\\
543-
\possibleextremitiesleft(\op, \va, \vb) \typearrow \extpairs\\
544-
\newcs \eqdef [(\vap, \vbp) \in \extpairs: \AbbrevConstraintRange{\AbbrevEBinop{\op}{\vap}{\vc}}{\AbbrevEBinop{\op}{\vbp}{\vc}}]
545-
}{
546-
\applybinopextremities(\op, \vcone, \vctwo) \typearrow
547-
\newcs
548-
}
549-
\end{mathpar}
550-
551-
\begin{mathpar}
552-
\inferrule[exact\_range]{
553-
\vcone = \ConstraintExact(\va)\\
554-
\vctwo = \ConstraintRange(\vc, \vd)\hva\\
555-
\possibleextremitiesright(\op, \vc, \vd) \typearrow \extpairs\\
556-
\newcs \eqdef [(\vcp, \vdp) \in \extpairs: \AbbrevConstraintRange{\AbbrevEBinop{\op}{\va}{\vcp}}{\AbbrevEBinop{\op}{\va}{\vdp}}]
557-
}{
558-
\applybinopextremities(\op, \vcone, \vctwo) \typearrow
559-
\newcs
560-
}
561-
\end{mathpar}
562-
563-
\begin{mathpar}
564-
\inferrule[range\_range]{
565-
\vcone = \ConstraintRange(\va, \vb)\\
566-
\vctwo = \ConstraintRange(\vc, \vd)\hva\\
567-
\possibleextremitiesleft(\op, \va, \vb) \typearrow \extpairsab\\
568-
\possibleextremitiesright(\op, \vc, \vd) \typearrow \extpairscd\hva\\
569-
\newcs \eqdef [(\vap, \vbp) \in \extpairsab, (\vcp, \vdp) \in \extpairscd:
570-
\AbbrevConstraintRange{\AbbrevEBinop{\op}{\vap}{\vcp}}{\AbbrevEBinop{\op}{\vbp}{\vdp}}]
571-
}{
572-
\applybinopextremities(\op, \vcone, \vctwo) \typearrow
573-
\newcs
574-
}
575-
\end{mathpar}
576-
%\RenderProseAndFormally{apply_binop_extremities}
482+
\RenderProseAndFormally{apply_binop_extremities}
577483

578484
\TypingRuleDef{PossibleExtremitiesLeft}
579485
\RenderRelation{possible_extremities_left}

‎asllib/doc/asl.spec‎

Lines changed: 60 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10266,8 +10266,18 @@ semantics function static_env_to_env(tenv: static_envs) ->
1026610266
\staticenvironmentterm{} {tenv} into an environment
1026710267
{env}.",
1026810268
prose_transition = "transforming the constants defined in {tenv} into an \environmentterm{} yields",
10269-
};
10270-
10269+
} =
10270+
constant_bindings := bindings(tenv.static_envs_G.constant_values);
10271+
constant_bindings =: list_combine(constant_ids, constant_literals);
10272+
constant_values := list_map(l, constant_literals, NV_Literal(l));
10273+
global_storage_bindings := list_combine(constant_ids, constant_values);
10274+
global_storage := bindings_to_map(global_storage_bindings);
10275+
empty_global := empty_denv.dynamic_envs_G;
10276+
new_global := empty_global(storage: global_storage);
10277+
new_denv := empty_denv(dynamic_envs_G: new_global);
10278+
--
10279+
(tenv, new_denv);
10280+
;
1027110281

1027210282
//////////////////////////////////////////////////
1027310283
// Relations for Subprogram Calls
@@ -13930,7 +13940,54 @@ typing function apply_binop_extremities(op: binop, c1: int_constraint, c2: int_c
1393013940
{op} yields a \dynamicerrorterm{}.",
1393113941
prose_application = "the range constraints for {c1} and {c2}",
1393213942
prose_transition = "computing the range constraints for {c1} and {c2} yields",
13933-
};
13943+
} =
13944+
case exact_exact {
13945+
c1 =: Constraint_Exact(a);
13946+
c2 =: Constraint_Exact(c);
13947+
--
13948+
make_singleton_list(Constraint_Exact(AbbrevEBinop(op, a, c)));
13949+
}
13950+
13951+
case range_exact {
13952+
c1 =: Constraint_Range(a, b);
13953+
c2 =: Constraint_Exact(c);
13954+
possible_extremities_left(op, a, b) -> extpairs;
13955+
extpairs =: list_combine(ext_a, ext_b);
13956+
ext_a_c := list_map(i, indices(extpairs), AbbrevEBinop(op, ext_a[i], c));
13957+
ext_b_c := list_map(i, indices(extpairs), AbbrevEBinop(op, ext_b[i], c));
13958+
new_cs := list_map(i, indices(extpairs), AbbrevConstraintRange(ext_a_c[i], ext_b_c[i]));
13959+
--
13960+
new_cs;
13961+
}
13962+
13963+
case exact_range {
13964+
c1 =: Constraint_Exact(a);
13965+
c2 =: Constraint_Range(c, d);
13966+
possible_extremities_right(op, c, d) -> extpairs;
13967+
extpairs =: list_combine(ext_c, ext_d);
13968+
ext_a_c := list_map(i, indices(extpairs), AbbrevEBinop(op, a, ext_c[i]));
13969+
ext_a_d := list_map(i, indices(extpairs), AbbrevEBinop(op, a, ext_d[i]));
13970+
new_cs := list_map(i, indices(extpairs), AbbrevConstraintRange(ext_a_c[i], ext_a_d[i]));
13971+
--
13972+
new_cs;
13973+
}
13974+
13975+
case range_range {
13976+
c1 =: Constraint_Range(a, b);
13977+
c2 =: Constraint_Range(c, d);
13978+
possible_extremities_left(op, a, b) -> extpairs_a_b;
13979+
possible_extremities_right(op, c, d) -> extpairs_c_d;
13980+
ext_cross := list_cross(extpairs_a_b, extpairs_c_d);
13981+
ext_cross =: list_combine(cross_a_b, cross_c_d);
13982+
cross_a_b =: list_combine(ext_a, ext_b);
13983+
cross_c_d =: list_combine(ext_c, ext_d);
13984+
new_a_c := list_map(i, indices(ext_cross), AbbrevEBinop(op, ext_a[i], ext_c[i]));
13985+
new_b_d := list_map(i, indices(ext_cross), AbbrevEBinop(op, ext_b[i], ext_d[i]));
13986+
new_cs := list_map(i, indices(ext_cross), AbbrevConstraintRange(new_a_c[i], new_b_d[i]));
13987+
--
13988+
new_cs;
13989+
}
13990+
;
1393413991

1393513992
typing function possible_extremities_left(op: binop, a: expr, b: expr) ->
1393613993
(extpairs: list0((expr, expr)))

‎asllib/doc/variable_name_macros.tex‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,6 @@
120120
\newcommand\typedspec[0]{\texttt{typed\_spec}}
121121
\newcommand\va[0]{\texttt{a}}
122122
\newcommand\vapprox[0]{\texttt{approx}}
123-
\newcommand\vap[0]{\texttt{a'}}
124123
\newcommand\vaccess[0]{\texttt{access}}
125124
\newcommand\vaccessors[0]{\texttt{accessors}}
126125
\newcommand\vaccessorpair[0]{\texttt{accessor\_pair}}
@@ -143,7 +142,6 @@
143142
\newcommand\vb[0]{\texttt{b}}
144143
\newcommand\vbuiltin[0]{\texttt{builtin}}
145144
\newcommand\vbits[0]{\texttt{bits}}
146-
\newcommand\vbp[0]{\texttt{b'}}
147145
\newcommand\vbase[0]{\texttt{base}}
148146
\newcommand\vbasiclexpr[0]{\texttt{basic\_lexpr}}
149147
\newcommand\vbinop[0]{\texttt{binop}}
@@ -169,7 +167,6 @@
169167
\newcommand\vcs[0]{\texttt{vcs}}
170168
\newcommand\vctwo[0]{\texttt{c2}}
171169
\newcommand\vd[0]{\texttt{d}}
172-
\newcommand\vdp[0]{\texttt{d'}}
173170
\newcommand\vdebug[0]{\texttt{debug}}
174171
\newcommand\vdecl[0]{\texttt{decl}}
175172
\newcommand\vdeclp[0]{\texttt{decl'}}
@@ -225,9 +222,7 @@
225222
\newcommand\vlhsaccess[0]{\texttt{lhs\_access}}
226223
\newcommand\vlhsaccessopt[0]{\texttt{lhs\_access\_opt}}
227224
\newcommand\vlhsaccessopts[0]{\texttt{lhs\_access\_opts}}
228-
\newcommand\vlocal[0]{\texttt{local}}
229225
\newcommand\vlooplimit[0]{\texttt{looplimit}}
230-
\newcommand\vglobal[0]{\texttt{global}}
231226
\newcommand\vgone[0]{\texttt{g1}}
232227
\newcommand\vgp[0]{\texttt{g'}}
233228
\newcommand\vgthree[0]{\texttt{g3}}
@@ -267,9 +262,6 @@
267262
\newcommand\vltwo[0]{\texttt{l2}}
268263
\newcommand\vlthree[0]{\texttt{l3}}
269264
\newcommand\vm[0]{\texttt{m}}
270-
\newcommand\extpairs[0]{\texttt{extpairs}}
271-
\newcommand\extpairsab[0]{\texttt{extpairs\_a\_b}}
272-
\newcommand\extpairscd[0]{\texttt{extpairs\_c\_d}}
273265
\newcommand\vmlist[0]{\texttt{vm\_list}}
274266
\newcommand\vmone[0]{\texttt{m1}}
275267
\newcommand\vmtwo[0]{\texttt{m2}}

0 commit comments

Comments
 (0)