Skip to content
Snippets Groups Projects
Verified Commit 4139ab0c authored by Vincent Lafeychine's avatar Vincent Lafeychine
Browse files

chore(radium): Improve generation for FunctionCode

parent 23a32571
No related branches found
No related tags found
1 merge request!46Some refactor in Radium crate
Pipeline #101128 passed
Hide whitespace changes
Inline Side-by-side
case_studies/minivec/annotation_patch.patch
+ 12
− 12
View file @ 4139ab0c
95a96,97
96a97,98
> (* TODO fix update of lft name map here, manually added *)
> annot: CopyLftNameAnnot "plft15" "vlft23";
121a124,125
122a125,126
> (* TODO fix update of lft name map here, manually added *)
> annot: CopyLftNameAnnot "plft18" "vlft24";
1048c1052,1056
1051c1055,1059
< "ret" <-{ PtrOp } AnnotExpr (* assignment *) 0 (GetLftNamesAnnot (LftNameTreeRef "plft14" (LftNameTreeLeaf))) (&ref{ Mut, Some (RSTTyVar "T"), "vlft4" } (!{ PtrOp } ( "p" )));
---
> (* TODO: I edited the code, some of the annotations are currently wrong *)
......@@ -12,9 +12,9 @@
> "__0" <-{ PtrOp } AnnotExpr (* assignment *) 0 (GetLftNamesAnnot (LftNameTreeRef "plft14" (LftNameTreeLeaf))) (&ref{ Mut, Some (RSTTyVar "T"), "llft6" } (!{ PtrOp } ( "p" )));
> annot: ExtendLftAnnot "llft6";
> (*
1054a1063
1057a1066
> *)
1112c1121,1125
1115c1124,1128
< "__0" <-{ (use_op_alg' (((Option_els ((PtrSynType))) : syn_type))) } EnumInit (Option_els ((PtrSynType))) "Some" (RSTLitType ["Option_ty"] [RSTRef Mut "placeholder_lft" (RSTTyVar "T")]) (StructInit (Option_Some_sls ((PtrSynType))) [("0", use{ PtrOp } ("__7") : expr)]);
---
> (* TODO inserted the right lifetime manually *)
......@@ -22,33 +22,33 @@
> (* TODO manually inserted extendlft *)
> annot: ExtendLftAnnot "llft4";
> annot: ExtendLftAnnot "llft5";
1117c1130,1131
1120c1133,1134
< "__0" <-{ (use_op_alg' (((Option_els ((PtrSynType))) : syn_type))) } EnumInit (Option_els ((PtrSynType))) "None" (RSTLitType ["Option_ty"] [RSTRef Mut "placeholder_lft" (RSTTyVar "T")]) (StructInit (Option_None_sls ((PtrSynType))) []);
---
> (* TODO inserted the right lifetime manually *)
> "__0" <-{ (use_op_alg' (((Option_els ((PtrSynType))) : syn_type))) } EnumInit (Option_els ((PtrSynType))) "None" (RSTLitType ["Option_ty"] [RSTRef Mut "plft10" (RSTTyVar "T")]) (StructInit (Option_None_sls ((PtrSynType))) []);
1162c1176,1177
1165c1179,1180
< annot: StartLftAnnot "vlft4" []; (* borrow *)
---
> (* TODO: manually constrained this by "ulft_1", maybe this should just be copylftannot instead? *)
> annot: StartLftAnnot "vlft4" ["ulft_1"]; (* borrow *)
1166a1182,1183
1169a1185,1186
> (* TODO: manually added *)
> annot: ExtendLftAnnot "plft7";
1216a1234,1235
1219a1237,1238
> (* TODO manually inserted *)
> annot: CopyLftNameAnnot "plft13" "vlft16";
1225c1244,1245
1228c1247,1248
< "__0" <-{ (use_op_alg' (((Option_els ((PtrSynType))) : syn_type))) } EnumInit (Option_els ((PtrSynType))) "Some" (RSTLitType ["Option_ty"] [RSTRef Shr "placeholder_lft" (RSTTyVar "T")]) (StructInit (Option_Some_sls ((PtrSynType))) [("0", use{ PtrOp } ("__7") : expr)]);
---
> (* TODO manually inserted the right lifetime *)
> "__0" <-{ (use_op_alg' (((Option_els ((PtrSynType))) : syn_type))) } EnumInit (Option_els ((PtrSynType))) "Some" (RSTLitType ["Option_ty"] [RSTRef Shr "plft12" (RSTTyVar "T")]) (StructInit (Option_Some_sls ((PtrSynType))) [("0", use{ PtrOp } ("__7") : expr)]);
1230c1250,1251
1233c1253,1254
< "__0" <-{ (use_op_alg' (((Option_els ((PtrSynType))) : syn_type))) } EnumInit (Option_els ((PtrSynType))) "None" (RSTLitType ["Option_ty"] [RSTRef Shr "placeholder_lft" (RSTTyVar "T")]) (StructInit (Option_None_sls ((PtrSynType))) []);
---
> (* TODO manually inserted the right lifetime *)
> "__0" <-{ (use_op_alg' (((Option_els ((PtrSynType))) : syn_type))) } EnumInit (Option_els ((PtrSynType))) "None" (RSTLitType ["Option_ty"] [RSTRef Shr "vlft15" (RSTTyVar "T")]) (StructInit (Option_None_sls ((PtrSynType))) []);
1241c1262
1244c1265
< End code.
\ No newline at end of file
---
......
rr_frontend/Cargo.lock
+ 7
− 0
View file @ 4139ab0c
......@@ -395,6 +395,12 @@ dependencies = [
"hashbrown 0.14.3",
]
[[package]]
name = "indoc"
version = "2.0.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5"
[[package]]
name = "is-terminal"
version = "0.4.12"
......@@ -587,6 +593,7 @@ version = "0.1.0"
dependencies = [
"derive_more 1.0.0-beta.6",
"indent_write",
"indoc",
"log",
]
......
rr_frontend/Cargo.toml
+ 1
− 0
View file @ 4139ab0c
......@@ -24,6 +24,7 @@ datafrog = "2"
derive_more = { version = "1.0.0-beta.6", features = ["display"] }
env_logger = "0.11"
indent_write = "2"
indoc = "2"
lazy_static = "1"
log = "0.4"
path-clean = "1"
......
rr_frontend/radium/Cargo.toml
+ 1
− 0
View file @ 4139ab0c
......@@ -10,4 +10,5 @@ version.workspace = true
[dependencies]
derive_more.workspace = true
indent_write.workspace = true
indoc.workspace = true
log.workspace = true
rr_frontend/radium/src/code.rs
+ 94
− 112
View file @ 4139ab0c
......@@ -14,6 +14,7 @@ use std::{fmt, io};
use derive_more::Display;
use indent_write::indentable::Indentable;
use indent_write::io::IndentWriter;
use indoc::{formatdoc, writedoc};
use log::info;
use crate::specs::*;
......@@ -565,121 +566,10 @@ impl Binop {
}
}
/// Representation of a Caesium function's source code
pub struct FunctionCode {
name: String,
stack_layout: StackMap,
basic_blocks: BTreeMap<usize, Stmt>,
/// Coq parameters that the function is parameterized over
required_parameters: Vec<(CoqName, CoqType)>,
}
fn make_map_string(sep0: &str, sep: &str, els: &Vec<(String, String)>) -> String {
let mut out = String::with_capacity(100);
for (key, value) in els {
out.push_str(sep);
out.push_str(format!("<[{sep}\"{}\" :={}{}{}]>%E $", key, sep0, value, sep).as_str());
}
out.push_str(sep);
out.push('∅');
out
}
fn make_lft_map_string(els: &Vec<(String, String)>) -> String {
let mut out = String::with_capacity(100);
for (key, value) in els {
out.push_str(format!("named_lft_update \"{}\" {} $ ", key, value).as_str());
}
out.push('∅');
out
}
impl FunctionCode {
const INITIAL_BB: usize = 0;
#[must_use]
pub fn caesium_fmt(&self) -> String {
// format args
let format_stack_layout = |layout: &Vec<Variable>| {
let mut formatted_args: String = String::with_capacity(100);
formatted_args.push('[');
push_str_list!(formatted_args, layout, "; ", |Variable((ref name, ref st))| {
let ly = st.layout_term(&[]); //should be closed already
let indent = make_indent(2);
format!("\n{indent}(\"{name}\", {ly} : layout)")
});
formatted_args.push_str(format!("\n{}]", make_indent(1).as_str()).as_str());
formatted_args
};
let mut formatted_args = String::with_capacity(100);
formatted_args.push_str(
format!("{}f_args := {}", make_indent(1), format_stack_layout(&self.stack_layout.args).as_str())
.as_str(),
);
let mut formatted_locals = String::with_capacity(100);
formatted_locals.push_str(
format!(
"{}f_local_vars := {}",
make_indent(1),
format_stack_layout(&self.stack_layout.locals).as_str()
)
.as_str(),
);
let formatted_bb = make_map_string(
"\n",
format!("\n{}", make_indent(2).as_str()).as_str(),
&self
.basic_blocks
.iter()
.map(|(name, bb)| (format!("_bb{name}"), bb.indented(&make_indent(3)).to_string()))
.collect(),
);
if self.basic_blocks.is_empty() {
panic!("Function has no basic block");
}
let formatted_init = format!("{}f_init := \"_bb{}\"", make_indent(1).as_str(), Self::INITIAL_BB);
// format Coq parameters
let mut formatted_params = String::with_capacity(20);
for (ref name, ref ty) in &self.required_parameters {
formatted_params.push_str(format!(" ({} : {})", name, ty).as_str());
}
format!(
"Definition {}_def{} : function := {{|\n{};\n{};\n{}f_code := {};\n{};\n|}}.",
self.name.as_str(),
formatted_params.as_str(),
formatted_args.as_str(),
formatted_locals.as_str(),
make_indent(1).as_str(),
formatted_bb.as_str(),
formatted_init.as_str()
)
}
/// Get the number of arguments of the function.
#[must_use]
pub fn get_argument_count(&self) -> usize {
self.stack_layout.args.len()
}
}
/**
* A variable in the Caesium code, composed of a name and a type.
*/
#[derive(Clone, Eq, PartialEq, Debug, Display)]
#[display("(\"{}\", {} : layout)", _0.0, _0.1.layout_term(&[]))]
#[derive(Clone, Eq, PartialEq, Debug)]
struct Variable((String, SynType));
impl Variable {
......@@ -748,6 +638,98 @@ impl StackMap {
}
}
/// Representation of a Caesium function's source code
pub struct FunctionCode {
name: String,
stack_layout: StackMap,
basic_blocks: BTreeMap<usize, Stmt>,
/// Coq parameters that the function is parameterized over
required_parameters: Vec<(CoqName, CoqType)>,
}
fn make_map_string(sep0: &str, sep: &str, els: &Vec<(String, String)>) -> String {
let mut out = String::with_capacity(100);
for (key, value) in els {
out.push_str(sep);
out.push_str(format!("<[\n \"{key}\" :=\n{value}\n ]>%E $").as_str());
}
out.push_str(sep);
out.push('∅');
out
}
fn make_lft_map_string(els: &Vec<(String, String)>) -> String {
let mut out = String::with_capacity(100);
for (key, value) in els {
out.push_str(format!("named_lft_update \"{}\" {} $ ", key, value).as_str());
}
out.push('∅');
out
}
impl Display for FunctionCode {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
fn fmt_params((name, ty): &(CoqName, CoqType)) -> String {
format!("({} : {})", name, ty)
}
fn fmt_variable(Variable((name, ty)): &Variable) -> String {
format!("(\"{}\", {} : layout)", name, ty.layout_term(&[]))
}
fn fmt_blocks((name, bb): (&usize, &Stmt)) -> String {
formatdoc!(
r#"<[
"_bb{}" :=
{}
]>%E $"#,
name,
bb.indented_skip_initial(&make_indent(1))
)
}
if self.basic_blocks.is_empty() {
panic!("Function has no basic block");
}
let params = display_list!(&self.required_parameters, " ", fmt_params);
let args = display_list!(&self.stack_layout.args, ";\n", fmt_variable);
let locals = display_list!(&self.stack_layout.locals, ";\n", fmt_variable);
let blocks = display_list!(&self.basic_blocks, "\n", fmt_blocks);
writedoc!(
f,
r#"Definition {}_def {} : function := {{|
f_args := [
{}
];
f_local_vars := [
{}
];
f_code :=
{}
∅;
f_init := "_bb0";
|}}."#,
self.name,
params,
args.indented_skip_initial(&make_indent(2)),
locals.indented_skip_initial(&make_indent(2)),
blocks.indented_skip_initial(&make_indent(2))
)
}
}
impl FunctionCode {
/// Get the number of arguments of the function.
#[must_use]
pub fn get_argument_count(&self) -> usize {
self.stack_layout.args.len()
}
}
/// Builder for a `FunctionCode`.
pub struct FunctionCodeBuilder {
stack_layout: StackMap,
......
rr_frontend/translation/src/lib.rs
+ 1
− 1
View file @ 4139ab0c
......@@ -433,7 +433,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
.unwrap();
for (_, fun) in self.procedure_registry.iter_code() {
code_file.write(fun.code.caesium_fmt().as_bytes()).unwrap();
code_file.write(fun.code.to_string().as_bytes()).unwrap();
code_file.write("\n\n".as_bytes()).unwrap();
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment