From e696b7a8a83672d263d01714239289d782c8ea3d Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 16 Oct 2019 13:36:00 -0700 Subject: [PATCH] Various small documentation and error changes (#566) * Remove references to LSS in intTests Fixes #493. * Remove obsolete note about globals and unsoundness Fixes #563 * Point users at `enable_{deprecated,experimental}` Fixes #496. --- doc/manual/manual.pdf | Bin 375980 -> 375982 bytes intTests/test0012_jss_aig/README | 8 ++++---- intTests/test0015_sawscript_aig/README | 11 +++++------ intTests/test0015_sawscript_aig/test.saw | 3 +-- src/SAWScript/Interpreter.hs | 4 +--- src/SAWScript/MGU.hs | 6 +++++- 6 files changed, 16 insertions(+), 16 deletions(-) diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index dcfec8152e8ec93ff64ad4b3d5e2d85996d62b7f..efb7bde929c421e9d0fc13160b64873cf5327294 100644 GIT binary patch delta 210 zcmZ4UQ*7N&v4$4L7N!>F7M3lnTUJO06y>LsCZ`rDXcVNRg``I48tR!C=ouMkPT#bG zwRL*HN>&9OLjyxILjzM2V>4X?b9Dm)bxkgP-~1Gp#FA764HqjT14B!=lI?R=vOeK( zHZ?LcH#f9&G&Hm{0qS;gGIBODG;lUEcQi9LcXDyIQ?MbVWc%SwteKolRSTx;?P2v} a-}&4AIP)XL>CJms6*(-pR8?L5-M9ePDLhR8 delta 188 zcmZ4YQ*6yov4$4L7N!>F7M3lnTUJazzk;<{JfJ8)r8GIUNTVPnEhIHU*HF*IK+niv zdcaCnB~AlVBMU<_BNM~v)hk)05ZvwaRG<9`$b8<5@FgA5^Gqx~yG%c_tExBXGeN3zpf_pmB*m~pA9y863u F0RZ~dILrV5 diff --git a/intTests/test0012_jss_aig/README b/intTests/test0012_jss_aig/README index c2303dd0b6..54a7882964 100644 --- a/intTests/test0012_jss_aig/README +++ b/intTests/test0012_jss_aig/README @@ -4,10 +4,10 @@ The tests in 'test.saw' only make sense for the SAW backend; the default backend encodes the arguments and results in a different way. -There used to be a bug in JSS and LSS where multiple AIG writes -interacted, causing the number of input bits in the AIG to grow with -each write. So in 'test.sh' we are careful to check that the number of -input bits is always 16. +There used to be a bug in JSS where multiple AIG writes interacted, +causing the number of input bits in the AIG to grow with each write. So +in 'test.sh' we are careful to check that the number of input bits is +always 16. Besides checking predicates, where the input encoding does not matter, and the output is a single bit, we also check the input and output diff --git a/intTests/test0015_sawscript_aig/README b/intTests/test0015_sawscript_aig/README index e0c9b66d06..cc3c817597 100644 --- a/intTests/test0015_sawscript_aig/README +++ b/intTests/test0015_sawscript_aig/README @@ -3,9 +3,8 @@ Test AIG generation in SAWScript. These examples provide some documentation of the SAWScript AIG encoding. -Note that, compared to LSS and JSS, the arguments here are reversed: -for functions '\x -> \y -> e' the arguments are packed as 'x # y' -here, but as 'y # x' for LSS and JSS. However, in LSS and JSS you -don't actually write the arguments explicitly -- rather, open terms -are closed over the symbolic variables in scope -- so I'm not sure the -comparison is fair. +Note that, compared to JSS, the arguments here are reversed: for +functions '\x -> \y -> e' the arguments are packed as 'x # y' here, but +as 'y # x' for JSS. However, in JSS you don't actually write the +arguments explicitly -- rather, open terms are closed over the symbolic +variables in scope -- so I'm not sure the comparison is fair. diff --git a/intTests/test0015_sawscript_aig/test.saw b/intTests/test0015_sawscript_aig/test.saw index f37a1694a1..74b83f4402 100644 --- a/intTests/test0015_sawscript_aig/test.saw +++ b/intTests/test0015_sawscript_aig/test.saw @@ -9,13 +9,12 @@ write_aig "tmp/yy.aig" {{ \(x:[8]) -> \(y:[8]) -> y + y }}; write_aig "tmp/2y.aig" {{ \(x:[8]) -> \(y:[8]) -> 2 * y }}; // The code below is very similar to '../test0012_jss_aig/test.saw' -// and '../test0014_lss_aig/test.saw'. // Many of these Cryptol functions have types more specific than // necessary. The point is to document the behavior of SAWScript // AIG generation. let {{ - // Arguments are reversed, compared to LSS and JSS. + // Arguments are reversed, compared to JSS. run_pred : ([16] -> [1]) -> [8] -> [8] -> [1] run_pred f x y = f (((zero # x) <<< 8) + (zero # y)) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index ad7b811e87..9668c962ec 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -2001,9 +2001,7 @@ primitives = Map.fromList Current [ "Return a SetupValue representing the value of the initializer of a named" , "global. The String should be the name of a global value." - , "Note that initializing global variables may be unsound in the presence" - , "of compositional verification (see GaloisInc/saw-script#203)." - ] -- TODO: There should be a section in the manual about global-unsoundness. + ] , prim "crucible_term" "Term -> SetupValue" diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs index f550eb02c2..3305e7161b 100644 --- a/src/SAWScript/MGU.hs +++ b/src/SAWScript/MGU.hs @@ -473,7 +473,11 @@ inferE (ln, expr) = case expr of do env <- TI $ asks typeEnv case M.lookup x env of Nothing -> do - recordError $ "unbound variable: " ++ show x + recordError $ unlines + [ "Unbound variable: " ++ show x + , "Note that some built-in commands are available only after running" + , "either `enable_deprecated` or `enable_experimental`." + ] t <- newType return (Var x, t) Just (Forall as t) -> do