Sim refactor #1298

robdockins · 2021-05-18T00:22:45Z

This PR implements a variety of refactorings, mostly to the saw-core simulator. These refactorings are aimed toward implementing a new evaluation mode for saw-core which does evaluation and simplification directly on saw-core terms, without passing first through what4, or some other term representation. The goal of this is to make the term evaluator a total function
on well-typed terms, so that terms are reconstructed as necessary when an external variable or opaque constant is encountered.

In order to enable the term evaluator, a number of improvements to the generic evaluator code are necessary. First, the environment that binds de Bruijn variables to values must also keep track of the types of variables, because the term reconstruction procedure is type-directed. Achieving this required a relatively extensive detour into reworking some aspects related to the implementation of datatype recursors. The end result is that it is now possible to lambda-abstract over recursor values and later apply them to data type arguments (although no concrete syntax exists for this). Secondly, the evaluator needs a way to gracefully handle the situation where evaluation gets "stuck" on a term that isn't in canonical form for an eliminator. These "neutral" terms represent places where evaluation would proceed into external variables, opaque constants, or other forms that don't immediately evaluate. The simulator would mostly panic before in these situations.

Along the way, a number of other, smaller, improvements have been made. There are some situations involving the new VIntToNat constructor that still need to be handled, but they were already non-working cases before.

This PR consists entirely of internal changes that I expect to have minimal user-facing impact.

brianhuffman · 2021-06-04T19:58:55Z

saw-core/src/Verifier/SAW/Simulator/Prims.hs

-    VToNat (VVector v) -> fromIntegral (V.length v)
-    VToNat (VWord w) -> fromIntegral (bpBvSize bp w)
+    VBVToNat n _ -> fromIntegral n -- TODO, remove this fromIntegral 
+    VIntToNat _ -> error "natSize: symbolic integer"


Is there a better alternative to calling error here?

brianhuffman · 2021-06-04T20:04:25Z

saw-core/src/Verifier/SAW/Simulator/Prims.hs

@@ -455,9 +457,9 @@ natToWord :: (VMonad l, Show (Extra l)) => BasePrims l -> Int -> Value l -> MWor
 natToWord bp w val =
  case val of
    VNat n -> bpBvLit bp w (toInteger n)
-    VToNat v ->
+    VIntToNat _i -> error "natToWord of VIntToNat TODO!"


What needs to be done here?

brianhuffman · 2021-06-04T20:05:58Z

saw-core/src/Verifier/SAW/Simulator/Prims.hs

          _ -> panic "atOp: expected vector"
+
+      VIntToNat _i ->
+        error "atWithDefault: symbolic integer TODO"


We'll probably need to implement a proper indexing operation with symbolic integer index.

brianhuffman · 2021-06-04T20:07:48Z

