1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00

Compare commits

...

3 Commits

Author SHA1 Message Date
monsterkrampe
a0ad716b28
WIP: return immediately for solving and add get endpoint 2023-03-31 16:27:45 +02:00
monsterkrampe
ba752514ce
Satisfy clippy for server code 2023-03-31 15:11:23 +02:00
monsterkrampe
565683721d
Add API for getting and updating user 2023-03-31 15:07:54 +02:00
6 changed files with 262 additions and 53 deletions

23
Cargo.lock generated
View File

@ -283,6 +283,7 @@ dependencies = [
"adf_bdd", "adf_bdd",
"argon2", "argon2",
"env_logger 0.9.3", "env_logger 0.9.3",
"futures-util",
"log", "log",
"mongodb", "mongodb",
"names", "names",
@ -1143,9 +1144,9 @@ dependencies = [
[[package]] [[package]]
name = "futures-core" name = "futures-core"
version = "0.3.27" version = "0.3.28"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "86d7a0c1aa76363dac491de0ee99faf6941128376f1cf96f07db7603b7de69dd" checksum = "4bca583b7e26f571124fe5b7561d49cb2868d79116cfa0eefce955557c6fee8c"
[[package]] [[package]]
name = "futures-executor" name = "futures-executor"
@ -1160,19 +1161,19 @@ dependencies = [
[[package]] [[package]]
name = "futures-io" name = "futures-io"
version = "0.3.27" version = "0.3.28"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "89d422fa3cbe3b40dca574ab087abb5bc98258ea57eea3fd6f1fa7162c778b91" checksum = "4fff74096e71ed47f8e023204cfd0aa1289cd54ae5430a9523be060cdb849964"
[[package]] [[package]]
name = "futures-macro" name = "futures-macro"
version = "0.3.27" version = "0.3.28"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3eb14ed937631bd8b8b8977f2c198443447a8355b6e3ca599f38c975e5a963b6" checksum = "89ca545a94061b6365f2c7355b4b32bd20df3ff95f02da9329b34ccc3bd6ee72"
dependencies = [ dependencies = [
"proc-macro2", "proc-macro2",
"quote", "quote",
"syn 1.0.109", "syn 2.0.8",
] ]
[[package]] [[package]]
@ -1183,15 +1184,15 @@ checksum = "ec93083a4aecafb2a80a885c9de1f0ccae9dbd32c2bb54b0c3a65690e0b8d2f2"
[[package]] [[package]]
name = "futures-task" name = "futures-task"
version = "0.3.27" version = "0.3.28"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "fd65540d33b37b16542a0438c12e6aeead10d4ac5d05bd3f805b8f35ab592879" checksum = "76d3d132be6c0e6aa1534069c705a74a5997a356c0dc2f86a47765e5617c5b65"
[[package]] [[package]]
name = "futures-util" name = "futures-util"
version = "0.3.27" version = "0.3.28"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3ef6b17e481503ec85211fed8f39d1970f128935ca1f814cd32ac4a6842e84ab" checksum = "26b01e40b772d54cf6c6d721c1d1abd0647a0106a12ecaa1c186273392a69533"
dependencies = [ dependencies = [
"futures-core", "futures-core",
"futures-io", "futures-io",

View File

@ -24,6 +24,7 @@ actix-identity = "0.5.2"
argon2 = "0.5.0" argon2 = "0.5.0"
actix-session = { version="0.7.2", features = ["cookie-session"] } actix-session = { version="0.7.2", features = ["cookie-session"] }
names = "0.14.0" names = "0.14.0"
futures-util = "0.3.28"
[features] [features]
cors_for_local_development = [] cors_for_local_development = []

View File

@ -1,16 +1,18 @@
use std::collections::HashMap; use std::collections::{HashMap, HashSet};
use std::sync::{Arc, RwLock}; use std::sync::{Arc, RwLock};
use actix_identity::Identity; use actix_identity::Identity;
use actix_web::rt::spawn;
use actix_web::rt::task::spawn_blocking; use actix_web::rt::task::spawn_blocking;
use actix_web::rt::time::timeout; use actix_web::rt::time::timeout;
use actix_web::{post, put, web, HttpMessage, HttpRequest, HttpResponse, Responder}; use actix_web::{get, post, put, web, HttpMessage, HttpRequest, HttpResponse, Responder};
use adf_bdd::datatypes::adf::VarContainer; use adf_bdd::datatypes::adf::VarContainer;
use adf_bdd::datatypes::{BddNode, Term, Var}; use adf_bdd::datatypes::{BddNode, Term, Var};
use mongodb::bson::doc; use mongodb::bson::doc;
use mongodb::bson::{to_bson, Bson}; use mongodb::bson::{to_bson, Bson};
use names::{Generator, Name}; use names::{Generator, Name};
use serde::{Deserialize, Serialize}; use serde::{Deserialize, Serialize};
use futures_util::FutureExt;
use adf_bdd::adf::{Adf, DoubleLabeledGraph}; use adf_bdd::adf::{Adf, DoubleLabeledGraph};
use adf_bdd::adfbiodivine::Adf as BdAdf; use adf_bdd::adfbiodivine::Adf as BdAdf;
@ -22,13 +24,13 @@ use crate::user::{username_exists, User};
type Ac = Vec<Term>; type Ac = Vec<Term>;
type AcDb = Vec<String>; type AcDb = Vec<String>;
#[derive(Clone, Deserialize, Serialize)] #[derive(Copy, Clone, Deserialize, Serialize)]
pub(crate) enum Parsing { pub(crate) enum Parsing {
Naive, Naive,
Hybrid, Hybrid,
} }
#[derive(Clone, PartialEq, Eq, Hash, Deserialize, Serialize)] #[derive(Copy, Clone, PartialEq, Eq, Hash, Deserialize, Serialize)]
pub(crate) enum Strategy { pub(crate) enum Strategy {
Ground, Ground,
Complete, Complete,
@ -44,9 +46,9 @@ pub(crate) struct AcAndGraph {
pub(crate) graph: DoubleLabeledGraph, pub(crate) graph: DoubleLabeledGraph,
} }
impl Into<Bson> for AcAndGraph { impl From<AcAndGraph> for Bson {
fn into(self) -> Bson { fn from(source: AcAndGraph) -> Self {
to_bson(&self).expect("Serialization should work") to_bson(&source).expect("Serialization should work")
} }
} }
@ -175,6 +177,32 @@ async fn adf_problem_exists(
.is_some() .is_some()
} }
#[derive(Serialize)]
struct AdfProblemInfo {
name: String,
code: String,
parsing_used: Parsing,
acs_per_strategy: AcsPerStrategy,
running_tasks: Vec<Task>,
}
impl AdfProblemInfo {
fn from_adf_prob_and_tasks(adf: AdfProblem, tasks: &HashSet<RunningInfo>) -> Self {
AdfProblemInfo {
name: adf.name.clone(),
code: adf.code,
parsing_used: adf.parsing_used,
acs_per_strategy: adf.acs_per_strategy,
running_tasks: tasks
.iter()
.filter_map(|t| {
(t.adf_name == adf.name && t.username == adf.username).then_some(t.task)
})
.collect(),
}
}
}
#[post("/add")] #[post("/add")]
async fn add_adf_problem( async fn add_adf_problem(
req: HttpRequest, req: HttpRequest,
@ -274,6 +302,8 @@ async fn add_adf_problem(
let adf_problem_input_clone = adf_problem_input.clone(); let adf_problem_input_clone = adf_problem_input.clone();
let username_clone = username.clone(); let username_clone = username.clone();
let problem_name_clone = problem_name.clone(); let problem_name_clone = problem_name.clone();
// TODO: change this: we want to return a response from the request whil the computation is running
let adf_res = timeout( let adf_res = timeout(
COMPUTE_TIME, COMPUTE_TIME,
spawn_blocking(move || { spawn_blocking(move || {
@ -297,9 +327,7 @@ async fn add_adf_problem(
Parsing::Naive => Adf::from_parser(&parser), Parsing::Naive => Adf::from_parser(&parser),
Parsing::Hybrid => { Parsing::Hybrid => {
let bd_adf = BdAdf::from_parser(&parser); let bd_adf = BdAdf::from_parser(&parser);
let naive_adf = bd_adf.hybrid_step_opt(false); bd_adf.hybrid_step_opt(false)
naive_adf
} }
}; };
@ -324,8 +352,10 @@ async fn add_adf_problem(
Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()), Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
Ok(Ok(Err(err))) => HttpResponse::InternalServerError().body(err.to_string()), Ok(Ok(Err(err))) => HttpResponse::InternalServerError().body(err.to_string()),
Ok(Ok(Ok((adf, ac_and_graph)))) => { Ok(Ok(Ok((adf, ac_and_graph)))) => {
let mut acs = AcsPerStrategy::default(); let acs = AcsPerStrategy {
acs.parse_only = Some(vec![ac_and_graph]); parse_only: Some(vec![ac_and_graph]),
..Default::default()
};
let adf_problem: AdfProblem = AdfProblem { let adf_problem: AdfProblem = AdfProblem {
name: problem_name, name: problem_name,
@ -339,7 +369,7 @@ async fn add_adf_problem(
let result = adf_coll.insert_one(&adf_problem, None).await; let result = adf_coll.insert_one(&adf_problem, None).await;
match result { match result {
Ok(_) => HttpResponse::Ok().json(adf_problem), // TODO: return name of problem here (especially since it may be generated) Ok(_) => HttpResponse::Ok().json(AdfProblemInfo::from_adf_prob_and_tasks(adf_problem, &HashSet::new())), // there should be no tasks running here
Err(err) => HttpResponse::InternalServerError().body(err.to_string()), Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
} }
} }
@ -403,7 +433,9 @@ async fn solve_adf_problem(
let username_clone = username.clone(); let username_clone = username.clone();
let problem_name_clone = problem_name.clone(); let problem_name_clone = problem_name.clone();
let strategy_clone = adf_problem_input.strategy.clone(); let strategy_clone = adf_problem_input.strategy.clone();
let acs_and_graphs_res = timeout(
// TODO: change this: we want to return a response from the request whil the computation is running
let acs_and_graphs_fut = timeout(
COMPUTE_TIME, COMPUTE_TIME,
spawn_blocking(move || { spawn_blocking(move || {
let running_info = RunningInfo { let running_info = RunningInfo {
@ -459,26 +491,68 @@ async fn solve_adf_problem(
acs_and_graphs acs_and_graphs
}), }),
) );
.await;
match acs_and_graphs_res { spawn(acs_and_graphs_fut.then(move |acs_and_graphs_res| async move {
Err(err) => HttpResponse::InternalServerError().body(err.to_string()), match acs_and_graphs_res {
Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()), // TODO: error states should somehow be set in the database since the status codes are irrelevant in this future
Ok(Ok(acs_and_graphs)) => { Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
let result = adf_coll.update_one(doc! { "name": &problem_name, "username": &username }, match adf_problem_input.strategy { Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
Strategy::Complete => doc! { "$set": { "acs_per_strategy.complete": Some(&acs_and_graphs) } }, Ok(Ok(acs_and_graphs)) => {
Strategy::Ground => doc! { "$set": { "acs_per_strategy.ground": Some(&acs_and_graphs) } }, let result = adf_coll.update_one(doc! { "name": problem_name, "username": username }, match adf_problem_input.strategy {
Strategy::Stable => doc! { "$set": { "acs_per_strategy.stable": Some(&acs_and_graphs) } }, Strategy::Complete => doc! { "$set": { "acs_per_strategy.complete": Some(&acs_and_graphs) } },
Strategy::StableCountingA => doc! { "$set": { "acs_per_strategy.stable_counting_a": Some(&acs_and_graphs) } }, Strategy::Ground => doc! { "$set": { "acs_per_strategy.ground": Some(&acs_and_graphs) } },
Strategy::StableCountingB => doc! { "$set": { "acs_per_strategy.stable_counting_b": Some(&acs_and_graphs) } }, Strategy::Stable => doc! { "$set": { "acs_per_strategy.stable": Some(&acs_and_graphs) } },
Strategy::StableNogood => doc! { "$set": { "acs_per_strategy.stable_nogood": Some(&acs_and_graphs) } }, Strategy::StableCountingA => doc! { "$set": { "acs_per_strategy.stable_counting_a": Some(&acs_and_graphs) } },
}, None).await; Strategy::StableCountingB => doc! { "$set": { "acs_per_strategy.stable_counting_b": Some(&acs_and_graphs) } },
Strategy::StableNogood => doc! { "$set": { "acs_per_strategy.stable_nogood": Some(&acs_and_graphs) } },
}, None).await;
match result { match result {
Ok(_) => HttpResponse::Ok().json(acs_and_graphs), Ok(_) => HttpResponse::Ok().json(acs_and_graphs),
Err(err) => HttpResponse::InternalServerError().body(err.to_string()), Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
} }
} };
} }));
HttpResponse::Ok().body("Parsing started...")
}
#[get("/{problem_name}")]
async fn get_adf_problem(
app_state: web::Data<AppState>,
identity: Option<Identity>,
path: web::Path<String>,
) -> impl Responder {
let problem_name = path.into_inner();
let adf_coll: mongodb::Collection<AdfProblem> = app_state
.mongodb_client
.database(DB_NAME)
.collection(ADF_COLL);
let username = match identity.map(|id| id.id()) {
None => {
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
}
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
Some(Ok(username)) => username,
};
let adf_problem = match adf_coll
.find_one(doc! { "name": &problem_name, "username": &username }, None)
.await
{
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
Ok(None) => {
return HttpResponse::NotFound()
.body(format!("ADF problem with name {problem_name} not found."))
}
Ok(Some(prob)) => prob,
};
HttpResponse::Ok().json(AdfProblemInfo::from_adf_prob_and_tasks(
adf_problem,
&app_state.currently_running.lock().unwrap(),
))
} }

View File

@ -3,6 +3,7 @@ use std::sync::Mutex;
use std::time::Duration; use std::time::Duration;
use mongodb::Client; use mongodb::Client;
use serde::Serialize;
use crate::adf::Strategy; use crate::adf::Strategy;
@ -16,7 +17,7 @@ pub(crate) const DB_NAME: &str = "adf-obdd";
pub(crate) const USER_COLL: &str = "users"; pub(crate) const USER_COLL: &str = "users";
pub(crate) const ADF_COLL: &str = "adf-problems"; pub(crate) const ADF_COLL: &str = "adf-problems";
#[derive(Clone, PartialEq, Eq, Hash)] #[derive(Copy, Clone, PartialEq, Eq, Hash, Serialize)]
pub(crate) enum Task { pub(crate) enum Task {
Parse, Parse,
Solve(Strategy), Solve(Strategy),

View File

@ -19,7 +19,9 @@ mod user;
use adf::{add_adf_problem, solve_adf_problem}; use adf::{add_adf_problem, solve_adf_problem};
use config::{AppState, ASSET_DIRECTORY, COOKIE_DURATION}; use config::{AppState, ASSET_DIRECTORY, COOKIE_DURATION};
use user::{create_username_index, delete_account, login, logout, register}; use user::{
create_username_index, delete_account, login, logout, register, update_user, user_info,
};
#[actix_web::main] #[actix_web::main]
async fn main() -> std::io::Result<()> { async fn main() -> std::io::Result<()> {
@ -38,7 +40,7 @@ async fn main() -> std::io::Result<()> {
// cookie secret ket // cookie secret ket
let secret_key = Key::generate(); let secret_key = Key::generate();
let server = HttpServer::new(move || { HttpServer::new(move || {
let app = App::new(); let app = App::new();
#[cfg(feature = "cors_for_local_development")] #[cfg(feature = "cors_for_local_development")]
@ -73,7 +75,9 @@ async fn main() -> std::io::Result<()> {
.service(register) .service(register)
.service(delete_account) .service(delete_account)
.service(login) .service(login)
.service(logout), .service(logout)
.service(user_info)
.service(update_user),
) )
.service( .service(
web::scope("/adf") web::scope("/adf")
@ -85,7 +89,5 @@ async fn main() -> std::io::Result<()> {
}) })
.bind(("0.0.0.0", 8080))? .bind(("0.0.0.0", 8080))?
.run() .run()
.await; .await
server
} }

View File

@ -1,9 +1,9 @@
use actix_identity::Identity; use actix_identity::Identity;
use actix_web::{delete, post, web, HttpMessage, HttpRequest, HttpResponse, Responder}; use actix_web::{delete, get, post, put, web, HttpMessage, HttpRequest, HttpResponse, Responder};
use argon2::password_hash::rand_core::OsRng; use argon2::password_hash::rand_core::OsRng;
use argon2::password_hash::SaltString; use argon2::password_hash::SaltString;
use argon2::{Argon2, PasswordHash, PasswordHasher, PasswordVerifier}; use argon2::{Argon2, PasswordHash, PasswordHasher, PasswordVerifier};
use mongodb::results::DeleteResult; use mongodb::results::{DeleteResult, UpdateResult};
use mongodb::{bson::doc, options::IndexOptions, Client, IndexModel}; use mongodb::{bson::doc, options::IndexOptions, Client, IndexModel};
use serde::{Deserialize, Serialize}; use serde::{Deserialize, Serialize};
@ -22,6 +22,12 @@ struct UserPayload {
password: String, password: String,
} }
#[derive(Deserialize, Serialize)]
struct UserInfo {
username: String,
temp: bool,
}
// Creates an index on the "username" field to force the values to be unique. // Creates an index on the "username" field to force the values to be unique.
pub(crate) async fn create_username_index(client: &Client) { pub(crate) async fn create_username_index(client: &Client) {
let options = IndexOptions::builder().unique(true).build(); let options = IndexOptions::builder().unique(true).build();
@ -215,3 +221,127 @@ async fn logout(app_state: web::Data<AppState>, id: Option<Identity>) -> impl Re
}, },
} }
} }
// Get current user
#[get("/info")]
async fn user_info(app_state: web::Data<AppState>, identity: Option<Identity>) -> impl Responder {
let user_coll: mongodb::Collection<User> = app_state
.mongodb_client
.database(DB_NAME)
.collection(USER_COLL);
match identity.map(|id| id.id()) {
None => {
HttpResponse::Unauthorized().body("You need to login get your account information.")
}
Some(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
Some(Ok(username)) => {
match user_coll
.find_one(doc! { "username": &username }, None)
.await
{
Ok(Some(user)) => {
let info = UserInfo {
username: user.username,
temp: user.password.is_none(),
};
HttpResponse::Ok().json(info)
}
Ok(None) => HttpResponse::NotFound().body("Logged in user does not exist anymore."),
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
}
}
}
// Update current user
#[put("/update")]
async fn update_user(
req: HttpRequest,
app_state: web::Data<AppState>,
identity: Option<Identity>,
user: web::Json<UserPayload>,
) -> impl Responder {
let mut user: UserPayload = user.into_inner();
let user_coll = app_state
.mongodb_client
.database(DB_NAME)
.collection(USER_COLL);
let adf_coll: mongodb::Collection<AdfProblem> = app_state
.mongodb_client
.database(DB_NAME)
.collection(ADF_COLL);
match identity {
None => {
HttpResponse::Unauthorized().body("You need to login get your account information.")
}
Some(id) => match id.id() {
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
Ok(username) => {
if user.username != username && username_exists(&user_coll, &user.username).await {
return HttpResponse::Conflict()
.body("Username is already taken. Please pick another one!");
}
let pw = &user.password;
let salt = SaltString::generate(&mut OsRng);
let hashed_pw = Argon2::default()
.hash_password(pw.as_bytes(), &salt)
.expect("Error while hashing password!")
.to_string();
user.password = hashed_pw;
let result = user_coll
.replace_one(
doc! { "username": &username },
User {
username: user.username.clone(),
password: Some(user.password),
},
None,
)
.await;
match result {
Ok(UpdateResult {
modified_count: 0, ..
}) => HttpResponse::InternalServerError().body("Account could not be updated."),
Ok(UpdateResult {
modified_count: 1, ..
}) => {
// re-login with new username
Identity::login(&req.extensions(), user.username.clone()).unwrap();
// update all adf problems of user
match adf_coll
.update_many(
doc! { "username": &username },
doc! { "$set": { "username": &user.username } },
None,
)
.await
{
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
Ok(UpdateResult {
modified_count: 0, ..
}) => HttpResponse::InternalServerError()
.body("Account could not be updated."),
Ok(UpdateResult {
modified_count: _, ..
}) => HttpResponse::Ok().json(UserInfo {
username: user.username,
temp: false,
}),
}
}
Ok(_) => unreachable!(
"replace_one replaces at most one entry so all cases are covered already"
),
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
}
}
},
}
}