fn process_events()

in smt2proxy/src/main.rs [130:208]

• 71 lines of code
• 6 McCabe index (conditional complexity)

fn process_events(
    receiver: std::sync::mpsc::Receiver<Event>,
    z3_args: Vec<String>,
    mut processor: smt2proxy::CommandProcessor,
) {
    if let Some(logger) = processor.logger() {
        let mut f = logger.lock().unwrap();
        writeln!(
            f,
            "; z3 {}",
            z3_args
                .iter()
                .map(|x| format!("\"{}\"", x))
                .collect::<Vec<_>>()
                .join(" ")
        )
        .unwrap();
    }

    let mut child = std::process::Command::new("z3")
        .args(&z3_args)
        .stdin(std::process::Stdio::piped())
        .stdout(std::process::Stdio::piped())
        .stderr(std::process::Stdio::piped())
        .spawn()
        .unwrap();

    let handler_stdout = spawn_child_stream_logger(
        processor.logger().clone(),
        child.stdout.take().expect("Failed to open child stdout"),
        /* repeat */ true,
        "Failed to read child stdout",
    );

    let handler_stderr = spawn_child_stream_logger(
        processor.logger().clone(),
        child.stderr.take().expect("Failed to open child stderr"),
        /* repeat */ false,
        "Failed to read child stderr",
    );

    {
        let mut child_stdin = child.stdin.take().expect("Failed to open child stdin");

        while let Ok(event) = receiver.recv() {
            match event {
                Event::Query(value) => match *value {
                    Ok(in_command) => {
                        let out_commands = processor.process(in_command);
                        for command in out_commands {
                            writeln!(child_stdin, "{}", command)
                                .expect("Failed to write to child stdin");
                        }
                    }
                    Err(error) => {
                        if let Some(logger) = processor.logger() {
                            let mut f = logger.lock().unwrap();
                            writeln!(f, "; {}", error).expect("Failed to write to log file");
                        }
                        break;
                    }
                },
                Event::Done => {
                    break;
                }
            }
        }
        let out_commands = processor.stop();
        for command in out_commands {
            writeln!(child_stdin, "{}", command).expect("Failed to write to child stdin");
        }
    }
    // child_stdin is now closed.
    // Wait for z3 to read EOF and terminate normally.
    child.wait().unwrap();
    // Wait for the child stream loggers to read EOF and terminate.
    handler_stdout.join().unwrap();
    handler_stderr.join().unwrap();
}