Skip to content

Commit 19b45e2

Browse files
rafaelsamenezesrafaelsamenezes
committed
added support for function parameters
1 parent 3de1141 commit 19b45e2

File tree

9 files changed

+206
-24
lines changed

9 files changed

+206
-24
lines changed

‎.dir-locals.el

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
((nil . ((eval . (progn
2+
;; Load the configuration script
3+
(load-file "goto-transcoder-mode.el")
4+
;; Enable the `goto-transcoder` minor mode
5+
(goto-transcoder-mode 1))))))

‎resources/test/first-steps-pass.goto

410 KB
Binary file not shown.

‎resources/test/first-steps-pass.rs

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// Taken from Kani Book
2+
3+
fn estimate_size(x: u32) -> u32 {
4+
if x < 256 {
5+
if x < 128 {
6+
return 1;
7+
} else {
8+
return 3;
9+
}
10+
} else if x < 1024 {
11+
if x > 1022 {
12+
panic!("Oh no, a failing corner case!");
13+
} else {
14+
return 5;
15+
}
16+
} else {
17+
if x < 2048 {
18+
return 7;
19+
} else {
20+
return 9;
21+
}
22+
}
23+
}
24+
25+
#[cfg(kani)]
26+
#[kani::proof]
27+
fn check_estimate_size() {
28+
let x: u32 = 42;
29+
estimate_size(x);
30+
}

‎resources/test/first-steps.rs

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// Taken from Kani Book
2+
3+
fn estimate_size(x: u32) -> u32 {
4+
if x < 256 {
5+
if x < 128 {
6+
return 1;
7+
} else {
8+
return 3;
9+
}
10+
} else if x < 1024 {
11+
if x > 1022 {
12+
panic!("Oh no, a failing corner case!");
13+
} else {
14+
return 5;
15+
}
16+
} else {
17+
if x < 2048 {
18+
return 7;
19+
} else {
20+
return 9;
21+
}
22+
}
23+
}
24+
25+
#[cfg(kani)]
26+
#[kani::proof]
27+
fn check_estimate_size() {
28+
let x: u32 = kani::any();
29+
estimate_size(x);
30+
}

‎resources/test/first_steps.rs.goto

407 KB
Binary file not shown.

‎resources/test/hello_func_parameter.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int id_foo(int i) {
4+
assert(i > 24);
5+
return i;
6+
}
7+
8+
int main() {
9+
id_foo(30);
10+
int a = 42;
11+
assert(a == id_foo(a));
12+
return 0;
13+
}

‎resources/test/hello_func_parameter_fail.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
3+
int id_foo(int i) {
4+
assert(i > 24);
5+
return i;
6+
}
7+
8+
int main() {
9+
id_foo(30);
10+
int a = 42;
11+
assert(a != id_foo(a));
12+
return 0;
13+
}

‎src/adapter.rs

