Direct source const_at/expect_const, to_value, to_branch and to_leaf queries for atomic and SIMD intrinsics. These inspect canonical compiler constants; they do not normalize aliases or invent const evaluation. Source compiler invariants are explicit invalid-program errors, while absent imported metadata remains unsupported.

def Miri.Input.CompilerIntrinsicConstants.ordering (p : CompilerIntrinsicFacts.Prepared) (callee : Interpreter.CallInstance) (index : Nat) : Except Interpreter.StepError Concurrency.AtomicOrdering

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.CompilerIntrinsicConstants.volatile (p : CompilerIntrinsicFacts.Prepared) (callee : Interpreter.CallInstance) (index : Nat) : Except Interpreter.StepError Unit

Source atomic_load/store only calls to_value; the volatile value is ignored.

Equations

• Miri.Input.CompilerIntrinsicConstants.volatile p callee index = do let _ ← Miri.Input.CompilerIntrinsicConstants.argument✝ p callee index pure ()

def Miri.Input.CompilerIntrinsicConstants.shuffle (p : CompilerIntrinsicFacts.Prepared) (callee : Interpreter.CallInstance) (index : Nat) : Except Interpreter.StepError (Array UInt32)

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.CompilerIntrinsicConstants.alignment (p : CompilerIntrinsicFacts.Prepared) (callee : Interpreter.CallInstance) (index : Nat) : Except Interpreter.StepError Memory.SimdAlignment

Equations

• One or more equations did not get rendered due to their size.

def Miri.Input.CompilerIntrinsicConstants.hooks {K User C Other Extern Host : Type} (p : CompilerIntrinsicFacts.Prepared) (base : Interpreter.ExecutionMachine.Config K User C Other Extern Host) : Interpreter.ExecutionMachine.Config K User C Other Extern Host

Equations

• One or more equations did not get rendered due to their size.