[asl reference] added explanations and examples for symbolic evaluability and constrainedness

Author: Roman-Manevich

asllib/doc/SideEffects.tex

@@ -158,10 +158,19 @@ \section{Side Effect Sets\label{sec:SideEffectSets}}
 See \ExampleRef{Checking Whether Expressions are Symbolically Evaluable}.
 
 \ExampleDef{Why Symbolically Evaluability Matters}
+
+The specification in \listingref{SESIsSymbolicallyEvaluable-bad} is ill-typed.
+Specifically, it shows that when an expression is not \symbolicallyevaluableterm{},
+it cannot be used to express the type of a bitvector. This is because the value
+of the expression might change at runtime.
+
+\ASLListing{Why symbolic evaluability matters}{SESIsSymbolicallyEvaluable-bad}{\typingtests/TypingRule.SESIsSymbolicallyEvaluable.bad.asl}
+
+\ExampleDef{Symbolically Evaluability for Equivalence Testing}
 The specification in \listingref{SESIsSymbolicallyEvaluable} is well-typed.
 Specifically, it shows how the fact that an expression is \symbolicallyevaluableterm{}
 is used to reason about the equivalence of bitwidth expressions.
-\ASLListing{Why symbolic evaluability matters}{SESIsSymbolicallyEvaluable}{\typingtests/TypingRule.SESIsSymbolicallyEvaluable.asl}
+\ASLListing{Symbolically evaluable expressions}{SESIsSymbolicallyEvaluable}{\typingtests/TypingRule.SESIsSymbolicallyEvaluable.asl}
 
 \RenderProseAndFormally{is_symbolically_evaluable}
 

asllib/doc/Types.tex

@@ -539,6 +539,14 @@ \section{Bitvector Types\label{sec:BitvectorTypes}}
 The width of a \bitvectortypeterm{} can be either \staticallyevaluableterm{}
 or \emph{constrained}. That is, a \symbolicallyevaluableterm{} \constrainedintegerterm{}.
 
+Intuitively, the width of bitvectors need to be \symbolicallyevaluableterm{} in order
+to ensure that the types of bitvectors can be statically expressed.
+See \ExampleRef{Why Symbolically Evaluability Matters}.
+
+Intuitively, the widths of bitvectors are constrained to help provide an upper bound
+on their representations when translating ASL to other languages.
+See \ExampleRef{Why Constrained Bitvector Widths Matter}.
+
 \ExampleDef{Symbolic and Constrained Bitwidth}
 \listingref{symbolicbitwidth} shows an example of a bitvector whose width
 is symbolic --- \verb|2 * N| and a bitvector whose width is determined
@@ -602,8 +610,11 @@ \subsection{Typing Bitvector Types}
 In \listingref{typing-tbits}, all the uses of bitvector types are well-typed.
 \ASLListing{Well-typed Bitvector types}{typing-tbits}{\typingtests/TypingRule.TBits.asl}
 
+\ExampleDef{Why Constrained Bitvector Widths Matter}
 The specification in \listingref{typing-tbits-bad} is ill-typed, since widths need
 to be \constrainedintegersterm.
+If the requirement for constrained widths were not in place, this subprogram could generate
+bitvectors of unbounded width.
 \ASLListing{An ill-typed Bitvector type}{typing-tbits-bad}{\typingtests/TypingRule.TBits.bad.asl}
 
 \ExampleRef{A bitvector type with bitfields} shows a well-typed \bitvectortypeterm{} with bitfields.

asllib/doc/dictionary.txt

@@ -84,6 +84,7 @@ always
 ambiguous
 among
 amongst
+amount
 an
 analysis
 analyze
@@ -191,6 +192,8 @@ away
 axiom
 axiomatically
 back
+backend
+backends
 background
 backslash
 badly
@@ -305,6 +308,7 @@ causes
 cell
 certain
 chance
+change
 changed
 changes
 changing
@@ -1301,6 +1305,7 @@ matches
 matching
 material
 mathematical
+matter
 matters
 maximal
 maximum
@@ -2198,6 +2203,7 @@ transitively
 translate
 translated
 translates
+translating
 translation
 transliteration
 traversing

asllib/tests/ASLTypingReference.t/TypingRule.SESIsSymbolicallyEvaluable.bad.asl

@@ -0,0 +1,16 @@
+func returns_bitvector_symbolically_evaluable() => bits(10)
+begin
+    let x : integer{0..10} = 10;
+    var bv: bits(x) = ARBITRARY: bits(x);
+    // The type of bv is type bits(x) because x is immutable.
+    return bv;
+end;
+
+func returns_bitvector_not_symbolically_evaluable() => bits(10)
+begin
+    var x : integer{0..10} = 9;
+    var bv: bits(x) = ARBITRARY: bits(x);
+    x = 10;
+    // What is the type of bv here? It's certainly not bits(x).
+    return bv;
+end;

asllib/tests/ASLTypingReference.t/TypingRule.TBits.bad.asl

@@ -1,4 +1,8 @@
-func foo(I: integer)
+func bitvector_sizes()
 begin
-    var R: bits(I); // illegal: I is unconstrained.
+    var size = ARBITRARY : integer;
+    let immutable_size = size;
+    // immutable_size is symbolically evaluable.
+    // Illegal: immutable_size is not constrained.
+    var bv: bits(immutable_size);
 end;

asllib/tests/ASLTypingReference.t/run.t

@@ -160,9 +160,9 @@ ASL Typing Tests / annotating types:
 
   $ aslref TypingRule.TBits.asl
   $ aslref TypingRule.TBits.bad.asl
-  File TypingRule.TBits.bad.asl, line 3, characters 16 to 17:
-      var R: bits(I); // illegal: I is unconstrained.
-                  ^
+  File TypingRule.TBits.bad.asl, line 7, characters 17 to 31:
+      var bv: bits(immutable_size);
+                   ^^^^^^^^^^^^^^
   ASL Type error: constrained integer expected, provided integer.
   [1]
   $ aslref TypingRule.TTuple.asl
@@ -1035,6 +1035,13 @@ ASL Typing Tests / annotating types:
   [1]
   $ aslref --no-exec TypingRule.SESForSubprogram.asl
   $ aslref --no-exec TypingRule.SESIsSymbolicallyEvaluable.asl
+  $ aslref --no-exec TypingRule.SESIsSymbolicallyEvaluable.bad.asl
+  File TypingRule.SESIsSymbolicallyEvaluable.bad.asl, line 12,
+    characters 38 to 39:
+      var bv: bits(x) = ARBITRARY: bits(x);
+                                        ^
+  ASL Type error: expected a symbolically evaluable expression/subprogram.
+  [1]
   $ aslref TypingRule.SliceEqual.asl
   $ aslref TypingRule.SlicesEqual.asl
   $ aslref TypingRule.BitwidthEqual.asl