Lines changed: 67 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,7 @@ mod esbmcfixes {
143143
"dereference",
144144
"bitand",
145145
"struct",
146+
"return",
146147
]
147148
.map(|x| x.to_string()),
148149
);
@@ -155,7 +156,9 @@ mod esbmcfixes {
155156
&& irep.named_subt["type"].id == "array"
156157
&& irep.subt.len() != 0;
157158

158-
if expressions.contains(&irep.id) || array_has_operand {
159+
let is_function_call = irep.id == "arguments" && irep.subt.len() != 0;
160+
161+
if expressions.contains(&irep.id) || array_has_operand || is_function_call {
159162
let mut operands = Irept::default();
160163
operands.subt = irep.subt.clone();
161164
irep.named_subt.insert("operands".to_string(), operands);
@@ -278,6 +281,42 @@ impl IrepAdapter for CBMCSymbol {
278281
.insert("is_type".to_string(), Irept::from("1"));
279282
}
280283

284+
if self.is_macro {
285+
result
286+
.named_subt
287+
.insert("is_macro".to_string(), Irept::from("1"));
288+
}
289+
290+
if self.is_parameter {
291+
result
292+
.named_subt
293+
.insert("is_parameter".to_string(), Irept::from("1"));
294+
}
295+
296+
if self.is_lvalue {
297+
result
298+
.named_subt
299+
.insert("lvalue".to_string(), Irept::from("1"));
300+
}
301+
302+
if self.is_static_lifetime {
303+
result
304+
.named_subt
305+
.insert("static_lifetime".to_string(), Irept::from("1"));
306+
}
307+
308+
if self.is_file_local {
309+
result
310+
.named_subt
311+
.insert("file_local".to_string(), Irept::from("1"));
312+
}
313+
314+
if self.is_extern {
315+
result
316+
.named_subt
317+
.insert("is_extern".to_string(), Irept::from("1"));
318+
}
319+
281320
result
282321
.named_subt
283322
.insert("base_name".to_string(), Irept::from(basename));
@@ -543,6 +582,13 @@ impl Irept {
543582
return;
544583
}
545584

585+
if self.id == "code" && self.named_subt.contains_key("parameters") {
586+
let subt = self.named_subt["parameters"].subt.clone();
587+
let mut arguments = Irept::from("arguments");
588+
arguments.subt = subt;
589+
self.named_subt.insert("arguments".to_string(), arguments);
590+
}
591+
546592
if self.named_subt.contains_key("components") {
547593
for v in &mut self.named_subt.get_mut("components").unwrap().subt {
548594
v.fix_struct();
@@ -792,6 +838,8 @@ mod tests {
792838
run_test("hello_func.c", &["--goto-functions-only"], 0);
793839
run_test("hello_func.c", &["--incremental-bmc"], 0);
794840
run_test("hello_func_fail.c", &["--incremental-bmc"], 1);
841+
run_test("hello_func_parameter.c", &["--incremental-bmc"], 0);
842+
run_test("hello_func_parameter_fail.c", &["--incremental-bmc"], 1);
795843
}
796844
#[test]
797845
#[ignore]
@@ -821,13 +869,27 @@ mod tests {
821869

822870
#[test]
823871
#[ignore]
824-
fn from_rust() {
825-
// These are example taken from the Kani first steps and then translated into C
872+
fn goto_test() {
873+
run_goto_test("mul.goto", &["--goto-functions-only"], 0);
826874
}
827875

876+
////////////////
877+
// KANI TESTS //
878+
////////////////
879+
// TODO: Integrate Kani into the test framework
880+
828881
#[test]
829882
#[ignore]
830-
fn goto_test() {
831-
run_goto_test("mul.goto", &["--goto-functions-only"], 0);
883+
fn hello_rust_book() {
884+
run_goto_test("hello_world.rs.goto", &["--goto-functions-only"], 0);
885+
run_goto_test("hello_world.rs.goto", &["--incremental-bmc"], 1);
886+
}
887+
888+
#[test]
889+
#[ignore]
890+
fn first_steps_book() {
891+
run_goto_test("first_steps.rs.goto", &["--goto-functions-only"], 0);
892+
run_goto_test("first_steps.rs.goto", &["--incremental-bmc"], 1);
893+
run_goto_test("first-steps-pass.goto", &["--incremental-bmc"], 0);
832894
}
833895
}

‎src/cbmc.rs

Lines changed: 48 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,23 @@ pub struct CBMCSymbol {
2121
pub pretty_name: String,
2222
pub flags: u32,
2323
pub is_type: bool,
24+
pub is_weak: bool,
25+
pub is_property: bool,
26+
pub is_macro: bool,
27+
pub is_exported: bool,
28+
pub is_input: bool,
29+
pub is_output: bool,
30+
pub is_state_var: bool,
31+
pub is_parameter: bool,
32+
pub is_auxiliary: bool,
33+
pub binding: bool,
34+
pub is_lvalue: bool,
35+
pub is_static_lifetime: bool,
36+
pub is_thread_local: bool,
37+
pub is_file_local: bool,
38+
pub is_extern: bool,
39+
pub is_volatile: bool,
2440
}
25-
2641
impl Default for CBMCSymbol {
2742
fn default() -> Self {
2843
CBMCSymbol {
@@ -36,6 +51,22 @@ impl Default for CBMCSymbol {
3651
pretty_name: String::default(),
3752
flags: 0,
3853
is_type: false,
54+
is_weak: false,
55+
is_property: false,
56+
is_macro: false,
57+
is_exported: false,
58+
is_input: false,
59+
is_output: false,
60+
is_state_var: false,
61+
is_parameter: false,
62+
is_auxiliary: false,
63+
binding: false,
64+
is_lvalue: false,
65+
is_static_lifetime: false,
66+
is_thread_local: false,
67+
is_file_local: false,
68+
is_extern: false,
69+
is_volatile: false,
3970
}
4071
}
4172
}
@@ -110,24 +141,22 @@ pub fn process_cbmc_file(path: &str) -> CBMCParseResult {
110141
sym.flags = result.reader.read_cbmc_word();
111142

112143
sym.is_type = sym.flags & (1 << 15) != 0;
113-
114-
// sym.is_weak = (flags &(1 << 16))!=0;
115-
// sym.is_type = (flags &(1 << 15))!=0;
116-
// sym.is_property = (flags &(1 << 14))!=0;
117-
// sym.is_macro = (flags &(1 << 13))!=0;
118-
// sym.is_exported = (flags &(1 << 12))!=0;
119-
// // sym.is_input = (flags &(1 << 11))!=0;
120-
// sym.is_output = (flags &(1 << 10))!=0;
121-
// sym.is_state_var = (flags &(1 << 9))!=0;
122-
// sym.is_parameter = (flags &(1 << 8))!=0;
123-
// sym.is_auxiliary = (flags &(1 << 7))!=0;
124-
// // sym.binding = (flags &(1 << 6))!=0;
125-
// sym.is_lvalue = (flags &(1 << 5))!=0;
126-
// sym.is_static_lifetime = (flags &(1 << 4))!=0;
127-
// sym.is_thread_local = (flags &(1 << 3))!=0;
128-
// sym.is_file_local = (flags &(1 << 2))!=0;
129-
// sym.is_extern = (flags &(1 << 1))=0;
130-
// sym.is_volatile = (flags &1)!=0;
144+
sym.is_weak = sym.flags & (1 << 16) != 0;
145+
sym.is_property = sym.flags & (1 << 14) != 0;
146+
sym.is_macro = sym.flags & (1 << 13) != 0;
147+
sym.is_exported = sym.flags & (1 << 12) != 0;
148+
sym.is_input = sym.flags & (1 << 11) != 0;
149+
sym.is_output = sym.flags & (1 << 10) != 0;
150+
sym.is_state_var = sym.flags & (1 << 9) != 0;
151+
sym.is_parameter = sym.flags & (1 << 8) != 0;
152+
sym.is_auxiliary = sym.flags & (1 << 7) != 0;
153+
sym.binding = sym.flags & (1 << 6) != 0;
154+
sym.is_lvalue = sym.flags & (1 << 5) != 0;
155+
sym.is_static_lifetime = sym.flags & (1 << 4) != 0;
156+
sym.is_thread_local = sym.flags & (1 << 3) != 0;
157+
sym.is_file_local = sym.flags & (1 << 2) != 0;
158+
sym.is_extern = sym.flags & (1 << 1) != 0;
159+
sym.is_volatile = sym.flags & 1 != 0;
131160

132161
result.symbols_irep.push(sym);
133162
}

0 commit comments

Comments
 (0)