Merge pull request #1266 from GaloisInc/T1024-crucible-syntax-exotic-…

…fresh-var-names

`crucible-syntax`: Allow exotic characters in fresh atom names

crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs

@@ -1564,21 +1564,24 @@ atomSetter (AtomName anText) =
 
     fresh =
       do t <- reading (unary Fresh isType)
-         describe "user symbol" $
-           case userSymbol (T.unpack anText) of
-             Left err -> describe (T.pack (show err)) empty
-             Right nm ->
-               do loc <- position
-                  case t of
-                    Some (FloatRepr fi) ->
-                      Some <$>
-                        freshAtom loc (FreshFloat fi (Just nm))
-                    Some NatRepr ->
-                      Some <$> freshAtom loc (FreshNat (Just nm))
-                    Some tp
-                      | AsBaseType bt <- asBaseType tp ->
-                          Some <$> freshAtom loc (FreshConstant bt (Just nm))
-                      | otherwise -> describe "atomic type" $ empty
+         -- Note that we are using safeSymbol below to create a What4 symbol
+         -- name, which will Z-encode names that aren't legal solver names. This
+         -- includes names that include hyphens, which are very common in
+         -- S-expression syntax. This is fine to do, since the Z-encoded name
+         -- name is only used for solver purposes; the original, unencoded name
+         -- is recorded separately.
+         let nm = safeSymbol (T.unpack anText)
+         loc <- position
+         case t of
+           Some (FloatRepr fi) ->
+             Some <$>
+               freshAtom loc (FreshFloat fi (Just nm))
+           Some NatRepr ->
+             Some <$> freshAtom loc (FreshNat (Just nm))
+           Some tp
+             | AsBaseType bt <- asBaseType tp ->
+                 Some <$> freshAtom loc (FreshConstant bt (Just nm))
+             | otherwise -> describe "atomic type" $ empty
 
     evaluated =
        do Pair _ e' <- reading synth

crucible-syntax/test-data/exotic-fresh-names.cbl

@@ -0,0 +1,10 @@
+; A regression test for #1024.
+
+(defun @exotic-fresh-names () Bool
+  (start start:
+    ; Although the list of allowable characters in What4 solver names is very
+    ; small, we can nevertheless define atom names with unallowable characters
+    ; by Z-encoding them under the hood.
+    (let ω (fresh Bool))                ; Fancy Unicode characters
+    (let hyphens-are-fine (fresh Bool)) ; Hyphens
+    (return (and ω hyphens-are-fine))))

crucible-syntax/test-data/exotic-fresh-names.out.good

@@ -0,0 +1,17 @@
+(defun @exotic-fresh-names () Bool
+   (start start:
+      (let ω (fresh Bool))
+      (let hyphens-are-fine (fresh Bool))
+      (return (and ω hyphens-are-fine))))
+
+exotic-fresh-names
+%0
+  % 8:12
+  $0 = fresh BaseBoolRepr zenc!z3c9U
+  % 9:27
+  $1 = fresh BaseBoolRepr zenc!hyphenszmarezmfine
+  % 10:13
+  $2 = and($0, $1)
+  % 10:5
+  return $2
+  % no postdom