Skip to content

Commit

Permalink
Reinsert sign semantics
Browse files Browse the repository at this point in the history
  • Loading branch information
@jsalzbergedu
jsalzbergedu committed Apr 13, 2022
1 parent d62b7fd commit 3686b58
Showing 1 changed file with 13 additions and 74 deletions.
87 changes: 13 additions & 74 deletions server/src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@
use actix_web::{get, post, web, App, HttpResponse, HttpServer, Responder, http::header::HttpDate, HttpRequest};

use serde::{Serialize, Deserialize};
use z3::{Config, Context, Solver};
use std::{collections::HashMap, io::{BufWriter, Write, ErrorKind, BufReader, BufRead}, fmt::Debug, borrow::Borrow, sync::Mutex, os::unix::prelude::MetadataExt};
use std::{collections::HashMap, io::{BufWriter, Write, ErrorKind, BufReader, BufRead}, fmt::Debug, borrow::Borrow};
use mktemp::Temp;
use std::process::{ Command, Stdio };

Expand Down Expand Up @@ -46,8 +45,6 @@ fn write_tmp_file(s: &str) -> std::io::Result<i64> {
},
};
}

println!("starting python");
let cmd = Command::new("timeout")
.arg("10s")
.arg("python3")
Expand All @@ -64,14 +61,14 @@ fn write_tmp_file(s: &str) -> std::io::Result<i64> {
.map_err(|_| std::io::Error::new(ErrorKind::Other, "bad path string"))?).as_bytes()).map(|_| ()),
None => Err(std::io::Error::new(ErrorKind::Other, "No stdin")),
}?;
match cmd.stdout {
Some(stdout) => {
let mut buf = String::new();
let mut reader = BufReader::new(stdout);
reader.read_line(&mut buf)?;
let node_response : NodeResponse = serde_json::from_str(&buf)?;
Ok(node_response.node)
}
match cmd.stdout {
Some(stdout) => {
let mut buf = String::new();
let mut reader = BufReader::new(stdout);
reader.read_line(&mut buf)?;
let node_response : NodeResponse = serde_json::from_str(&buf)?;
Ok(node_response.node)
}
None => Err(std::io::Error::new(ErrorKind::Other, "No stdout")),
}
}
Expand All @@ -94,73 +91,24 @@ fn print_property_cache<T: AbstractProperty + Sized + Clone + Eq + Debug>(output
async fn analyze(body: String) -> Result<impl Responder, std::io::Error> {
let mut map = HashMap::new();
let analyze_request : AnalyzeRequest = serde_json::from_str(&body)?;
println!("Im not even getting to program analysis!");
let pgm_idt = write_tmp_file(&analyze_request.document)?;
println!("wrote temp file");
let db = DB::from_path("analysis.db")?;
println!("its in the db bb");
match Program::from_db(&db, pgm_idt) {
Ok(p) => {
let mut labels = Labels::from_program(&p);
println!("labels failing?");
match Labels::set_labelling_tree_program(&p, &mut labels) {
Err(err) => return Err(std::io::Error::new(std::io::ErrorKind::Other, err)),
_ => {},
};
println!("set labelling tree failing?");
Labels::set_collections_program(&p, &mut labels);
println!("About to request analysis!");
match analyze_request.analysis.borrow() {
"sign" => {
// let sign = SignSemantics();
// let output: HashMap<i64, PropertyCacheElement<SignProperty>> = sign.interpret_program(&p, &labels);
// print_property_cache(output, db, &mut map);
let mut predicate = match PredicateSemantics::from_db(&db, &labels) {
Ok(it) => it,
Err(err) => return Err(std::io::Error::new(std::io::ErrorKind::Other, err)),
};
let output: HashMap<i64, PropertyCacheElement<Predicate>> = predicate.interpret_program(&p, &labels);
let config = Config::new();
let context = Context::new(&config);
let solver = Solver::new(&context);
db.node.into_iter()
.filter(|node| !(node.kind.eq("empty") || node.kind.eq("sl")))
.map(|node| {let id = node.id; (node, get_by_id(&db.fileinfo, id).unwrap())})
.map(|(node, finfo)| (node, finfo.column.clone(), finfo.line.clone()))
.filter(|(node, _, _)| output.contains_key(&node.id))
.map(|(node, column, line)| {let id = node.id;
let mut result = "No Model -- Unsatisfied";
let result_string;
if output.contains_key(&id) {
let inv = &output[&id].at_property;
match inv.into_sat(&context) {
Z3Repr::Int(_) => panic!("Property may not be int"),
Z3Repr::Bool(b) => {
solver.assert(&b);
match solver.check() {
z3::SatResult::Unsat => {println!("UNSAT!: {:?}", solver)},
z3::SatResult::Unknown => {result = "No Model -- Unknown"},
z3::SatResult::Sat => {
let s = &output[&id].at_property.model();
result_string = format!("Satisfied -- {}", s);
result = &result_string;
},
};
},
Z3Repr::Array(a) => panic!("Property may not be array"),
}
}
println!("{}", result);
solver.reset();
(node, column, line, format!("{}", result))})
.for_each(|(node, column, line, property_string)| {
let mut property = Vec::new();
property.push((column, node.kind, property_string));
map.insert(line, property);
})
let sign = SignSemantics();
let output: HashMap<i64, PropertyCacheElement<SignProperty>> = sign.interpret_program(&p, &labels);
print_property_cache(output, db, &mut map);
},
"trace" => {
let mut asstnl = AssertionalSemantics();
let asstnl = AssertionalSemantics();
let output: HashMap<i64, PropertyCacheElement<SetOfEnvironments>> = asstnl.interpret_program(&p, &labels);
print_property_cache(output, db, &mut map);
},
Expand All @@ -175,15 +123,6 @@ async fn analyze(body: String) -> Result<impl Responder, std::io::Error> {
#[actix_web::main]
async fn main() -> Result<(), std::io::Error> {
println!("hello?");
let config = z3::Config::new();
let context = z3::Context::new(&config);
// unsafe {
// GLOBAL_CONTEXT = Some(Mutex::new(GlobalContext(context)));
// GLOBAL_INT_INDICES = Some(Mutex::new(HashMap::new()));
// GLOBAL_BOOL_INDICES = Some(Mutex::new(HashMap::new()));
// GLOBAL_INTS = Some(Mutex::new(Vec::new()));
// GLOBAL_BOOLS = Some(Mutex::new(Vec::new()));
// }
HttpServer::new(|| {
App::new().service(hello).service(echo).service(analyze)
}).bind(("127.0.0.1", 8000))?.run().await
Expand Down

0 comments on commit 3686b58

Please sign in to comment.