Skip to content

Commit d918b58

Browse files
aadityanaikaadityanaik
authored
Merge pull request #5 from PL-ML/clang-fe
Clang fe
2 parents 5d2486b + b5bbcd0 commit d918b58

File tree

985 files changed

+65241
-69038
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

985 files changed

+65241
-69038
lines changed

‎README.md‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11

2+
This clang-fe branch uses Clang compiler as the front-end, which is still under development by [Aaditya Naik](https://github.com/aadityanaik).
23

34
# Environment Setup
45

@@ -12,13 +13,13 @@
1213
## Z3 Setup
1314
code2inv uses the Z3 theorem prover to verify the correctness of generated loop invariants. Follow these steps to build Z3:
1415

15-
1. Download and unzip the source code of Z3 from https://github.com/Z3Prover/z3/releases/tag/z3-4.4.0
16+
1. Clone the source code of Z3 from https://github.com/Z3Prover/z3
1617
2. Run ```python scripts/mk_make.py --prefix /usr/local/; cd build; make -j16; make install ```
1718

1819
Remember to set environment variables DYLD_LIBRARY_PATH and PYTHONPATH to contain paths for Z3 shared libraries and Z3Py, respectively. These paths will be indicated upon successful installation of Z3.
1920

2021
## Frontend Setup (Optional)
21-
The frontend is used to extract program graphs and verification conditions (VCs) from the input C programs. The program graphs and VCs for our benchmarks are already included in the `benchmarks` directory. To build the frontend, follow the instructions in README in `code2inv-fe`.
22+
The frontend is used to extract program graphs and verification conditions (VCs) from the input C programs. The program graphs and VCs for our benchmarks are already included in the `benchmarks` directory. To build the frontend, follow the instructions in README in `clang-fe`.
2223

2324

2425
# Experiments

‎benchmarks/graph/1.c.json‎

Lines changed: 135 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -1,83 +1,136 @@
11
{
2-
"nodes": {
3-
"22": {
4-
"cmd": "Phi",
5-
"lval": { "Var": "y_22" },
6-
"rval": {
7-
"OP": "phi_merge",
8-
"arg0": { "Var": "y_14" },
9-
"arg1": { "Var": "y_16" }
10-
}
11-
},
12-
"21": {
13-
"cmd": "Phi",
14-
"lval": { "Var": "x_21" },
15-
"rval": {
16-
"OP": "phi_merge",
17-
"arg0": { "Var": "x_13" },
18-
"arg1": { "Var": "x_15" }
19-
}
20-
},
21-
"17": {
22-
"cmd": "Assert",
23-
"rval": {
24-
"OP": ">=",
25-
"arg1": { "Var": "x_21" },
26-
"arg2": { "Var": "y_22" }
27-
}
28-
},
29-
"16": {
30-
"cmd": "assign",
31-
"lval": { "Var": "y_16" },
32-
"rval": {
33-
"OP": "+",
34-
"arg1": { "Var": "y_22" },
35-
"arg2": { "Const": "1" }
36-
}
37-
},
38-
"15": {
39-
"cmd": "assign",
40-
"lval": { "Var": "x_15" },
41-
"rval": {
42-
"OP": "+",
43-
"arg1": { "Var": "x_21" },
44-
"arg2": { "Var": "y_22" }
45-
}
46-
},
47-
"14": {
48-
"cmd": "assign",
49-
"lval": { "Var": "y_14" },
50-
"rval": { "Const": "0" }
51-
},
52-
"13": {
53-
"cmd": "assign",
54-
"lval": { "Var": "x_13" },
55-
"rval": { "Const": "1" }
56-
},
57-
"12": { "cmd": "TrueBranch" },
58-
"11": { "cmd": "FalseBranch" },
59-
"4": {
60-
"cmd": "if",
61-
"rval": {
62-
"OP": "<",
63-
"arg1": { "Var": "y_22" },
64-
"arg2": { "Const": "100000" }
65-
}
66-
},
67-
"2": { "cmd": "Loop" },
68-
"ENTRY": { "cmd": "SKIP" }
69-
},
70-
"control-flow": [
71-
[ "12", "16" ],
72-
[ "12", "15" ],
73-
[ "11", "17" ],
74-
[ "4", "12" ],
75-
[ "4", "11" ],
76-
[ "2", "22" ],
77-
[ "2", "21" ],
78-
[ "2", "4" ],
79-
[ "ENTRY", "14" ],
80-
[ "ENTRY", "13" ],
81-
[ "ENTRY", "2" ]
82-
]
83-
}
2+
"nodes": {
3+
"5_1": {
4+
"cmd": "assign",
5+
"lval": {
6+
"Var": "x_1"
7+
},
8+
"rval": {
9+
"Const": "1"
10+
}
11+
},
12+
"4_2": {
13+
"cmd": "Phi",
14+
"lval": {
15+
"Var": "x_2"
16+
},
17+
"rval": {
18+
"OP": "phi_merge",
19+
"arg0": {
20+
"Var": "x_1"
21+
},
22+
"arg1": {
23+
"Var": "x_3"
24+
}
25+
}
26+
},
27+
"4_3": {
28+
"cmd": "Phi",
29+
"lval": {
30+
"Var": "y_2"
31+
},
32+
"rval": {
33+
"OP": "phi_merge",
34+
"arg0": {
35+
"Var": "y_1"
36+
},
37+
"arg1": {
38+
"Var": "y_3"
39+
}
40+
}
41+
},
42+
"4_5": {
43+
"cmd": "TrueBranch"
44+
},
45+
"4_6": {
46+
"cmd": "FalseBranch"
47+
},
48+
"1_1": {
49+
"cmd": "Assert",
50+
"rval": {
51+
"OP": ">=",
52+
"arg0": {
53+
"Var": "x_2"
54+
},
55+
"arg1": {
56+
"Var": "y_2"
57+
}
58+
}
59+
},
60+
"4_4": {
61+
"cmd": "if",
62+
"rval": {
63+
"OP": "<",
64+
"arg0": {
65+
"Var": "y_2"
66+
},
67+
"arg1": {
68+
"Const": "100000"
69+
}
70+
}
71+
},
72+
"EXIT": {
73+
"cmd": "SKIP"
74+
},
75+
"3_1": {
76+
"cmd": "assign",
77+
"lval": {
78+
"Var": "x_3"
79+
},
80+
"rval": {
81+
"OP": "+",
82+
"arg0": {
83+
"Var": "x_2"
84+
},
85+
"arg1": {
86+
"Var": "y_2"
87+
}
88+
}
89+
},
90+
"3_2": {
91+
"cmd": "assign",
92+
"lval": {
93+
"Var": "y_3"
94+
},
95+
"rval": {
96+
"OP": "+",
97+
"arg0": {
98+
"Var": "y_2"
99+
},
100+
"arg1": {
101+
"Const": "1"
102+
}
103+
}
104+
},
105+
"ENTRY": {
106+
"cmd": "SKIP"
107+
},
108+
"5_2": {
109+
"cmd": "assign",
110+
"lval": {
111+
"Var": "y_1"
112+
},
113+
"rval": {
114+
"Const": "0"
115+
}
116+
},
117+
"4_1": {
118+
"cmd": "Loop"
119+
}
120+
},
121+
"control-flow": [
122+
[ "1_1", "EXIT" ],
123+
[ "3_1", "3_2" ],
124+
[ "3_2", "4_1" ],
125+
[ "4_1", "4_2" ],
126+
[ "4_2", "4_3" ],
127+
[ "4_3", "4_4" ],
128+
[ "4_4", "4_5" ],
129+
[ "4_4", "4_6" ],
130+
[ "4_5", "3_1" ],
131+
[ "4_6", "1_1" ],
132+
[ "5_1", "5_2" ],
133+
[ "5_2", "4_1" ],
134+
[ "ENTRY", "5_1" ]
135+
]
136+
}

0 commit comments

Comments
 (0)