Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

mir_tuple_value #1934

Merged
merged 2 commits into from
Sep 11, 2023
Merged

mir_tuple_value #1934

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d4acee4
mir_tuple_value
RyanGlScott Sep 2, 2023
124709b
manual.md: Correctly use MIRValue, not SetupValue, in MIR commands
RyanGlScott Sep 6, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions crucible-mir-comp/src/Mir/Compositional/Builder.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -636,6 +636,7 @@ substMethodSpec sc sm ms = do
MS.SetupTerm tt -> MS.SetupTerm <$> goTypedTerm tt
MS.SetupNull _ -> return sv
MS.SetupStruct b svs -> MS.SetupStruct b <$> mapM goSetupValue svs
MS.SetupTuple b svs -> MS.SetupTuple b <$> mapM goSetupValue svs
MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs
MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx
MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name
Expand Down Expand Up @@ -677,14 +678,14 @@ regToSetup bak p eval shp rv = go shp rv

go :: forall tp. TypeShape tp -> RegValue sym tp ->
BuilderT sym t (OverrideSim p sym MIR rtp args ret) (MS.SetupValue MIR)
go (UnitShape _) () = return $ MS.SetupStruct () []
go (UnitShape _) () = return $ MS.SetupTuple () []
go (PrimShape _ btpr) expr = do
-- Record all vars used in `expr`
cache <- use msbVisitCache
visitExprVars cache expr $ \var -> do
msbPrePost p . seVars %= Set.insert (Some var)
liftIO $ MS.SetupTerm <$> eval btpr expr
go (TupleShape _ _ flds) rvs = MS.SetupStruct () <$> goFields flds rvs
go (TupleShape _ _ flds) rvs = MS.SetupTuple () <$> goFields flds rvs
go (ArrayShape _ elemTy shp) vec = do
svs <- case vec of
MirVector_Vector v -> mapM (go shp) (toList v)
Expand Down
8 changes: 4 additions & 4 deletions crucible-mir-comp/src/Mir/Compositional/Override.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -356,7 +356,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
where
go :: forall tp. TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR ->
MirOverrideMatcher sym ()
go (UnitShape _) () (MS.SetupStruct () []) = return ()
go (UnitShape _) () (MS.SetupTuple () []) = return ()
go (PrimShape _ _btpr) expr (MS.SetupTerm tt) = do
loc <- use MS.osLocation
exprTerm <- liftIO $ eval expr
Expand Down Expand Up @@ -390,7 +390,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
("mismatch on " ++ show (W4.exprType expr) ++ ": expected " ++
show (W4.printSymExpr val))
""
go (TupleShape _ _ flds) rvs (MS.SetupStruct () svs) = goFields flds rvs svs
go (TupleShape _ _ flds) rvs (MS.SetupTuple () svs) = goFields flds rvs svs
go (ArrayShape _ _ shp) vec (MS.SetupArray _ svs) = case vec of
MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs
MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do
Expand Down Expand Up @@ -510,7 +510,7 @@ setupToReg :: forall sym t st fs tp.
setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
where
go :: forall tp. TypeShape tp -> MS.SetupValue MIR -> IO (RegValue sym tp)
go (UnitShape _) (MS.SetupStruct _ []) = return ()
go (UnitShape _) (MS.SetupTuple _ []) = return ()
go (PrimShape _ btpr) (MS.SetupTerm tt) = do
term <- liftIO $ SAW.scInstantiateExt sc termSub $ SAW.ttTerm tt
Some expr <- termToExpr sym sc regMap term
Expand All @@ -519,7 +519,7 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
Nothing -> error $ "setupToReg: expected " ++ show btpr ++ ", but got " ++
show (W4.exprType expr)
return expr
go (TupleShape _ _ flds) (MS.SetupStruct _ svs) = goFields flds svs
go (TupleShape _ _ flds) (MS.SetupTuple _ svs) = goFields flds svs
go (ArrayShape _ _ shp) (MS.SetupArray _ svs) = do
rvs <- mapM (go shp) svs
return $ MirVector_Vector $ V.fromList rvs
Expand Down
10 changes: 6 additions & 4 deletions doc/manual/manual.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2435,9 +2435,9 @@ The experimental MIR implementation also has a `mir_alloc` function, which
behaves similarly to `llvm_alloc`. `mir_alloc` creates an immutable reference,
but there is also a `mir_alloc_mut` function for creating a mutable reference:

* `mir_alloc : MIRType -> MIRSetup SetupValue`
* `mir_alloc : MIRType -> MIRSetup MIRValue`

* `mir_alloc_mut : MIRType -> MIRSetup SetupValue`
* `mir_alloc_mut : MIRType -> MIRSetup MIRValue`

MIR tracks whether references are mutable or immutable at the type level, so it
is important to use the right allocation command for a given reference type.
Expand Down Expand Up @@ -2538,7 +2538,7 @@ value.

MIR verification has a single `mir_points_to` command:

* `mir_points_to : SetupValue -> SetupValue -> MIRSetup ()`
* `mir_points_to : MIRValue -> MIRValue -> MIRSetup ()`
takes two `SetupValue` arguments, the first of which must be a reference,
and states that the memory specified by that reference should contain the
value given in the second argument (which may be any type of
Expand Down Expand Up @@ -2624,9 +2624,11 @@ specifies the name of an object field.
In the experimental MIR verification implementation, the following functions
construct compound values:

* `mir_array_value : MIRType -> [SetupValue] -> SetupValue` constructs an array
* `mir_array_value : MIRType -> [MIRValue] -> MIRValue` constructs an array
of the given type whose elements consist of the given values. Supplying the
element type is necessary to support length-0 arrays.
* `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given
list of values as elements.

### Bitfields

Expand Down
13 changes: 13 additions & 0 deletions intTests/test_mir_verify_tuples/Makefile
View file
Open in desktop
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
1 change: 1 addition & 0 deletions intTests/test_mir_verify_tuples/test.linked-mir.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:10:13: 10:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:11:13: 11:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"test.rs:12:11: 12:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:12:11: 12:28"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"pos":"test.rs:12:5: 12:28","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}},"pos":"test.rs:13:11: 13:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:13:11: 13:28"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"pos":"test.rs:13:5: 13:28","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb2"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}]},"name":"test/34c2a073::h","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:2:6: 2:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:2:6: 2:25"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"test.rs:2:27: 2:30","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:2:27: 2:46"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:2:5: 2:47"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:2:5: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:2:5: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}]},"name":"test/34c2a073::f","return_ty":"ty::Tuple::f54c7b3282e27392","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:6:6: 6:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:6: 6:25"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"test.rs:6:27: 6:30","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:27: 6:46"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:6:5: 6:47"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:6:5: 6:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:6:5: 6:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}]},"name":"test/34c2a073::g","return_ty":"ty::Tuple::f54c7b3282e27392","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:13: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1163:10: 1163:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}]},"name":"core/73237d41::num::{impl#9}::wrapping_add","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/34c2a073::h","kind":"Item","substs":[]},"name":"test/34c2a073::h"},{"inst":{"def_id":"test/34c2a073::f","kind":"Item","substs":[]},"name":"test/34c2a073::f"},{"inst":{"def_id":"test/34c2a073::g","kind":"Item","substs":[]},"name":"test/34c2a073::g"},{"inst":{"def_id":"core/73237d41::num::{impl#9}::wrapping_add","kind":"Item","substs":[]},"name":"core/73237d41::num::{impl#9}::wrapping_add"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}},{"name":"ty::Ref::25602b11826e1882","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Tuple::f54c7b3282e27392"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::f55acdef755f1aaa","ty":{"defid":"core/73237d41::num::{impl#9}::wrapping_add","kind":"FnDef"}},{"name":"ty::Ref::22d6f3c23aaa2830","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Tuple::f54c7b3282e27392"}}],"roots":["test/34c2a073::f","test/34c2a073::g","test/34c2a073::h"]}
14 changes: 14 additions & 0 deletions intTests/test_mir_verify_tuples/test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
pub fn f(s: (u32, u32)) -> (u32, u32) {
(s.1.wrapping_add(1), s.0.wrapping_add(2))
}

pub fn g(s: &(u32, u32)) -> (u32, u32) {
(s.1.wrapping_add(1), s.0.wrapping_add(2))
}

pub fn h(s: &mut (u32, u32)) {
let x = s.0;
let y = s.1;
s.0 = y.wrapping_add(1);
s.1 = x.wrapping_add(2);
}
Loading