saw-core/src/Verifier/SAW/Simulator/Prims.hs

        do let update i = return (VVector (xv V.// [(i, y)]))
           iv' <- V.mapM (liftM toBool . force) iv
           selectV (lazyMuxValue bp) (fromIntegral n - 1) update iv' -- FIXME dangerous fromIntegral
+
+      VIntToNat _ -> error "updOp: symbolic integer TODO"


A symbolic-integer-index update should be implementable by putting an equality-test if-then-else in each array position

brianhuffman · 2021-06-04T20:09:21Z

saw-core/src/Verifier/SAW/Simulator/Prims.hs

@@ -808,6 +816,8 @@ expByNatOp bp =

         loop one . V.toList =<< toBits (bpUnpack bp) w

+    VIntToNat _ -> error "expByNat: symbolic integer"


I guess exponentiation by a symbolic integer will never be supported, as it's not in the SMT-Lib theory. We should throw a catchable user-error exception.

brianhuffman · 2021-06-04T20:11:05Z

saw-core/src/Verifier/SAW/Simulator/Prims.hs

          VWord xw -> do
            zb <- toBool <$> force z
            VWord <$> wordOp zb xw iw
          _ -> panic $ "shiftOp: " ++ show xs
+
+      VIntToNat _i -> error "shiftOp: symbolic integer TODO"


This should be implementable; we will need to produce a big chain of nested if-then-else expressions with index equality tests.

brianhuffman · 2021-06-04T20:13:59Z

saw-core/src/Verifier/SAW/Simulator/Value.hs

  | VVector !(Vector (Thunk l))
  | VBool (VBool l)
  | VWord (VWord l)
-  | VToNat (Value l)
+  | VBVToNat !Int (Value l) -- TODO: don't use @Int@ for this, use @Natural@


Is there anything tricky about changing this to Natural?

Mainly that vectors and the concrete bitvector representations use Int for their lengths.

brianhuffman · 2021-06-04T20:18:23Z

Commit d17926a "Improve scAbstractExts and scGeneralizeExts" seems like it's fixing a separate bug; maybe it would make more sense as a separate PR

saw-core/src/Verifier/SAW/Simulator/Prims.hs

saw-core/src/Verifier/SAW/Module.hs

saw-core/src/Verifier/SAW/Recognizer.hs

saw-core/src/Verifier/SAW/Term/CtxTerm.hs

saw-core/src/Verifier/SAW/Term/Functor.hs

brianhuffman

Make sure to open tickets for the unimplemented Integer operations.

This distinguishes the two different coercions that can occur, and allows us to track the width of the bitvector type in `VBVToNat`.

where they can be reused more easily.

The main techincal change here is to allow "recursors" to be value forms in their own right at the AST level, conceptually separate from recursor applications. This simplifies a variety of things relating to the implementation of recursors; in particular, the terms representing iota reductions require fewer free variables and have simpler types. The "recursor" value is specified by giving: the data type, the parameters to that data type, the elimination motive, and the constructor eliminator functions. The data defining a recursor are constant throughout the execution of recursive elimination. A "recursor application" takes a recursor value, values for the indices of the data type being eliminated, and the argument to be eliminated. Although this change allows recursor values to be abstracted by lambdas and for recursor applications to be built separately from a concrete recursor value, there is currently no surface syntax for building such a "partially applied" recursor, nor for the new type of recursor values. As before, only fully-applied recursors are allowed by the parser/typechecker front-end.

Split the collection of arguments to data constructors to keep parameters separate from regular arguments.

`PrimName` values instead of just `Ident` and register their names in the naming environment so they participate in pretty printing name resolution.

This really only properly handles pretty narrow situations regarding constructors. Muxing data type values will only succeed if the same constructor is used in both values, and if the constructor forms a non-dependent function on its regular (non-parameter) arguments. However, this is similar to the prior situation, where the constructors were required to be the same, and muxing arguments would panic if they differed in shape.

on opaque values.

Minor other fixes.

It is a context-dependent keyword and causes problems with some syntax highlighting systems.

robdockins requested review from brianhuffman and eddywestbrook May 18, 2021 00:22

robdockins mentioned this pull request May 18, 2021

Avoid concatenating Text values in termToPat. #1272

Merged

robdockins force-pushed the sim-refactor branch from 93c6d0b to d005f62 Compare June 3, 2021 18:59

robdockins added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Jun 3, 2021

brianhuffman reviewed Jun 4, 2021

View reviewed changes

saw-core/src/Verifier/SAW/Simulator/Prims.hs Outdated Show resolved Hide resolved

brianhuffman reviewed Jun 4, 2021

View reviewed changes

saw-core/src/Verifier/SAW/Module.hs Outdated Show resolved Hide resolved

brianhuffman reviewed Jun 4, 2021

View reviewed changes

saw-core/src/Verifier/SAW/Recognizer.hs Outdated Show resolved Hide resolved

brianhuffman reviewed Jun 4, 2021

View reviewed changes

saw-core/src/Verifier/SAW/Term/CtxTerm.hs Outdated Show resolved Hide resolved

brianhuffman reviewed Jun 4, 2021

View reviewed changes

saw-core/src/Verifier/SAW/Term/Functor.hs Outdated Show resolved Hide resolved

robdockins removed the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Jun 7, 2021

This was referenced Jun 11, 2021

Improve scAbstractExts and scGeneralizeExts #1335

Merged

Typed term #1336

Merged

robdockins force-pushed the sim-refactor branch from d005f62 to 9aa7a62 Compare June 14, 2021 20:58

brianhuffman approved these changes Jun 14, 2021

View reviewed changes

robdockins added 7 commits June 15, 2021 11:59

Split VToNat into VBVToNat and VIntToNat

0e48393

This distinguishes the two different coercions that can occur, and allows us to track the width of the bitvector type in `VBVToNat`.

Move some operations from the concrete simulator into Prim

ffc1d20

where they can be reused more easily.

Pipe type info through mux operations.

2656efc

Add type information to the simulator evaluation environment

e360dcc

Split the collection of arguments to data constructors to keep parameters separate from regular arguments.

Refactor the names of data type and constructors to carry

33a4c37

`PrimName` values instead of just `Ident` and register their names in the naming environment so they participate in pretty printing name resolution.

Implement recursors on concrete Nat values

432bfa4

robdockins added 6 commits June 15, 2021 11:59

Better error reporting for recursors and recursor applications

7f988d0

Add a notion of NeutralTerm for when evaluation gets stuck

1707182

on opaque values.

Update comments relating to the way iota reductions work.

2ac830c

Minor other fixes.

Fix typos and remove commented-out lines

cc0d892

Avoid using the identifier rec as a bound variable.

e8dcf93

It is a context-dependent keyword and causes problems with some syntax highlighting systems.

robdockins force-pushed the sim-refactor branch from 9aa7a62 to e8dcf93 Compare June 15, 2021 19:00

robdockins merged commit c8edab3 into master Jun 15, 2021

mergify bot deleted the sim-refactor branch June 15, 2021 20:53

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Sim refactor #1298

Sim refactor #1298

robdockins commented May 18, 2021

brianhuffman Jun 4, 2021

brianhuffman Jun 4, 2021

brianhuffman Jun 4, 2021

brianhuffman Jun 4, 2021

brianhuffman Jun 4, 2021

brianhuffman Jun 4, 2021

brianhuffman Jun 4, 2021

robdockins Jun 4, 2021

brianhuffman commented Jun 4, 2021

brianhuffman left a comment

		@@ -808,6 +816,8 @@ expByNatOp bp =

		loop one . V.toList =<< toBits (bpUnpack bp) w

		VIntToNat _ -> error "expByNat: symbolic integer"

Sim refactor #1298

Sim refactor #1298

Conversation

robdockins commented May 18, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

brianhuffman commented Jun 4, 2021

brianhuffman left a comment

Choose a reason for hiding this comment