Skip to content

Commit

Permalink
Draft: Basic checking for underspecified mutable allocs in overrides
Browse files Browse the repository at this point in the history
  • Loading branch information
RyanGlScott committed Nov 7, 2023
1 parent 2d306dd commit 2e79a1e
Show file tree
Hide file tree
Showing 8 changed files with 476 additions and 14 deletions.
19 changes: 10 additions & 9 deletions intTests/test_mir_unsafe_assume_spec/test.saw
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,8 @@ let side_spec_2 = do {
mir_return (mir_term a);
};

// This spec is erroneous—see the comments below in the "Avoid unsoundness"
// part of the test.
let foo_spec = do {
x <- mir_fresh_var "x" mir_u32;

Expand Down Expand Up @@ -141,18 +143,17 @@ fails (
// Avoid unsoundness //
///////////////////////

// https://github.com/GaloisInc/saw-script/issues/30

side_ov_1 <- mir_verify m "test::side_effect" [] false side_spec_1 z3;
side_ov_2 <- mir_verify m "test::side_effect" [] false side_spec_2 z3;

// This should not verify, as invoking `side_effect` should cause `foo` to
// always return `0` rather than the argument value.
fails (
mir_verify m "test::foo" [side_ov_1] false foo_spec z3
);
// TODO: This should not verify, as side_spec_2 underspecifies the mutable
// allocation `a_ptr`. We need to implement a check that catches this.
// fails (
// mir_verify m "test::foo" [side_ov_2] false foo_spec z3
// );

// TODO: Add similar tests for mutable statics.
// This should not verify, as side_spec_2 underspecifies the mutable
// allocation `a_ptr` in its postconditions. SAW will catch this when attempting
// to use side_ov_2 as an override.
fails (
mir_verify m "test::foo" [side_ov_2] false foo_spec z3
);
13 changes: 13 additions & 0 deletions intTests/test_mir_unsafe_assume_spec_statics/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
all: test.linked-mir.json

test.linked-mir.json: test.rs
saw-rustc $<
$(MAKE) remove-unused-build-artifacts

.PHONY: remove-unused-build-artifacts
remove-unused-build-artifacts:
rm -f test libtest.mir libtest.rlib

.PHONY: clean
clean: remove-unused-build-artifacts
rm -f test.linked-mir.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:1:21: 1:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:1: 1:24"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/65ce71a4::A","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::5c073f3fd0b9c562"},"kind":"Constant"},"kind":"Call","pos":"test.rs:12:5: 12:18"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::5c073f3fd0b9c562"},"kind":"Constant"},"kind":"Call","pos":"test.rs:13:5: 13:18"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}]},"name":"test/65ce71a4::foo","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:5:22: 5:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/65ce71a4::A","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:5:22: 5:23","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:6:9: 6:10","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/65ce71a4::A","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:6:9: 6:14","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"0"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:9:2: 9:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}]},"name":"test/65ce71a4::side_effect","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[{"kind":"body","mutable":true,"name":"test/65ce71a4::A","ty":"ty::u32"}],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/65ce71a4::foo","kind":"Item","substs":[]},"name":"test/65ce71a4::foo"},{"inst":{"def_id":"test/65ce71a4::side_effect","kind":"Item","substs":[]},"name":"test/65ce71a4::side_effect"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::FnDef::5c073f3fd0b9c562","ty":{"defid":"test/65ce71a4::side_effect","kind":"FnDef"}},{"name":"ty::RawPtr::63e5937014067f41","ty":{"kind":"RawPtr","mutability":{"kind":"Mut"},"ty":"ty::u32"}}],"roots":["test/65ce71a4::side_effect","test/65ce71a4::foo"]}
14 changes: 14 additions & 0 deletions intTests/test_mir_unsafe_assume_spec_statics/test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
static mut A: u32 = 42;

pub fn side_effect() -> u32 {
unsafe {
let v: u32 = A;
A = 0;
v
}
}

pub fn foo() -> u32 {
side_effect();
side_effect()
}
56 changes: 56 additions & 0 deletions intTests/test_mir_unsafe_assume_spec_statics/test.saw
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
enable_experimental;

m <- mir_load_module "test.linked-mir.json";

let side_spec_1 = do {
let a_static = mir_static "test::A";
a_init <- mir_fresh_var "A" mir_u32;
mir_points_to a_static (mir_term a_init);

mir_execute_func [];

mir_points_to a_static (mir_term {{ 0 : [32] }});
mir_return (mir_term a_init);
};

let side_spec_2 = do {
let a_static = mir_static "test::A";
a_init <- mir_fresh_var "A" mir_u32;
mir_points_to a_static (mir_term a_init);

mir_execute_func [];

mir_return (mir_term a_init);
};

// This spec is erroneous—see the comments below in the "Avoid unsoundness"
// part of the test.
let foo_spec = do {
let a_static = mir_static "test::A";
a_init <- mir_fresh_var "A" mir_u32;
mir_points_to a_static (mir_term a_init);

mir_execute_func [];

mir_points_to a_static (mir_term {{ 0 : [32] }});
mir_return (mir_term a_init);
};

///////////////////////
// Avoid unsoundness //
///////////////////////

side_ov_1 <- mir_verify m "test::side_effect" [] false side_spec_1 z3;
side_ov_2 <- mir_verify m "test::side_effect" [] false side_spec_2 z3;

// This should not verify, as invoking `side_effect` should cause `foo` to
// always return `0` rather than the original value of A.
fails (
mir_verify m "test::foo" [side_ov_1] false foo_spec z3
);
// This should not verify, as side_spec_2 underspecifies the mutable
// static `a_ptr` in its postconditions. SAW will catch this when attempting
// to use side_ov_2 as an override.
fails (
mir_verify m "test::foo" [side_ov_2] false foo_spec z3
);
3 changes: 3 additions & 0 deletions intTests/test_mir_unsafe_assume_spec_statics/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
set -e

$SAW test.saw
19 changes: 18 additions & 1 deletion src/SAWScript/Crucible/MIR/MethodSpecIR.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# Language DataKinds #-}
{-# Language LambdaCase #-}
{-# Language OverloadedStrings #-}
{-# Language RankNTypes #-}
{-# Language TemplateHaskell #-}
Expand Down Expand Up @@ -33,6 +34,9 @@ module SAWScript.Crucible.MIR.MethodSpecIR
, maMirType
, maLen

, mutIso
, isMut

-- * @MirPointer@
, MirPointer(..)
, mpType
Expand All @@ -51,7 +55,7 @@ module SAWScript.Crucible.MIR.MethodSpecIR
, initialCrucibleSetupState
) where

import Control.Lens (Getter, (^.), to)
import Control.Lens (Getter, Iso', Lens', (^.), iso, to)
import qualified Prettyprinter as PP

import Lang.Crucible.FunctionHandle (HandleAllocator)
Expand Down Expand Up @@ -83,6 +87,19 @@ instance PP.Pretty MirPointsTo where
pretty (MirPointsTo _md ref sv) = PP.parens $
MS.ppSetupValue ref PP.<+> "->" PP.<+> PP.list (map MS.ppSetupValue sv)

mutIso :: Iso' M.Mutability Bool
mutIso =
iso
(\case
M.Mut -> True
M.Immut -> False)
(\case
True -> M.Mut
False -> M.Immut)

isMut :: Lens' (MirAllocSpec tp) Bool
isMut = maMutbl . mutIso

type MIRMethodSpec = MS.CrucibleMethodSpecIR MIR

initialDefCrucibleMethodSpecIR ::
Expand Down
Loading

0 comments on commit 2e79a1e

Please sign in to comment.