wip

GaloisInc · Sep 8, 2021 · 8a19270 · 8a19270
1 parent 8bf2f4e
commit 8a19270
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 28 deletions.
diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile
@@ -7,7 +7,7 @@ WORKDIR /saw-script
 RUN mkdir -p /saw-script && \
     git clone https://github.com/GaloisInc/aws-lc-verification.git && \
     cd aws-lc-verification && \
-    git checkout 44c849279a45b17ded570af7e89928b1e2a0f456 && \
+    git checkout 0e55a079cf53187bf4bf8e4548f7fd885a004899 && \
     git config --file=.gitmodules submodule.src.url https://github.com/awslabs/aws-lc && \
     git submodule sync && \
     git submodule update --init

diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1478,26 +1478,7 @@ learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) =
 
                    return Nothing
 
-              -- _ ->
-              --   do expected_sz_bv <- liftIO $ resolveSAWSymBV cc (knownNat @64) (ttTerm expected_sz_tm)
-              --      case BV.asUnsigned <$> W4.asBV expected_sz_bv of
-              --        Just expected_sz ->
-              --          do res <- liftIO $ Crucible.loadRaw sym mem ptr1 (Crucible.arrayType (fromIntegral expected_sz) (Crucible.bitvectorType 1)) Crucible.noAlignment
-              --             case res of
-              --               Crucible.NoErr pred_ res_val -> do
-              --                 addAssert pred_ $ Crucible.SimError loc $ Crucible.AssertFailureSimError (show errMsg) ""
-              --                 -- realTerm <- valueToSC sym loc (show errMsg) tval res_val
-              --                 -- instantiateExtMatchTerm sc cc (cs ^. MS.csLoc) prepost realTerm (ttTerm expectedTT)
-              --                 -- arr_tm <- memArrayToSawCoreTerm cc
-
-              --                 -- instantiateExtMatchTerm sc cc loc prepost arr_tm (ttTerm expected_arr_tm)
-
-              --      return Nothing
-
-              --        Nothing -> return $ Just errMsg
-              _ -> do
-                liftIO $ putStrLn $ show $ Crucible.ppMem $ Crucible.memImplHeap mem
-                return $ Just errMsg
+              _ -> return $ Just errMsg
 
 ------------------------------------------------------------------------
 

diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -512,12 +512,8 @@ llvm_verify_x86' (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat m
              arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) ->
                toSC sym sawst $ Crucible.LLVM.Fixpoint.headerValue fixpoint_entry
              applied_func <- scApplyAll sc (ttTerm func) $ baz ++ arguments
-             putStrLn $ scPrettyTerm Verifier.SAW.SharedTerm.defaultPPOpts applied_func
-             tp <- scTypeOf sc applied_func
-             putStrLn $ scPrettyTerm Verifier.SAW.SharedTerm.defaultPPOpts tp
-             applied_func_selectors <- forM [1 .. (length fixpoint_substitution_as_list)] $ \i -> do
-               la <- scTupleSelector sc applied_func i (length fixpoint_substitution_as_list)
-               putStrLn $ scPrettyTerm Verifier.SAW.SharedTerm.defaultPPOpts la
+            --  putStrLn $ scPrettyTerm Verifier.SAW.SharedTerm.defaultPPOpts applied_func
+             applied_func_selectors <- forM [1 .. (length fixpoint_substitution_as_list)] $ \i ->
                scTupleSelector sc applied_func i (length fixpoint_substitution_as_list)
              result_substitution <- MapF.fromList <$> zipWithM
                (\(MapF.Pair variable _) applied_func_selector ->
@@ -540,7 +536,7 @@ llvm_verify_x86' (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat m
              w <- scNat sc 64
              rhs <- scBvMul sc w (head baz) =<< scBvNat sc w =<< scNat sc 128
              foo_condition <- scBvULt sc w lhs rhs
-             putStrLn $ "foo_condition: " ++ scPrettyTerm Verifier.SAW.SharedTerm.defaultPPOpts foo_condition
+            --  putStrLn $ "foo_condition: " ++ scPrettyTerm Verifier.SAW.SharedTerm.defaultPPOpts foo_condition
              foo_type <- scTupleType sc =<< mapM (scTypeOf sc) lala_arguments
              foo_lala <- scIte sc foo_type foo_condition foo_applied_func foo_la
              foo_lalala <- scEq sc foo_lala body