better error message when the program tries to spawn a thread

Author: RalfJung

src/lib.rs

@@ -38,7 +38,7 @@ pub use crate::helpers::{EvalContextExt as HelpersEvalContextExt};
 pub use crate::mono_hash_map::MonoHashMap;
 pub use crate::stacked_borrows::{EvalContextExt as StackedBorEvalContextExt, Tag, Permission, Stack, Stacks, Item};
 pub use crate::machine::{
-    PAGE_SIZE, STACK_ADDR, NUM_CPUS,
+    PAGE_SIZE, STACK_ADDR, STACK_SIZE, NUM_CPUS,
     MemoryExtra, AllocExtra, MiriMemoryKind, Evaluator, MiriEvalContext, MiriEvalContextExt,
 };
 pub use crate::eval::{eval_main, create_ecx, MiriConfig};

src/machine.rs

@@ -18,7 +18,8 @@ use crate::*;
 
 // Some global facts about the emulated machine.
 pub const PAGE_SIZE: u64 = 4*1024; // FIXME: adjust to target architecture
-pub const STACK_ADDR: u64 = 16*PAGE_SIZE; // not really about the "stack", but where we start assigning integer addresses to allocations
+pub const STACK_ADDR: u64 = 32*PAGE_SIZE; // not really about the "stack", but where we start assigning integer addresses to allocations
+pub const STACK_SIZE: u64 = 16*PAGE_SIZE; // whatever
 pub const NUM_CPUS: u64 = 1;
 
 /// Extra memory kinds

src/shims/dlsym.rs

@@ -8,11 +8,17 @@ pub enum Dlsym {
 }
 
 impl Dlsym {
-    pub fn from_str(name: &str) -> Option<Dlsym> {
+    // Returns an error for unsupported symbols, and None if this symbol
+    // should become a NULL pointer (pretend it does not exist).
+    pub fn from_str(name: &str) -> InterpResult<'static, Option<Dlsym>> {
         use self::Dlsym::*;
-        Some(match name {
-            "getentropy" => GetEntropy,
-            _ => return None,
+        Ok(match name {
+            "getentropy" => Some(GetEntropy),
+            "__pthread_get_minstack" => None,
+            _ =>
+                return err!(Unimplemented(format!(
+                    "Unsupported dlsym: {}", name
+                ))),
         })
     }
 }
@@ -32,7 +38,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
 
         let dest = dest.expect("we don't support any diverging dlsym");
         let ret = ret.expect("dest is `Some` but ret is `None`");
-        
+
         match dlsym {
             GetEntropy => {
                 let ptr = this.read_scalar(args[0])?.not_undef()?;

src/shims/foreign_items.rs

@@ -324,13 +324,11 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
                 let symbol_name = this.memory().get(symbol.alloc_id)?.read_c_str(tcx, symbol)?;
                 let err = format!("bad c unicode symbol: {:?}", symbol_name);
                 let symbol_name = ::std::str::from_utf8(symbol_name).unwrap_or(&err);
-                if let Some(dlsym) = Dlsym::from_str(symbol_name) {
+                if let Some(dlsym) = Dlsym::from_str(symbol_name)? {
                     let ptr = this.memory_mut().create_fn_alloc(FnVal::Other(dlsym));
                     this.write_scalar(Scalar::from(ptr), dest)?;
                 } else {
-                    return err!(Unimplemented(format!(
-                        "Unsupported dlsym: {}", symbol_name
-                    )));
+                    this.write_null(dest)?;
                 }
             }
 
@@ -713,24 +711,31 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
                 this.write_null(dest)?;
             }
 
-            // Determine stack base address.
-            "pthread_attr_init" | "pthread_attr_destroy" | "pthread_attr_get_np" |
-            "pthread_getattr_np" | "pthread_self" | "pthread_get_stacksize_np" => {
+            // Stack size/address stuff.
+            "pthread_attr_init" | "pthread_attr_destroy" | "pthread_self" |
+            "pthread_attr_setstacksize" => {
                 this.write_null(dest)?;
             }
             "pthread_attr_getstack" => {
-                // Second argument is where we are supposed to write the stack size.
-                let ptr = this.deref_operand(args[1])?;
-                // Just any address.
-                let stack_addr = Scalar::from_uint(STACK_ADDR, args[1].layout.size);
-                this.write_scalar(stack_addr, ptr.into())?;
+                let addr_place = this.deref_operand(args[1])?;
+                let size_place = this.deref_operand(args[2])?;
+
+                this.write_scalar(
+                    Scalar::from_uint(STACK_ADDR, addr_place.layout.size),
+                    addr_place.into(),
+                )?;
+                this.write_scalar(
+                    Scalar::from_uint(STACK_SIZE, size_place.layout.size),
+                    size_place.into(),
+                )?;
+
                 // Return success (`0`).
                 this.write_null(dest)?;
             }
-            "pthread_get_stackaddr_np" => {
-                // Just any address.
-                let stack_addr = Scalar::from_uint(STACK_ADDR, dest.layout.size);
-                this.write_scalar(stack_addr, dest)?;
+
+            // We don't support threading.
+            "pthread_create" => {
+                return err!(Unimplemented(format!("Miri does not support threading")));
             }
 
             // Stub out calls for condvar, mutex and rwlock, to just return `0`.
@@ -758,6 +763,17 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
             }
 
             // macOS API stubs.
+            "pthread_attr_get_np" | "pthread_getattr_np" => {
+                this.write_null(dest)?;
+            }
+            "pthread_get_stackaddr_np" => {
+                let stack_addr = Scalar::from_uint(STACK_ADDR, dest.layout.size);
+                this.write_scalar(stack_addr, dest)?;
+            }
+            "pthread_get_stacksize_np" => {
+                let stack_size = Scalar::from_uint(STACK_SIZE, dest.layout.size);
+                this.write_scalar(stack_size, dest)?;
+            }
             "_tlv_atexit" => {
                 // FIXME: register the destructor.
             },

tests/compile-fail/thread-spawn.rs

@@ -0,0 +1,7 @@
+use std::thread;
+
+// error-pattern: Miri does not support threading
+
+fn main() {
+    thread::spawn(|| {});
+}