~ubuntu-branches/debian/sid/frama-c/sid

(** Given a transition a function name and a function status (call or return) it returns if the cross condition can be statisfied with only function status. *)

let isCrossable tr func st =

let rec isCross p =

match p with

| POr (c1, c2) -> bool3or (isCross c1) (isCross c2)

| PAnd (c1, c2) -> bool3and (isCross c1) (isCross c2)

| PNot (c1) -> bool3not (isCross c1)

| PCall (s) -> if func=s && st=Call then True else False

| PReturn (s) -> if func=s && st=Return then True else False

| PCallOrReturn (s) -> if func=s then True else False

| PTrue -> True

| PFalse -> False

(* | PGt (_,_)

| PGe (_,_)

| PLt (_,_)

| PLe (_,_)

| PEq (_,_)

| PNeq (_,_)

| PBoolVar (_) -> Undefined*)

| PIndexedExp (_) -> Undefined

(isCross tr.cross)<>False

(* ************************************************************************* *)

let debug_display_stmt_pre (pre,_)=

let r=ref "{" in

Array.iteri

(fun i s ->

if s then

begin

Format.printf "%s%s" !r (string_of_int i);

r:=","

end

)

pre;

if !r="{" then

Format.printf "{}"

else

Format.printf "}"

let debug_display_spec (pre_st,pre_tr,post_st,post_tr) name=

debug_display_stmt_pre(pre_st,pre_tr);

Format.printf " %s " name;

debug_display_stmt_pre(post_st,post_tr);

Format.printf "\n"

let debug_display_stmt_all_pre (st,tr)=

Format.printf "st=";

debug_display_stmt_pre(st,tr);

Format.printf " tr=";

debug_display_stmt_pre(tr,st)

let debug_display_func_status name =

let pre = Data_for_ltl.get_func_pre name in

let post = Data_for_ltl.get_func_post name in

100

debug_display_stmt_all_pre pre;

101

Format.printf " %s " name;

102

debug_display_stmt_all_pre post;

103

Format.printf "\n"

104

105

106

107

108

(* ************************************************************************* *)

109

110

let mk_empty_pre_or_post () =

111

(Array.make (Data_for_ltl.getNumberOfStates()) false,

112

Array.make (Data_for_ltl.getNumberOfTransitions()) false)

113

114

let mk_empty_spec () =

115

(Array.make (Data_for_ltl.getNumberOfStates()) false,

116

Array.make (Data_for_ltl.getNumberOfTransitions()) false,

117

Array.make (Data_for_ltl.getNumberOfStates()) false,

118

Array.make (Data_for_ltl.getNumberOfTransitions()) false

119

)

120

121

122

123

124

(** Given a function name, is status (call or return) and an array of boolean describing states status, it returns a couple of boolean array. The first one describes the set of reachable states and the second one is the set of crossable transitions. *)

125

let get_next func status states =

126

let st,tr = mk_empty_pre_or_post () in

127

let (_,trans_l) = Data_for_ltl.getAutomata() in

128

List.iter

129

(fun t ->

130

if (states.(t.start.nums)) && (isCrossable t func status) then

131

begin

132

st.(t.stop.nums)<- true ;

133

tr.(t.numt)<- true

134

end

135

)

136

trans_l;

137

(st,tr)

138

139

140

141

(** Given a function name, is status (call or return) and an array of boolean describing states status, it returns a couple of boolean array. The first one describes the set of possible initial states and the second one is the set of crossable transitions. *)

142

let get_prev func status (states,trans) =

143

let st,tr = mk_empty_pre_or_post () in

144

let (_,trans_l) = Data_for_ltl.getAutomata() in

145

List.iter

146

(fun t ->

147

if (states.(t.stop.nums)) && (isCrossable t func status) && trans.(t.numt) then

148

st.(t.start.nums)<- true

149

)

150

trans_l;

151

List.iter

152

(fun t ->

153

if (st.(t.stop.nums)) (*&& (isCrossable t func status) <- We do'nt have the action of prev transitions *) then

154

tr.(t.numt)<- true

155

)

156

trans_l;

157

(st,tr)

158

159

160

161

162

(** Given two bool arrays with the same length, it returns a fresh bool array corresponding to a logical OR between cells with same index from the two arrays. *)

163

let bool_array_and arr1 arr2 =

164

if Array.length arr1 <> Array.length arr2 then

165

assert false;

166

let res=Array.make (Array.length arr1) false in

167

Array.iteri

168

(fun i b1 -> if b1 && arr2.(i) then res.(i)<-true)

169

arr1;

170

res

171

172

173

(** Given two bool arrays with the same length, it returns a fresh bool array corresponding to a logical AND between cells with same index from the two arrays. *)

174

let bool_array_or arr1 arr2 =

175

if Array.length arr1 <> Array.length arr2 then

176

assert false;

177

let res=Array.make (Array.length arr1) false in

178

Array.iteri

179

(fun i b1 -> if b1 || arr2.(i) then res.(i)<-true)

180

arr1;

181

res

182

183

184

(** Given two bool arrays with the same length, it returns true if and only if their cells are equal for each index. *)

185

let bool_array_eq arr1 arr2 =

186

if Array.length arr1 <> Array.length arr2 then

187

assert false;

188

let res=ref true in

189

Array.iteri

190

(fun i b1 -> if b1 <> arr2.(i) then res:=false)

191

arr1;

192

!res

193

194

195

196

197

let double_bool_array_and (a1,a2) (b1,b2) =

198

(bool_array_and a1 b1,

199

bool_array_and a2 b2)

200

201

let quad_bool_array_and (a1,a2,a3,a4) (b1,b2,b3,b4) =

202

(bool_array_and a1 b1,

203

bool_array_and a2 b2,

204

bool_array_and a3 b3,

205

bool_array_and a4 b4)

206

207

let double_bool_array_or (a1,a2) (b1,b2) =

208

(bool_array_or a1 b1,

209

bool_array_or a2 b2)

210

let quad_bool_array_or (a1,a2,a3,a4) (b1,b2,b3,b4) =

211

(bool_array_or a1 b1,

212

bool_array_or a2 b2,

213

bool_array_or a3 b3,

214

bool_array_or a4 b4)

215

216

217

let double_bool_array_eq (a1,a2) (b1,b2) =

218

(bool_array_eq a1 b1) &&

219

(bool_array_eq a2 b2)

220

221

let quad_bool_array_eq (a1,a2,a3,a4) (b1,b2,b3,b4) =

222

(bool_array_eq a1 b1) &&

223

(bool_array_eq a2 b2) &&

224

(bool_array_eq a3 b3) &&

225

(bool_array_eq a4 b4)

226

227

228

229

230

231

232

233

234

(* ************************************************************************* *)

235

236

237

type pre_post_bycase_t = bool array array

238

type double_pre_post_bycase_t = (pre_post_bycase_t*pre_post_bycase_t)

239

type quad_pre_post_bycase_t = (pre_post_bycase_t*pre_post_bycase_t*pre_post_bycase_t*pre_post_bycase_t)

240

241

242

(* ************************************************************************* *)

243

244

245

let mk_empty_pre_or_post_bycase () =

246

(Array.make_matrix (Data_for_ltl.getNumberOfStates()) (Data_for_ltl.getNumberOfStates()) false,

247

Array.make_matrix (Data_for_ltl.getNumberOfStates()) (Data_for_ltl.getNumberOfTransitions()) false)

248

249

let mk_empty_spec_bycase () =

250

(Array.make_matrix (Data_for_ltl.getNumberOfStates()) (Data_for_ltl.getNumberOfStates()) false,

251

Array.make_matrix (Data_for_ltl.getNumberOfStates()) (Data_for_ltl.getNumberOfTransitions()) false,

252

Array.make_matrix (Data_for_ltl.getNumberOfStates()) (Data_for_ltl.getNumberOfStates()) false,

253

Array.make_matrix (Data_for_ltl.getNumberOfStates()) (Data_for_ltl.getNumberOfTransitions()) false

254

)

255

256

257

let mk_pre_or_post_bycase_from_pre_or_post (st,tr) =

258

let st_bc,tr_bc = mk_empty_pre_or_post_bycase () in

259

let (_,trans_l) = Data_for_ltl.getAutomata() in

260

Array.iteri

261

(fun index t -> if st.(index) then t.(index)<-true)

262

st_bc;

263

264

List.iter

265

(fun t -> if tr.(t.numt) then tr_bc.(t.stop.nums).(t.numt)<-true)

266

trans_l;

267

268

(st_bc,tr_bc)

269

270

271

272

let pre_flattening (pre_st,pre_tr) =

273

let new_st,new_tr = mk_empty_pre_or_post () in

274

let new_st,new_tr = ref new_st, ref new_tr in

275

Array.iteri

276

(fun index assocs ->

277

new_st:=bool_array_or assocs !new_st ;

278

new_tr:=bool_array_or pre_tr.(index) !new_tr

279

)

280

pre_st;

281

(!new_st,!new_tr)

282

283

284

let post_pseudo_flattening post =

285

let new_st,new_tr = mk_empty_pre_or_post_bycase () in

286

Array.iteri

287

(fun index _ ->

288

let flat_st,flat_tr=pre_flattening post in

289

new_st.(index) <- flat_st;

290

new_tr.(index) <- flat_tr

291

)

292

new_st;

293

(new_st,new_tr)

294

295

(* ************************************************************************* *)

296

297

let is_empty_behavior assocs =

298

Array.fold_left (fun b c -> if c then false else b) true assocs

299

300

let assocs_to_string assocs =

301

let r=ref "(" in

302

let s=ref "" in

303

Array.iteri

304

(fun i b ->

305

if b then

306

begin

307

s:=(!s)^(!r)^(string_of_int i);

308

r:=","

309

end

310

)

311

assocs;

312

!s^")"

313

314

315

316

let debug_display_stmt_pre_bycase (pre,_)=

317

let r=ref "{" in

318

Array.iteri

319

(fun i assocs ->

320

if not (is_empty_behavior assocs) then

321

begin

322

Format.printf "%s%s->%s" !r (string_of_int i) (assocs_to_string assocs) ;

323

r:=","

324

end

325

)

326

pre;

327

if !r="{" then

328

Format.printf "{}"

329

else

330

Format.printf "}"

331

332

333

334

let debug_display_spec_bycase (pre_st,pre_tr,post_st,post_tr) name=

335

debug_display_stmt_pre_bycase(pre_st,pre_tr);

336

Format.printf " %s " name;

337

debug_display_stmt_pre_bycase(post_st,post_tr);

338

Format.printf "\n"

339

340

341

342

let debug_display_stmt_all_pre_bycase (st,tr)=

343

Format.printf "st=";

344

debug_display_stmt_pre_bycase(st,tr);

345

Format.printf " tr=";

346

debug_display_stmt_pre_bycase(tr,st)

347

348

349

350

351

352

let debug_display_func_status_bycase name =

353

let pre = Data_for_ltl.get_func_pre name in

354

let pre = mk_pre_or_post_bycase_from_pre_or_post pre in

355

let post = Data_for_ltl.get_func_post_bycase name in

356

357

debug_display_stmt_all_pre_bycase pre;

358

Format.printf " %s " name;

359

debug_display_stmt_all_pre_bycase post;

360

Format.printf "\n"

361

362

363

364

365

(* ************************************************************************* *)

366

367

368

(** bool array -> (bool array array*bool array array) -> (bool array*bool array) *)

369

let compose_assocs_post assocs_st (post_st,post_tr) =

370

let st,tr = mk_empty_pre_or_post () in

371

let st,tr = ref st, ref tr in

372

Array.iteri

373

(fun index b ->

374

if b then begin

375

st:=bool_array_or post_st.(index) !st;

376

tr:=bool_array_or post_tr.(index) !tr

377

end

378

)

379

assocs_st;

380

381

(!st,!tr)

382

383

384

(** bool array array -> (bool array array*bool array array) -> (bool array array*bool array array)

385

Given a set of states and the bycase post-condition of an operation

386

this function returns the new pre-condition after the call of the operation in the context of current_st.

387

388

let mk_forward_composition current_st post =

389

let new_st,new_tr = mk_empty_pre_or_post_bycase () in

390

Array.iteri

391

(fun index assocs ->

392

let s,t = compose_assocs_post assocs post in

393

new_st.(index)<-s;

394

new_tr.(index)<-t

395

)

396

current_st;

397

398

(new_st,new_tr)

399

400

401

402

(** bool array -> (bool array * bool array) (bool array array*bool array array) -> (bool array*bool array) *)

403

let compose_assocs_pre assocs_st (_,pre_tr) (post_st,_) =

404

let st,tr = mk_empty_pre_or_post () in

405

let st,tr = ref st, ref tr in

406

let (_,trans_l) = Data_for_ltl.getAutomata() in

407

Array.iteri

408

(fun index b ->

409

if b then begin

410

Array.iteri

411

(fun value val_assocs -> if val_assocs.(index) then !st.(value)<-true)

412

post_st;

413

end

414

)

415

assocs_st;

416

417

418

List.iter

419

(fun t -> if pre_tr.(t.numt) && (!st).(t.stop.nums) then !tr.(t.numt)<-true)

420

trans_l;

421

422

423

(!st,!tr)

424

425

426

(** bool array array -> (bool array*bool array) -> (bool array array*bool array array) -> (bool array array*bool array array)

427

Given a set of states and the bycase post-condition of an operation

428

this function returns the new pre-condition after the call of the operation in the context of current_st.

429

430

let mk_backward_composition current_st pre post =

431

let new_st,new_tr = mk_empty_pre_or_post_bycase () in

432

Array.iteri

433

(fun index assocs ->

434

let s,t = compose_assocs_pre assocs pre post in

435

new_st.(index)<-s;

436

new_tr.(index)<-t

437

)

438

current_st;

439

440

(new_st,new_tr)

441

442

443

444

445

446

447

let get_next_bycase func status states_bycase =

448

(* In a first pass we compute all cases of specification (For each starting state, we compute ending states set) *)

449

let st_bc,tr_bc = mk_empty_pre_or_post_bycase () in

450

let (_,trans_l) = Data_for_ltl.getAutomata() in

451

List.iter

452

(fun t ->

453

if (isCrossable t func status) then

454

begin

455

st_bc.(t.start.nums).(t.stop.nums)<- true ;

456

tr_bc.(t.start.nums).(t.numt)<- true

457

end

458

)

459

trans_l;

460

461

(* In second pass we replace each ending state from states_bycase by the new computed one *)

462

let res_st_bc,res_tr_bc = mk_empty_pre_or_post_bycase () in

463

Array.iteri

464

(fun init_st init_st_assocs ->

465

Array.iteri

466

(fun end_st b ->

467

if b then

468

begin

469

res_st_bc.(init_st) <- (bool_array_or (res_st_bc.(init_st)) (st_bc.(end_st)) );

470

res_tr_bc.(init_st) <- (bool_array_or (res_tr_bc.(init_st)) (tr_bc.(end_st)) );

471

end

472

)

473

init_st_assocs;

474

)

475

states_bycase;

476

477

(res_st_bc,res_tr_bc)

478

479

480

481

482

483

484

let get_prev_bycase func status (states_bycase ,transitions_bycase) =

485

let res_st_bc,res_tr_bc = mk_empty_pre_or_post_bycase () in

486

(* For each starting case, we call the get_prev function *)

487

Array.iteri

488

(fun case_st case_st_assocs ->

489

let prev_st,prev_tr= get_prev func status (case_st_assocs,transitions_bycase.(case_st)) in

490

res_st_bc.(case_st) <- prev_st;

491

res_tr_bc.(case_st) <- prev_tr

492

)

493

states_bycase;

494

495

(res_st_bc,res_tr_bc)

496

497

498

499

(** Given two bool arrays with the same length, it returns a fresh bool array corresponding to a logical OR between cells with same index from the two arrays. *)

500

let bool_array_and_bycase bc_arr1 bc_arr2 =

501

if Array.length bc_arr1 <> Array.length bc_arr2 then

502

assert false;

503

504

let res=Array.make (Array.length bc_arr1) (Array.make (Array.length bc_arr1.(0)) false) in

505

Array.iteri

506

(fun case b1 -> res.(case)<-bool_array_and b1 (bc_arr2.(case)))

507

bc_arr1;

508

res

509

510

511

512

(** Given two bool arrays with the same length, it returns a fresh bool array corresponding to a logical AND between cells with same index from the two arrays. *)

513

let bool_array_or_bycase bc_arr1 bc_arr2 =

514

if Array.length bc_arr1 <> Array.length bc_arr2 then

515

assert false;

516

517

let res=Array.make (Array.length bc_arr1) (Array.make (Array.length bc_arr1.(0)) false) in

518

Array.iteri

519

(fun case b1 -> res.(case)<-bool_array_or b1 (bc_arr2.(case)))

520

bc_arr1;

521

res

522

523

524

(** Given two bool arrays with the same length, it returns true if and only if their cells are equal for each index. *)

525

let bool_array_eq_bycase bc_arr1 bc_arr2 =

526

if Array.length bc_arr1 <> Array.length bc_arr2 then

527

assert false;

528

529

let res=ref true in

530

Array.iteri

531

(fun case b1 -> if not (bool_array_eq b1 (bc_arr2.(case))) then res :=false)

532

bc_arr1;

533

!res

534

535

536

537

538

539

540

541

let double_bool_array_and_bycase (a1,a2) (b1,b2) =

542

(bool_array_and_bycase a1 b1,

543

bool_array_and_bycase a2 b2)

544

545

let quad_bool_array_and_bycase (a1,a2,a3,a4) (b1,b2,b3,b4) =

546

(bool_array_and_bycase a1 b1,

547

bool_array_and_bycase a2 b2,

548

bool_array_and_bycase a3 b3,

549

bool_array_and_bycase a4 b4)

550

551

let double_bool_array_or_bycase (a1,a2) (b1,b2) =

552

(bool_array_or_bycase a1 b1,

553

bool_array_or_bycase a2 b2)

554

let quad_bool_array_or_bycase (a1,a2,a3,a4) (b1,b2,b3,b4) =

555

(bool_array_or_bycase a1 b1,

556

bool_array_or_bycase a2 b2,

557

bool_array_or_bycase a3 b3,

558

bool_array_or_bycase a4 b4)

559

560

561

let double_bool_array_eq_bycase (a1,a2) (b1,b2) =

562

(bool_array_eq_bycase a1 b1) &&

563

(bool_array_eq_bycase a2 b2)

564

565

let quad_bool_array_eq_bycase (a1,a2,a3,a4) (b1,b2,b3,b4) =

566

(bool_array_eq_bycase a1 b1) &&

567

(bool_array_eq_bycase a2 b2) &&

568

(bool_array_eq_bycase a3 b3) &&

569

(bool_array_eq_bycase a4 b4)

570

571

572

573

574

575

576

577

578

579

580

581

582

583

584

(* ************************************************************************* *)

585

586

587

588

(*open Cil_types*)

589

590

(** Given a transition a function name and a function status (call or return) it returns if the cross condition can be statisfied with only function status. *)

591

let isCrossableAtInit tr func =

592

let rec isCross = function

593

| POr (c1, c2) ->

594

if not (isCross c1) then (isCross c2) else false

595

| PAnd (c1, c2) ->

596

if (isCross c1) then (isCross c2) else false

597

| PNot (c1) ->

598

not (isCross c1)

599

600

| PCall (s) ->

601

(func=s)

602

| PReturn (_) ->

603

false

604

| PCallOrReturn (s) ->

605

func=s

606

607

| PTrue ->

608

true

609

| PFalse ->

610

false

611

(* | PGt (_,_)

612

| PGe (_,_)

613

| PLt (_,_)

614

| PLe (_,_)

615

| PEq (_,_)

616

| PNeq (_,_)

617

| PBoolVar (_) -> Undefined*)

618

619

| PIndexedExp (e) ->

620

(evalExpAtInit (Data_for_ltl.get_exp_from_tmpident e))<>0

621

622

623

624

and error_msg msg =

625

Format.printf "Ltl_to_acsl plugin internal error. Status : %s. \n" msg;

626

assert false

627

628

and evalExpAtInit:Cil_types.exp -> int = function

629

| Cil_types.Const (c) ->

630

begin

631

match c with

632

| Cil_types.CInt64(int64,_,_) -> Int64.to_int int64

633

| Cil_types.CStr (_)

634

| Cil_types.CWStr(_) -> error_msg "String values not supported into LTL expressions"

635

| Cil_types.CChr(c) -> Char.code c

636

| Cil_types.CReal (_,_,_) -> error_msg "Real values not supported into LTL expressions"

637

| Cil_types.CEnum {eival = exp} -> evalExpAtInit exp

638

end

639

640

641

| Cil_types.Lval (Cil_types.Var(vi),Cil_types.NoOffset) -> get_val_from_vi vi

642

| Cil_types.Lval (_) ->

643

error_msg "Only simple LVAL supported at this time into LTL expressions"

644

645

| Cil_types.UnOp (unop,exp,typ) ->

646

if not (Cil.isIntegralType typ) then

647

error_msg "Such operator not yet supported in LTL expressions"

648

else

649

begin

650

match unop with

651

| Cil_types.Neg -> (-(evalExpAtInit exp))

652

| Cil_types.BNot -> error_msg "Bitwise complement not supported in LTL expressions"

653

| Cil_types.LNot -> if (evalExpAtInit exp)=0 then 1 else 0

654

end

655

656

| Cil_types.BinOp (binop,exp1,exp2,typ) ->

657

if not (Cil.isIntegralType typ) then

658

error_msg "Such operator not yet supported in LTL expressions"

659

else

660

begin

661

match binop with

662

| Cil_types.PlusA -> (evalExpAtInit exp1) + (evalExpAtInit exp2)

663

| Cil_types.MinusA -> (evalExpAtInit exp1) - (evalExpAtInit exp2)

664

| Cil_types.Mult -> (evalExpAtInit exp1) * (evalExpAtInit exp2)

665

| Cil_types.Div -> (evalExpAtInit exp1) / (evalExpAtInit exp2)

666

| Cil_types.Mod -> error_msg "Modulo not yet supported in LTL expressions"

667

| Cil_types.PlusPI

668

| Cil_types.IndexPI

669

| Cil_types.MinusPI

670

| Cil_types.MinusPP -> error_msg "Pointer and array not yet supported in LTL expressions"

671

| Cil_types.Shiftlt

672

| Cil_types.Shiftrt -> error_msg "Shifts not yet supported in LTL expressions"

673

| Cil_types.Lt -> if (evalExpAtInit exp1) < (evalExpAtInit exp2) then 1 else 0

674

| Cil_types.Gt -> if (evalExpAtInit exp1) > (evalExpAtInit exp2) then 1 else 0

675

| Cil_types.Le -> if (evalExpAtInit exp1) <= (evalExpAtInit exp2) then 1 else 0

676

| Cil_types.Ge -> if (evalExpAtInit exp1) >= (evalExpAtInit exp2) then 1 else 0

677

| Cil_types.Eq -> if (evalExpAtInit exp1) = (evalExpAtInit exp2) then 1 else 0

678

| Cil_types.Ne -> if (evalExpAtInit exp1) <> (evalExpAtInit exp2) then 1 else 0

679

| Cil_types.BAnd

680

| Cil_types.BXor

681

| Cil_types.BOr -> error_msg "Bitwise operations not supported in LTL expressions"

682

| Cil_types.LAnd -> if (evalExpAtInit exp1)<>0 && (evalExpAtInit exp2)<>0 then 1 else 0

683

| Cil_types.LOr -> if (evalExpAtInit exp1)<>0 or (evalExpAtInit exp2)<>0 then 1 else 0

684

end

685

686

687

688

| Cil_types.Info (exp,_) ->

689

evalExpAtInit exp

690

691

| Cil_types.CastE (_,exp) ->

692

Format.printf "Warning (Ltl_to_acsl plugin) CastE is not yet fully supported as a valid LTL expression. \n" ;

693

evalExpAtInit exp

694

695

696

697

| Cil_types.SizeOf (_)

698

| Cil_types.SizeOfE (_)

699

| Cil_types.SizeOfStr (_) ->

700

error_msg "Sizeof is not supported as a valid LTL expression"

701

702

| Cil_types.AlignOf (_)

703

| Cil_types.AlignOfE (_) ->

704

error_msg "AlignOf is not supported as a valid LTL expression"

705

706

| Cil_types.AddrOf (_) ->

707

error_msg "AddrOf is not yet supported as a valid LTL expression"

708

| Cil_types.StartOf(_) ->

709

error_msg "StartOf is not yet supported as a valid LTL expression"

710

711

712

and get_val_from_vi vi =

713

try

714

let ini=Globals.Vars.find vi in

715

match ini.Cil_types.init with

716

| None -> error_msg ("'"^(vi.Cil_types.vname)^"'Seems to not be initialized" )

717

| Some (Cil_types.SingleInit(exp)) -> evalExpAtInit exp

718

| Some (Cil_types.CompoundInit(_,_)) -> error_msg "Compound values not yet supported into LTL expressions"

719

with

720

| _ ->

721

error_msg ("initialisation of '"^(vi.Cil_types.vname)^"' not found")

722

723

724

725

726

isCross tr.cross

727

728

729

730

731

732

(* ************************************************************************* *)

733

(** {b Expressions management} *)

734

open Logic_const

735

open Cil_types

736

open Data_for_ltl

737

738

739

740

(** Returns an int constant expression which represents the given int value. *)

741

let mk_int_exp value =

742

Const(CInt64(Int64.of_int value,IInt,Some(string_of_int value)))

743

744

(** Returns an lval expression which represents the access of the host_name variable (a string) with the offset off_exp (an expression). *)

745

let mk_offseted_array_lval host_name off_exp =

746

let host_lval = (Cil.var (get_varinfo host_name)) in

747

Cil.addOffsetLval

748

(Index(off_exp,NoOffset))

749

host_lval

750

751

(** Returns an lval expression which represents the access of the host_name variable (a string) with the offset off_value (an int). *)

752

let mk_int_offseted_array_lval host_name off_value =

753

mk_offseted_array_lval host_name (mk_int_exp off_value)

754

755

756

757

758

(** This function rewrite a cross condition into a Cil expression.

759

Moreover, by giving current operation name and its status (call or return) the generation simplifies the generated expression. *)

760

let crosscond_to_exp cross func status =

761

(* TODO : Consider particular cases of result during return and parameters during call *)

762

let false_exp = Const(CInt64(Int64.of_int 0,IInt,Some("0"))) in

763

let true_exp = Const(CInt64(Int64.of_int 1,IInt,Some("1"))) in

764

let rec convert : Promelaast.condition -> Bool3.bool3 * Cil_types.exp = function

765

(* Lazy evaluation of logic operators if the result can be statically computed *)

766

| POr (c1, c2) -> (*BinOp(LOr,convert c1,convert c2,Cil.intType)*)

767

begin

768

let (c1_val,c1_exp) = convert c1 in

769

match c1_val with

770

| Bool3.True -> (c1_val,c1_exp)

771

| Bool3.False -> convert c2

772

| Undefined ->

773

let (c2_val,c2_exp) = convert c2 in

774

match c2_val with

775

| Bool3.True -> (c2_val,c2_exp)

776

| Bool3.False -> (c1_val,c1_exp)

777

| Undefined -> (Undefined,BinOp(LOr,c1_exp,c2_exp,Cil.intType))

778

end

779

780

| PAnd (c1, c2) -> (*BinOp(LAnd,convert c1,convert c2,Cil.intType)*)

781

begin

782

let (c1_val,c1_exp) = convert c1 in

783

match c1_val with

784

| Bool3.True -> convert c2

785

| Bool3.False -> (c1_val,c1_exp)

786

| Undefined ->

787

let (c2_val,c2_exp) = convert c2 in

788

match c2_val with

789

| Bool3.True -> (c1_val,c1_exp)

790

| Bool3.False -> (c2_val,c2_exp)

791

| Undefined -> (Undefined,BinOp(LAnd,c1_exp,c2_exp,Cil.intType))

792

end

793

794

| PNot (c1) -> (*UnOp(LNot,convert c1,Cil.intType)*)

795

begin

796

let (c1_val,c1_exp) = convert c1 in

797

match c1_val with

798

| Bool3.True -> (Bool3.False,false_exp)

799

| Bool3.False -> (Bool3.True,true_exp)

800

| Undefined -> (c1_val,UnOp(LNot,c1_exp,Cil.intType))

801

end

802

803

(* Call and return are statically defined *)

804

| PCall (s) ->

805

if(s=func) && (status=Promelaast.Call) then

806

(Bool3.True, true_exp)

807

else

808

(Bool3.False,false_exp)

809

810

811

| PReturn (s) ->

812

if(s=func) && (status=Promelaast.Return) then

813

(Bool3.True,true_exp)

814

(* snd (convert(PAnd(

815

PEq(PVar(s),PVar(curOp)),

816

PEq(PVar(callStatus),PVar(curOpStatus))

817

))))*)

818

else

819

(Bool3.False,false_exp)

820

821

822

823

| PCallOrReturn (s) ->

824

if(s=func) then

825

(Bool3.True,true_exp)

826

(* snd (convert(PEq(PVar(s),PVar(curOp)))))*)

827

else

828

(Bool3.False,false_exp)

829

830

831

832

833

(* Other expressions are left unchanged *)

834

| PTrue -> (Bool3.True, true_exp)

835

| PFalse -> (Bool3.False, false_exp)

836

837

| PIndexedExp(s) -> (Undefined,get_exp_from_tmpident s)

838

839

(* | PGt (c1,c2) -> (Undefined,BinOp(Gt,convert_arith c1,convert_arith c2,Cil.intType))

840

| PGe (c1,c2) -> (Undefined,BinOp(Ge,convert_arith c1,convert_arith c2,Cil.intType))

841

| PLt (c1,c2) -> (Undefined,BinOp(Lt,convert_arith c1,convert_arith c2,Cil.intType))

842

| PLe (c1,c2) -> (Undefined,BinOp(Le,convert_arith c1,convert_arith c2,Cil.intType))

843

| PEq (c1,c2) -> (Undefined,BinOp(Eq,convert_arith c1,convert_arith c2,Cil.intType))

844

| PNeq (c1,c2) -> (Undefined,BinOp(Ne,convert_arith c1,convert_arith c2,Cil.intType))

845

846

| PBoolVar (s) -> (Undefined,Lval(Cil.var(get_varinfo s))) *)

847

848

try

849

(*let (_,res) = *)

850

convert cross (*in

851

res*)

852

with

853

| _ ->

854

Format.printf "Ltl_to_acsl plugin internal error. Status : Not_found exception during exp conversion.\n";

855

assert false

856

857

858

859

860

861

862

863

864

865

866

867

868

869

870

871

872

873

874

875

876

877

878

879

880

881

882

883

(** This function rewrite a cross condition into a Cil expression.

884

Moreover, by giving current operation name and its status (call or return) the generation simplifies the generated expression. *)

885

let crosscond_to_pred cross op_logic_var status_logic_var =

886

(* TODO : Consider particular cases of result dureing return and parameters during call *)

887

let rec convert : Promelaast.condition -> Bool3.bool3 * Cil_types.predicate = function

888

(* Lazy evaluation of logic operators if the result can be statically computed *)

889

| POr (c1, c2) -> (*BinOp(LOr,convert c1,convert c2,Cil.intType)*)

890

begin

891

let (c1_val,c1_pred) = convert c1 in

892

match c1_val with

893

| Bool3.True -> (c1_val,c1_pred)

894

| Bool3.False -> convert c2

895

| Undefined ->

896

let (c2_val,c2_pred) = convert c2 in

897

match c2_val with

898

| Bool3.True -> (c2_val,c2_pred)

899

| Bool3.False -> (c1_val,c1_pred)

900

| Undefined -> (Undefined,Por(unamed c1_pred, unamed c2_pred))

901

end

902

903

| PAnd (c1, c2) -> (*BinOp(LAnd,convert c1,convert c2,Cil.intType)*)

904

begin

905

let (c1_val,c1_pred) = convert c1 in

906

match c1_val with

907

| Bool3.True -> convert c2

908

| Bool3.False -> (c1_val,c1_pred)

909

| Undefined ->

910

let (c2_val,c2_pred) = convert c2 in

911

match c2_val with

912

| Bool3.True -> (c1_val,c1_pred)

913

| Bool3.False -> (c2_val,c2_pred)

914

| Undefined -> (Undefined,Pand(unamed c1_pred, unamed c2_pred))

915

end

916

917

| PNot (c1) -> (*UnOp(LNot,convert c1,Cil.intType)*)

918

begin

919

let (c1_val,c1_pred) = convert c1 in

920

match c1_val with

921

| Bool3.True -> (Bool3.False,Pfalse)

922

| Bool3.False -> (Bool3.True,Ptrue)

923

| Undefined -> (c1_val,Pnot(unamed c1_pred))

924

end

925

926

(* Call and return are statically defined *)

927

| PCall (s) ->

928

(Undefined,

929

Pand(

930

unamed(

931

Prel(Req,

932

mk_dummy_term (TLval(TVar(op_logic_var),TNoOffset)) Cil.intType,

933

mk_dummy_term (TConst(func_to_cenum s)) Cil.intType

934

)

935

936

unamed (

937

Prel(Req,

938

mk_dummy_term (TLval(TVar(status_logic_var),TNoOffset)) Cil.intType,

939

mk_dummy_term (TConst(op_status_to_cenum Promelaast.Call)) Cil.intType

940

)

941

)

942

)

943

)

944

945

946

947

| PReturn (s) ->

948

(Undefined,

949

Pand(

950

unamed(

951

Prel(Req,

952

mk_dummy_term (TLval(TVar(op_logic_var),TNoOffset)) Cil.intType,

953

mk_dummy_term (TConst(func_to_cenum s)) Cil.intType

954

)

955

956

unamed (

957

Prel(Req,

958

mk_dummy_term (TLval(TVar(status_logic_var),TNoOffset)) Cil.intType,

959

mk_dummy_term (TConst(op_status_to_cenum Promelaast.Return)) Cil.intType

960

)

961

)

962

)

963

)

964

965

966

967

| PCallOrReturn (s) ->

968

(Undefined,

969

Prel(Req,

970

mk_dummy_term (TLval(TVar(op_logic_var),TNoOffset)) Cil.intType,

971

mk_dummy_term (TConst(func_to_cenum s)) Cil.intType

972

)

973

)

974

975

976

977

978

(* Other expressions are left unchanged *)

979

| PTrue -> (Bool3.True, Ptrue)

980

| PFalse -> (Bool3.False, Pfalse)

981

982

| PIndexedExp(s) -> (Undefined,get_pred_from_tmpident s)

983

984

try

985

let (_,res) = convert cross in

986

res

987

with

988

| _ ->

989

Format.printf "Ltl_to_acsl plugin internal error. Status : Not_found exception during term conversion.\n";

990

assert false

991

992

993

994

995

996

(* ************************************************************************* *)

997

(** {b Buchi automata and C code synchronisation } *)

998

999

let rec mk_expr_disjunction expr_l =

1000

match expr_l with

1001

| [] -> assert false

1002

| expr::[] -> expr

1003

| expr::l -> BinOp(LOr, expr,mk_expr_disjunction l,Cil.intType)

1004

1005

1006

let conj_crosscond_old (value,cross) expr =

1007

if value=Bool3.True

1008

then expr

1009

else BinOp (LAnd,cross,expr,Cil.intType)

1010

1011

1012

1013

1014

(** Computed formula : OR(tr) (crosscond(tr) && i==curStateTMP[transStart(tr)])*)

1015

(** It remains only to affect this result to curState[state]*)

1016

let upd_one_state trans_l statenum func status loc =

1017

let expr_l=ref [] in

1018

List.iter

1019

(fun tr ->

1020

if (statenum=tr.stop.nums) && (isCrossable tr func status) then

1021

expr_l:=

1022

(conj_crosscond_old

1023

(crosscond_to_exp tr.cross func status)

1024

(Lval(mk_int_offseted_array_lval curStateOld tr.start.nums)))::!expr_l

1025

)

1026

trans_l;

1027

1028

let expr =

1029

if !expr_l=[] then mk_int_exp 0

1030

else mk_expr_disjunction !expr_l

1031

1032

Cil_types.Set(

1033

(mk_int_offseted_array_lval curState statenum),

1034

expr,

1035

loc

1036

)

1037

1038

1039

1040

(** Computed formula : crosscond(trans) && curStateTMP[transStart(trans)] && curState[transStop(trans)]*)

1041

(** It remains only to affect this result to curTrans[trans]*)

1042

let upd_one_trans trans func status loc =

1043

let expr=

1044

if isCrossable trans func status then

1045

(* BinOp(LAnd,

1046

crosscond_to_exp trans.cross func status,

1047

BinOp(LAnd,

1048

Lval(mk_int_offseted_array_lval curStateOld trans.start.nums),

1049

Lval(mk_int_offseted_array_lval curState trans.stop.nums),

1050

Cil.intType),

1051

Cil.intType)

1052

1053

1054

1055

conj_crosscond_old

1056

(crosscond_to_exp trans.cross func status)

1057

(Lval(mk_int_offseted_array_lval curStateOld trans.start.nums))

1058

1059

1060

else

1061

(mk_int_exp 0)

1062

1063

Cil_types.Set(

1064

(mk_int_offseted_array_lval curTrans trans.numt),

1065

expr,

1066

loc

1067

)

1068

1069

1070

(** This function returns the list of instructions that have to be introduced just before each call of function and each return of function. These instructions correspond to the synchronisation between C code and Buchi automata. The parameters are :

1071

+ The buchi automata

1072

+ the name of the function that is called or that returns

1073

+ the status of this action (call or return)

1074

+ the localisation associated to this generated code*)

1075

let synch_upd_linear (state_l,trans_l) func status loc =

1076

(* WARNING ! Notice that the order of these operations is very important.

1077

1078

Step 1 has to be done after the Step 0 and before the steps 2 and 3.

1079

Step 4 has to be done after the Step 3.

1080

1081

1082

1083

(* Step 0 : define new value of current operation and its status *)

1084

let inst_curop_upd =

1085

Set(

1086

Cil.var (get_varinfo curOp),

1087

Const(func_to_cenum (func)),

1088

loc

1089

)

1090

1091

let inst_curopstatus_upd =

1092

Set(

1093

Cil.var (get_varinfo curOpStatus),

1094

Const(op_status_to_cenum status),

1095

loc

1096

)

1097

1098

1099

(* Step 1 : update of Old states *)

1100

let step_one_inst =

1101

List.fold_left

1102

(fun inst_l st -> (

1103

Cil_types.Set(

1104

(mk_int_offseted_array_lval curStateOld st.nums),

1105

Lval(mk_int_offseted_array_lval curState st.nums),

1106

loc

1107

))::inst_l)

1108

(inst_curopstatus_upd::[inst_curop_upd])

1109

state_l

1110

1111

1112

(* Step 2 : Computation of reachable states *)

1113

let step_two_inst =

1114

List.fold_left

1115

(fun inst_l st -> (upd_one_state trans_l st.nums func status loc)::inst_l)

1116

step_one_inst

1117

state_l

1118

1119

1120

(* Step 3 : Computation of crossable transitions *)

1121

let step_three_inst =

1122

List.fold_left

1123

(fun inst_l tr -> (upd_one_trans tr func status loc)::inst_l)

1124

step_two_inst

1125

trans_l

1126

1127

1128

(* (* Step 4 : update of Tmp transitions *)

1129

let step_four_inst =

1130

List.fold_left

1131

(fun inst_l tr -> (

1132

Cil_types.Set(

1133

(mk_int_offseted_array_lval curTransTmp tr.numt),

1134

Lval(mk_int_offseted_array_lval curTrans tr.numt),

1135

loc

1136

))::inst_l)

1137

step_three_inst

1138

trans_l

1139

1140

1141

step_four_inst*)

1142

1143

step_three_inst

1144

1145

1146

1147

1148

1149

1150

1151

+ The buchi automata

1152

+ the name of the function that is called or that returns

1153

+ the status of this action (call or return)

1154

+ the localisation associated to this generated code*)

1155

let synch_upd_loops (state_l,trans_l) func status loc =

1156

(* WARNING ! Notice that the order of these operations is very important.

1157

1158

Step 1 has to be done after the Step 0 and before the steps 2 and 3.

1159

Step 4 has to be done after the Step 3.

1160

1161

1162

let vi_iter = make_local_tmp func in

1163

let vi_tmp = make_local_iter func in

1164

1165

(* Step 0 : define new value of current operation and its status *)

1166

let stmt_curop_upd =

1167

Cil.mkStmtOneInstr (Set(

1168

Cil.var (get_varinfo curOp),

1169

Const(func_to_cenum (func)),

1170

loc

1171

))

1172

1173

let stmt_curopstatus_upd =

1174

Cil.mkStmtOneInstr (Set(

1175

Cil.var (get_varinfo curOpStatus),

1176

Const(op_status_to_cenum status),

1177

loc

1178

))

1179

1180

(* Step 1 : update of Old states and reset of states *)

1181

let loop_body =

1182

[Cil.mkStmtOneInstr (Cil_types.Set(

1183

(mk_offseted_array_lval curStateOld Lval(Cil.var vi_iter)),

1184

Lval(mk_offseted_array_lval curState Lval(Cil.var vi_iter)),

1185

loc

1186

));

1187

Cil.mkStmtOneInstr (Cil_types.Set(

1188

(mk_offseted_array_lval curState Lval(Cil.var vi_iter)),

1189

Lval(mk_int_exp 0),

1190

loc

1191

))

1192

]

1193

1194

let step_one_stmt =

1195

(Cil.mkForIncr

1196

vi_iter

1197

(Lval(mk_int_exp 0))

1198

(Lval(mk_int_exp (getNumberOfStates ()) ))

1199

(Lval(mk_int_exp 1))

1200

loop_body)

1201

1202

[stmt_curopstatus_upd;

1203

stmt_curop_upd]

1204

1205

1206

1207

(* Step 2 : Computation of crossable transitions and reachable states *)

1208

let loop_body =

1209

[Cil.mkStmtOneInstr (Cil_types.Set(

1210

Cil.var vi_tmp,

1211

BinOp(BAnd,

1212

...........

1213

));

1214

Cil.mkStmtOneInstr (Cil_types.Set(

1215

(mk_offseted_array_lval curStateOld Lval(Cil.var vi_iter)),

1216

Lval(mk_offseted_array_lval curState Lval(Cil.var vi_iter)),

1217

loc

1218

));

1219

Cil.mkStmtOneInstr (Cil_types.Set(

1220

(mk_offseted_array_lval curState Lval(Cil.var vi_iter)),

1221

Lval(mk_int_exp 0),

1222

loc

1223

))

1224

]

1225

1226

1227

1228

step_three_inst

1229

1230

1231

1232

1233

1234

1235

1236

1237

+ The buchi automata

1238

+ the name of the function that is called or that returns

1239

+ the status of this action (call or return)

1240

+ the localisation associated to this generated code*)

1241

let synch_upd (state_l,trans_l) func status loc =

1242

(*if true

1243

then synch_upd_loops (state_l,trans_l) func status loc

1244

else *)

1245

synch_upd_linear (state_l,trans_l) func status loc

1246

1247

1248

1249

(* ************************************************************************* *)

1250

(** {b Globals management} *)

1251

1252

(** Local copy of the file pointer *)

1253

let file = ref Cil.dummyFile

1254

1255

(** Copy the file pointer locally in the class in order to easiest globals management and initializes some tables. *)

1256

let initFile f =

1257

file:=f ;

1258

Data_for_ltl.setCData ();

1259

(* Adding C variables into our hashtable *)

1260

Globals.Vars.iter (fun vi _ -> set_varinfo vi.vname vi

1261

(* ;

1262

Format.printf" -> global variables added into hashtable: '%s' \n" vi.vname*)

1263

)

1264

1265

1266

(** List of globals awaiting for adding into C file globals *)

1267

let globals_queue = ref []

1268

1269

(** Flush all queued globals declarations into C file globals. *)

1270

let flush_globals () =

1271

let (before,after)=List.fold_left

1272

(fun (b,a) elem ->

1273

match elem with

1274

| GFun(_,_) as func -> (b,func::a)

1275

| _ as other -> (other::b,a)

1276

)

1277

([],[])

1278

!file.globals in

1279

1280

!file.globals <- (List.rev before)@(List.rev !globals_queue)@(List.rev after);

1281

(* !file.globals <- (List.rev !globals_queue)@(!file.globals);*)

1282

globals_queue:=[]

1283

1284

1285

1286

1287

1288

(* Utilities for global variables *)

1289

let mk_global_c_initialized_vars name ty ini=

1290

let vi = (Cil.makeGlobalVar ~logic:true name ty) in

1291

vi.vghost<-true;

1292

globals_queue:=GVar(vi,ini,vi.vdecl)::(!globals_queue);

1293

Globals.Vars.add vi ini;

1294

set_varinfo name vi

1295

1296

1297

let mk_global_c_vars name ty =

1298

let vi = (Cil.makeGlobalVar ~logic:true name ty) in

1299

vi.vghost<-true;

1300

let ini = {init=Some(Cil.makeZeroInit ty)} in

1301

globals_queue:=GVar(vi,ini,vi.vdecl)::(!globals_queue);

1302

Globals.Vars.add vi ini;

1303

set_varinfo name vi

1304

1305

1306

let mk_int_const value =

1307

Const(

1308

CInt64(

1309

Int64.of_int (value),

1310

IInt,

1311

Some(string_of_int(value))

1312

)

1313

)

1314

1315

let mk_global_c_initialized_array name size init =

1316

let ty =

1317

(TArray(

1318

TInt(IInt,[]),

1319

Some(mk_int_const size),

1320

[]

1321

))

1322

1323

mk_global_c_initialized_vars name ty init

1324

1325

let mk_global_c_array name size =

1326

let ty =

1327

(TArray(

1328

TInt(IInt,[]),

1329

Some(mk_int_const size),

1330

[]

1331

))

1332

1333

mk_global_c_vars name ty

1334

1335

1336

let mk_global_c_int name =

1337

let ty = (TInt(IInt,[])) in

1338

mk_global_c_vars name ty

1339

1340

1341

1342

1343

1344

1345

(* Utilities for global enumerations *)

1346

1347

1348

let mk_global_c_enum_type name elements_l =

1349

let i = ref 0 in

1350

let einfo = {

1351

ename=name;

1352

eitems=[];

1353

eattr=[];

1354

ereferenced=true

1355

}

1356

1357

let l = List.map

1358

(fun e ->

1359

i:=!i+1;

1360

{ einame = e;

1361

eival = mk_int_const(!i-1);

1362

eiloc = Cilutil.locUnknown;

1363

eihost = einfo})

1364

elements_l

1365

1366

einfo.eitems <- l;

1367

set_usedinfo name einfo;

1368

globals_queue:=GEnumTag(einfo,Cilutil.locUnknown)::(!globals_queue)

1369

1370

1371

let mk_global_c_enum name name_enuminfo =

1372

mk_global_c_vars name (TEnum(get_usedinfo name_enuminfo,[]))

1373

1374

1375

let mk_global_c_initialized_enum name name_enuminfo ini =

1376

mk_global_c_initialized_vars name (TEnum(get_usedinfo name_enuminfo,[])) ini

1377

1378

1379

1380

(* ************************************************************************* *)

1381

(** {b Terms management / computation} *)

1382

1383

(** Return an integer constant term from the given value. *)

1384

let mk_int_term value =

1385

mk_dummy_term

1386

(TConst( CInt64(Int64.of_int value,IInt,Some(string_of_int value))))

1387

Cil.intType

1388

1389

(** Return an integer constant term with the 0 value. *)

1390

let zero_term() =

1391

mk_int_term 0

1392

1393

(** Returns a term representing the given logic variable (usually a fresh quantified variable). *)

1394

let mk_term_from_logic_var lvar =

1395

mk_dummy_term (TLval(TVar(lvar),TNoOffset)) Cil.intType

1396

1397

1398

(** Returns a term representing the variable associated to the given varinfo *)

1399

let mk_term_from_vi vi =

1400

mk_dummy_term (TLval((Logic_const.lval_to_term_lval (Cil.var vi)))) Cil.intType

1401

1402

1403

(** Given an lval term 'host' and an integer value 'off', it returns a lval term host[off]. *)

1404

let mk_offseted_array host off =

1405

mk_dummy_term

1406

(TLval(Cil.addTermOffsetLval (TIndex(mk_int_term (off),TNoOffset)) host))

1407

Cil.intType

1408

1409

1410

(** Given an lval term 'host' and a term 'term_off', it returns a lval term host[off]. *)

1411

let mk_offseted_array_lval_from_term host term_off =

1412

mk_dummy_term

1413

(TLval(Cil.addTermOffsetLval (TIndex(term_off,TNoOffset)) host))

1414

Cil.intType

1415

1416

1417

(** Given an lval term 'host' and a logic variable 'lvar_off', it returns a lval term host[off].

1418

Usually, logic variables stand for fresh quantified variables. *)

1419

let mk_offseted_array_lval_from_lval host lvar_off =

1420

mk_offseted_array_lval_from_term host (mk_term_from_logic_var lvar_off)

1421

(* mk_dummy_term

1422

(TLval(Cil.addTermOffsetLval (TIndex(mk_term_from_logic_var lvar_off,TNoOffset)) host))

1423

Cil.intType

1424

1425

1426

1427

(** Given the name of a logic and a list of logic variables it returns a call of the logic with variables as parameters. *)

1428

let mk_logic_call name logicvar_param_l =

1429

mk_dummy_term

1430

(Tapp(get_logic name,[],List.map (fun p -> mk_term_from_logic_var p) logicvar_param_l))

1431

Cil.intType

1432

1433

1434

(** Returns a lval term associated to the curState generated variable. *)

1435

let host_state_term () =

1436

lval_to_term_lval (Cil.var (get_varinfo curState))

1437

1438

(** Returns a lval term associated to the curStateOld generated variable. *)

1439

let host_stateOld_term () =

1440

lval_to_term_lval (Cil.var (get_varinfo curStateOld))

1441

1442

(** Returns a lval term associated to the curTrans generated variable. *)

1443

let host_trans_term () =

1444

lval_to_term_lval (Cil.var (get_varinfo curTrans))

1445

1446

1447

1448

(** Given a logic variable and two bounces, it returns the predicate: min<=v<max *)

1449

let mk_logicvar_intervalle logvar min max =

1450

Pand(

1451

unamed (Prel(Rle,mk_int_term min,mk_term_from_logic_var logvar)),

1452

unamed (Prel(Rlt,mk_term_from_logic_var logvar,mk_int_term max))

1453

)

1454

1455

(** Given two names of generated arrays and their size, it returns the predicate: (forall i. 0<=i<size => host1[i]==host2[i]) *)

1456

let mk_eq_tables host_name1 host_name2 size =

1457

let lval1 = lval_to_term_lval ( Cil.var (get_varinfo host_name1)) in

1458

let lval2 = lval_to_term_lval ( Cil.var (get_varinfo host_name2)) in

1459

let tmp_i = Cil.make_logic_var "_buch_i" Cil_types.Linteger in

1460

Pforall([tmp_i],

1461

unamed (

1462

Pimplies (

1463

unamed ( mk_logicvar_intervalle tmp_i 0 size),

1464

unamed (

1465

Prel(Req,

1466

mk_offseted_array_lval_from_lval lval1 tmp_i ,

1467

mk_offseted_array_lval_from_lval lval2 tmp_i

1468

)

1469

)

1470

))

1471

)

1472

1473

1474

(** Given a name of generated array and its size, it returns the expression: (Valide_range(name,0,size-) *)

1475

let mk_valid_range name size =

1476

let lval = lval_to_tsets_lval ( Cil.var (get_varinfo name)) in

1477

let min = mk_int_term 0 in

1478

let max = mk_int_term (size-1) in

1479

Pvalid(TSSingleton(TSAdd_range(TSLval(lval),Some(min),Some(max))))

1480

1481

(** Given a NON EMPTY list of predicates, it returns a conjunction of these predicates. *)

1482

let rec mk_conjunction pred_l =

1483

match pred_l with

1484

| [] -> assert false

1485

| pred::[] -> pred

1486

| pred::l -> Pand (unamed pred,unamed (mk_conjunction l))

1487

1488

let rec mk_conjunction_named pred_l =

1489

match pred_l with

1490

| [] -> assert false

1491

| pred::[] -> pred

1492

| pred::l ->unamed ( Pand (pred,(mk_conjunction_named l)) )

1493

1494

1495

(** Given a NON EMPTY list of predicates, it returns a disjunction of these predicates. *)

1496

let rec mk_disjunction pred_l =

1497

match pred_l with

1498

| [] -> assert false

1499

| pred::[] -> pred

1500

| pred::l -> Por (unamed pred,unamed (mk_disjunction l))

1501

1502

let rec mk_disjunction_named pred_l =

1503

match pred_l with

1504

| [] -> assert false

1505

| pred::[] -> pred

1506

| pred::l -> unamed (Por ( pred, (mk_disjunction_named l)))

1507

1508

(* Utilities for other globals *)

1509

1510

1511

let mk_global_invariant pred name =

1512

globals_queue:=GAnnot (Cil_types.Dinvariant(

1513

{

1514

l_name=name;

1515

l_profile = [];

1516

l_labels = [];

1517

(* l_body = PDefinition(unamed pred);*)

1518

l_body = LBpred(unamed pred);

1519

l_type = None;

1520

l_tparams = []

1521

}

1522

), Cilutil.locUnknown)::(!globals_queue)

1523

1524

1525

let mk_global_comment txt =

1526

globals_queue:=GText (txt)::(!globals_queue)

1527

1528

1529

(** Given

1530

+ the name of the logic (string),

1531

+ the list of its genericity parameter names (string),

1532

+ the list of their type (logic_var),

1533

+ the type of the function return

1534

+ and a list of reads tsets,

1535

it returns a logic function declaration.

1536

A side effect of this function is the registration of this logic into the logics hashtbl from Data_for_ltl. *)

1537

let mk_global_logic name (*generics_l*) types_l type_ret (*reads*) =

1538

let log_info = {

1539

l_name = name; (* name of the function. *)

1540

l_type = type_ret; (* return type. *)

1541

l_profile = types_l;(* type of the arguments. *)

1542

l_labels = []; (* label arguments of the function. *)

1543

l_body = LBreads([]); (* body of the function. *)

1544

l_tparams = []

1545

} in

1546

Data_for_ltl.add_logic name log_info;

1547

Dfun_or_pred(log_info)

1548

1549

1550

let mk_global_axiom name pred =

1551

Dlemma (name, true, [], [], unamed pred)

1552

1553

1554

1555

1556

let mk_global_predicate name moment params_l pred =

1557

(*let log_var_params = List.map (fun p -> Cil.make_logic_var p Linteger) params_l in *)

1558

let pred_info={

1559

l_name =name; (* name of the predicate. *)

1560

l_profile = params_l; (*log_var_params;*) (* arguments of the predicate. *)

1561

l_labels = List.map (fun x -> LogicLabel(x)) moment; (* label arguments. *)

1562

l_body = LBpred(unamed pred); (* definition. *)

1563

l_type = None; (* return type. *)

1564

l_tparams = []

1565

} in

1566

Data_for_ltl.add_predicate name pred_info;

1567

globals_queue:=GAnnot(

1568

Dfun_or_pred(pred_info),

1569

(*Dpredicate_def (pred_info,

1570

[] (*moment*),

1571

pred_info.p_profile,

1572

unamed pred

1573

),*)

1574

Cilutil.locUnknown

1575

)::(!globals_queue)

1576

1577

1578

(** Generates an axiomatisation of transitions from automata into globals.

1579

These annotations are used to express some pre and post condition properties *)

1580

let mk_decl_axiomatized_auotmata () =

1581

let (_,trans_l) = getAutomata() in

1582

let param=(Cil.make_logic_var "tr" Linteger) in

1583

let logic=mk_global_logic transStart (*[]*) [param] (Some Linteger) (*[]*) (*[TSSingleton(TSLval(TSVar(param),TSNo_offset))]*) in

1584

let tr_start_log_info = Data_for_ltl.get_logic transStart in

1585

let annotlist=List.fold_left

1586

(fun res tr ->

1587

(mk_global_axiom

1588

(transStart^(string_of_int tr.numt))

1589

(Prel(Req,

1590

mk_dummy_term

1591

(Tapp(tr_start_log_info,[],[mk_int_term tr.numt]))

1592

Cil.intType,

1593

mk_int_term tr.start.nums))

1594

)::res

1595

)

1596

[logic]

1597

trans_l in

1598

globals_queue:=(GAnnot(Daxiomatic(transStart,List.rev annotlist),

1599

Cilutil.locUnknown

1600

))::(!globals_queue);

1601

1602

1603

let logic=mk_global_logic transStop (*[]*) [param] (Some Linteger) (*[]*) (*[TSSingleton(TSLval(TSVar(param),TSNo_offset))]*) in

1604

let tr_stop_log_info = Data_for_ltl.get_logic transStop in

1605

let annotlist=List.fold_left

1606

(fun res tr ->

1607

(mk_global_axiom

1608

(transStop^(string_of_int tr.numt))

1609

(Prel(Req,

1610

mk_dummy_term

1611

(Tapp(tr_stop_log_info,[],[mk_int_term tr.numt]))

1612

Cil.intType,

1613

mk_int_term tr.stop.nums))

1614

)::res

1615

)

1616

[logic]

1617

trans_l in

1618

1619

globals_queue:=(GAnnot(Daxiomatic(transStop,List.rev annotlist),

1620

Cilutil.locUnknown

1621

))::(!globals_queue);

1622

1623

1624

1625

1626

1627

1628

let num= Cil.make_logic_var "_buch_numTrans" Linteger in

1629

let op = Cil.make_logic_var "_buch_op" Linteger in

1630

let st = Cil.make_logic_var "_buch_status" Linteger in

1631

let pred =

1632

mk_conjunction

1633

(List.map

1634

(fun tr ->

1635

Pimplies(

1636

unamed (Prel(Req, mk_term_from_logic_var num, mk_int_term tr.numt)),

1637

unamed (crosscond_to_pred tr.cross op st)

1638

)

1639

)

1640

trans_l

1641

)

1642

1643

mk_global_predicate transCondP ["L"] [num;op;st] pred;

1644

1645

let pred2 =

1646

Papp(

1647

Data_for_ltl.get_predicate transCondP,

1648

[(LogicLabel("L"),LogicLabel("L"))],

1649

[mk_term_from_logic_var num;

1650

mk_term_from_logic_var (Cil.cvar_to_lvar (Data_for_ltl.get_varinfo curOp));

1651

mk_term_from_logic_var (Cil.cvar_to_lvar (Data_for_ltl.get_varinfo curOpStatus))

1652

]

1653

)

1654

1655

mk_global_predicate transCond ["L"] [num] pred2

1656

1657

1658

1659

1660

1661

(* ************************************************************************* *)

1662

(** {b Initialization management / computation} *)

1663

1664

1665

let get_states_trans_init root =

1666

let (states,trans) = Data_for_ltl.getAutomata () in

1667

let st_old_exps = (Array.make (List.length states) (mk_int_exp 0)) in

1668

let st_exps = (Array.make (List.length states) (mk_int_exp 0)) in

1669

let tr_exps = (Array.make (List.length trans ) (mk_int_exp 0)) in

1670

let acc_exps = (Array.make (List.length states) (mk_int_exp 0)) in

1671

1672

List.iter (

1673

fun tr ->

1674

if (tr.start.Promelaast.init==Bool3.True) && (isCrossableAtInit tr root) then

1675

begin

1676

Array.set tr_exps tr.numt (mk_int_exp 1);

1677

Array.set st_exps tr.stop.nums (mk_int_exp 1);

1678

Array.set st_old_exps tr.start.nums (mk_int_exp 1)

1679

end

1680

) trans;

1681

List.iter (

1682

fun st ->

1683

if (st.acceptation==Bool3.True) then

1684

begin

1685

Array.set acc_exps st.nums (mk_int_exp 1);

1686

end

1687

) states;

1688

1689

let st_old_init =

1690

Array.mapi (

1691

fun i exp ->

1692

(*Chaque cas doit contenir : (offset * init)*)

1693

(Index(mk_int_exp i,NoOffset),SingleInit(exp))

1694

) st_old_exps

1695

1696

let st_init =

1697

Array.mapi (

1698

fun i exp ->

1699

(*Chaque cas doit contenir : (offset * init)*)

1700

(Index(mk_int_exp i,NoOffset),SingleInit(exp))

1701

) st_exps

1702

1703

let tr_init =

1704

Array.mapi (

1705

fun i exp ->

1706

(Index(mk_int_exp i,NoOffset),SingleInit(exp))

1707

) tr_exps

1708

1709

let acc_init =

1710

Array.mapi (

1711

fun i exp ->

1712

(Index(mk_int_exp i,NoOffset),SingleInit(exp))

1713

) acc_exps

1714

1715

(

1716

{init=Some(CompoundInit(Cil.intType, Array.to_list st_old_init))},

1717

{init=Some(CompoundInit(Cil.intType, Array.to_list st_init))},

1718

{init=Some(CompoundInit(Cil.intType, Array.to_list tr_init))},

1719

{init=Some(CompoundInit(Cil.intType, Array.to_list acc_init))}

1720

)

1721

1722

1723

let func_to_init name =

1724

{init=Some(SingleInit(Const(func_to_cenum (name))))}

1725

1726

let funcStatus_to_init st =

1727

{init=Some(SingleInit(Const(op_status_to_cenum (st))))}

1728

1729

1730

1731

1732

1733

1734

1735

1736

class visit_decl_loops_init () =

1737

object (*(self) *)

1738

inherit Visitor.generic_frama_c_visitor

1739

(Project.current ()) (Cil.inplace_visit ()) as super

1740

1741

method vstmt_aux stmt =

1742

begin

1743

match stmt.skind with

1744

| Loop _ -> mk_global_c_vars (Data_for_ltl.loopInit^"_"^(string_of_int stmt.sid)) (TInt(IInt,[]))

1745

| _ -> ()

1746

end;

1747

Cil.DoChildren

1748

end

1749

1750

let mk_decl_loops_init () =

1751

let visitor = new visit_decl_loops_init () in

1752

Cil.visitCilFile (visitor :> Cil.cilVisitor) !file

1753

1754

1755

1756

1757

let mk_invariant_1 () =

1758

mk_global_comment "//* Inv 1 : Each active state is reachable";

1759

let tmp_st = Cil.make_logic_var "_buch_st" Cil_types.Linteger in

1760

let tmp_tr = Cil.make_logic_var "_buch_tr" Cil_types.Linteger in

1761

mk_global_invariant (

1762

Pforall(

1763

[tmp_st],

1764

unamed (Pimplies (

1765

unamed (Pand (

1766

unamed (mk_logicvar_intervalle tmp_st 0 (getNumberOfStates ())),

1767

unamed (Pforall([tmp_tr],

1768

unamed (Pimplies (

1769

unamed ( mk_logicvar_intervalle tmp_tr 0 (getNumberOfTransitions ())),

1770

unamed (

1771

mk_disjunction

1772

[ (* curTrans[tr]==0 *)

1773

Prel(Req,mk_offseted_array_lval_from_lval (host_trans_term ()) tmp_tr , mk_int_term 0) ;

1774

(* transStop(tr)!=st *)

1775

Prel(Rneq,(mk_logic_call transStop [tmp_tr]), mk_term_from_logic_var tmp_st) ;

1776

(* !transCond(tr) *)

1777

Pnot(unamed (Papp(get_predicate transCond,[],[mk_term_from_logic_var tmp_tr]))) ;

1778

(* curStatesOld[transStart(tr)]==0 *)

1779

Prel(Req,mk_offseted_array_lval_from_term (host_stateOld_term()) (mk_logic_call transStart [tmp_tr]), mk_int_term 0)

1780

]

1781

)

1782

))

1783

))

1784

)),

1785

unamed (

1786

(* curStates[st]==0 *)

1787

Prel(Req,mk_offseted_array_lval_from_lval (host_state_term()) (tmp_st), mk_int_term 0)

1788

)

1789

))

1790

)

1791

) "_Buch_st_reach_1"

1792

1793

1794

1795

1796

1797

1798

1799

let mk_invariant_2 () =

1800

mk_global_comment "//* Inv 2 : Each non-active state is not reachable";

1801

let tmp_st = Cil.make_logic_var "_buch_st" Cil_types.Linteger in

1802

let tmp_tr = Cil.make_logic_var "_buch_tr" Cil_types.Linteger in

1803

mk_global_invariant (

1804

Pforall(

1805

[tmp_st],

1806

unamed (Pimplies (

1807

unamed (Pand (

1808

(* 0 <= st <nbStates *)

1809

unamed (mk_logicvar_intervalle tmp_st 0 (getNumberOfStates ())),

1810

(* curStates[st]==0 *)

1811

unamed (Prel(Req,mk_offseted_array_lval_from_lval (host_state_term()) (tmp_st), mk_int_term 0))

1812

)),

1813

unamed (Pforall([tmp_tr],

1814

unamed (Pimplies (

1815

(* 0 <= tr <nbTrans *)

1816

unamed(mk_logicvar_intervalle tmp_tr 0 (getNumberOfTransitions ())),

1817

unamed(

1818

mk_disjunction

1819

[ (* curTrans[tr]==0 *)

1820

Prel(Req,mk_offseted_array_lval_from_lval (host_trans_term ()) tmp_tr , mk_int_term 0) ;

1821

(* transStop(tr)!=st *)

1822

Prel(Rneq,(mk_logic_call transStop [tmp_tr]), mk_term_from_logic_var tmp_st) ;

1823

(* !transCond(tr) *)

1824

Pnot(unamed (Papp(get_predicate transCond,[],[mk_term_from_logic_var tmp_tr]))) ;

1825

(* curStatesOld[transStart(tr)]==0 *)

1826

Prel(Req,mk_offseted_array_lval_from_term (host_stateOld_term()) (mk_logic_call transStart [tmp_tr]), mk_int_term 0)

1827

]

1828

)

1829

))

1830

))

1831

))

1832

)

1833

) "_Buch_st_reach_2"

1834

1835

1836

let mk_invariant_3 () =

1837

mk_global_comment "//* Inv 3 : Each active state is reachable";

1838

let tmp_st = Cil.make_logic_var "_buch_st" Cil_types.Linteger in

1839

let tmp_tr = Cil.make_logic_var "_buch_tr" Cil_types.Linteger in

1840

mk_global_invariant (

1841

Pforall(

1842

[tmp_st],

1843

unamed (Pimplies (

1844

unamed (Pand (

1845

(* 0 <= st <nbStates *)

1846

unamed (mk_logicvar_intervalle tmp_st 0 (getNumberOfStates ())),

1847

(* curStates[st]!=0 *)

1848

unamed (Prel(Rneq,mk_offseted_array_lval_from_lval (host_state_term()) (tmp_st), mk_int_term 0))

1849

)),

1850

unamed (Pexists([tmp_tr],

1851

unamed (mk_conjunction

1852

[ (* 0 <= tr <nbTrans *)

1853

mk_logicvar_intervalle tmp_tr 0 (getNumberOfTransitions ()) ;

1854

(* curTrans[tr]!=0 *)

1855

Prel(Rneq,mk_offseted_array_lval_from_lval (host_trans_term ()) tmp_tr , mk_int_term 0) ;

1856

(* transCond(tr) *)

1857

Papp(get_predicate transCond,[],[mk_term_from_logic_var tmp_tr]) ;

1858

(* transStop(tr)==st *)

1859

Prel(Req,(mk_logic_call transStop [tmp_tr]), mk_term_from_logic_var tmp_st) ;

1860

(* curStatesOld[transStart(tr)]!=0 *)

1861

Prel(Rneq,mk_offseted_array_lval_from_term (host_stateOld_term()) (mk_logic_call transStart [tmp_tr]), mk_int_term 0)

1862

]

1863

)

1864

))

1865

))

1866

)

1867

) "_Buch_st_reach_3"

1868

1869

1870

1871

1872

1873

1874

let mk_invariant_4 () =

1875

mk_global_comment "//* Inv 4 : Each transition annotated as crossable is crossable";

1876

let tmp_tr = Cil.make_logic_var "_buch_tr" Cil_types.Linteger in

1877

mk_global_invariant (

1878

Pforall(

1879

[tmp_tr],

1880

unamed (Pimplies (

1881

unamed (Pand (

1882

(* 0 <= tr <nbTrans *)

1883

unamed (mk_logicvar_intervalle tmp_tr 0 (getNumberOfTransitions ())),

1884

(* curTrans[tr]!=0 *)

1885

unamed (Prel(Rneq,mk_offseted_array_lval_from_lval (host_trans_term ()) tmp_tr , mk_int_term 0))

1886

)),

1887

unamed (mk_conjunction

1888

[

1889

(* transCond(tr) *)

1890

Papp(get_predicate transCond,[],[mk_term_from_logic_var tmp_tr]) ;

1891

(* curStatesOld[transStart(tr)]!=0 *)

1892

Prel(Rneq,mk_offseted_array_lval_from_term (host_stateOld_term()) (mk_logic_call transStart [tmp_tr]), mk_int_term 0);

1893

(* curStates[transStop(tr)]!=0 *)

1894

Prel(Rneq,mk_offseted_array_lval_from_term (host_state_term()) (mk_logic_call transStop [tmp_tr]), mk_int_term 0)

1895

]

1896

)

1897

))

1898

)

1899

) "_Buch_tr_cross_1"

1900

1901

1902

1903

let mk_invariant_5 () =

1904

mk_global_comment "//* Inv 5 : Each crossable transition is crossed";

1905

let tmp_tr = Cil.make_logic_var "_buch_tr" Cil_types.Linteger in

1906

mk_global_invariant (

1907

Pforall(

1908

[tmp_tr],

1909

unamed (Pimplies (

1910

unamed (mk_conjunction

1911

[

1912

(* 0 <= tr <nbTrans *)

1913

mk_logicvar_intervalle tmp_tr 0 (getNumberOfTransitions ());

1914

(* curStatesOld[transStart(tr)]!=0 *)

1915

Prel(Rneq,mk_offseted_array_lval_from_term (host_stateOld_term()) (mk_logic_call transStart [tmp_tr]), mk_int_term 0);

1916

(* transCond(tr) *)

1917

Papp(get_predicate transCond,[],[mk_term_from_logic_var tmp_tr])

1918

]

1919

1920

unamed (mk_conjunction

1921

[

1922

(* curTrans[tr]!=0 *)

1923

Prel(Rneq,mk_offseted_array_lval_from_lval (host_trans_term ()) tmp_tr , mk_int_term 0) ;

1924

(* curStates[transStop(tr)]!=0 *)

1925

Prel(Rneq,mk_offseted_array_lval_from_term (host_state_term()) (mk_logic_call transStop [tmp_tr]), mk_int_term 0)

1926

]

1927

)

1928

))

1929

)

1930

) "_Buch_tr_cross_2"

1931

1932

1933

1934

1935

1936

let mk_invariant_6 () =

1937

mk_global_comment "//* Inv 6 : Non-crossable transitions are not crossed over";

1938

let tmp_tr = Cil.make_logic_var "_buch_tr" Cil_types.Linteger in

1939

mk_global_invariant (

1940

Pforall(

1941

[tmp_tr],

1942

unamed (Pimplies (

1943

unamed (Pand (

1944

(* 0 <= tr <nbTrans *)

1945

unamed (mk_logicvar_intervalle tmp_tr 0 (getNumberOfTransitions ())),

1946

unamed (mk_disjunction

1947

[

1948

(* curStatesOld[transStart(tr)]==0 *)

1949

Prel(Rneq,mk_offseted_array_lval_from_term (host_stateOld_term()) (mk_logic_call transStart [tmp_tr]), mk_int_term 0);

1950

(* transCond(tr) *)

1951

Pnot(unamed(Papp(get_predicate transCond,[],[mk_term_from_logic_var tmp_tr])))

1952

]

1953

)

1954

)),

1955

(* curTrans[tr]!=0 *)

1956

unamed(Prel(Rneq,mk_offseted_array_lval_from_lval (host_trans_term ()) tmp_tr , mk_int_term 0))

1957

))

1958

)

1959

) "_Buch_tr_cross_3"

1960

1961

1962

1963

1964

1965

(** This function computes all newly introduced globals (variables, enumeration structure, invariants, etc. *)

1966

let initGlobals root =

1967

mk_global_comment "//****************";

1968

mk_global_comment "//* BEGIN Primitives generated for LTL verification";

1969

1970

mk_global_comment "//* ";

1971

mk_global_comment "//* States and Trans Variables";

1972

let (st_old_init, st_init, tr_init, (*acc_init*) _) = get_states_trans_init root in

1973

mk_global_c_initialized_array curState (getNumberOfStates()) st_init;

1974

mk_global_c_initialized_array curTrans (getNumberOfTransitions()) tr_init;

1975

mk_global_c_initialized_array curStateOld (getNumberOfStates()) st_old_init;

1976

(* mk_global_c_initialized_array curTransTmp (getNumberOfTransitions()) tr_init;*)

1977

1978

mk_global_comment "//* ";

1979

mk_global_comment "//* Their invariants";

1980

mk_global_invariant

1981

(mk_conjunction

1982

[(mk_valid_range curTrans (getNumberOfTransitions ())) ;

1983

(* (mk_valid_range curTransTmp (getNumberOfTransitions ())) ;*)

1984

(mk_valid_range curState (getNumberOfStates ())) ;

1985

(mk_valid_range curStateOld (getNumberOfStates ()))

1986

])

1987

"Buch_Ranges_Validity";

1988

1989

(* mk_global_invariant

1990

(*(mk_conjunction

1991

[*) (mk_eq_tables curTrans curTransTmp (getNumberOfTransitions ())) (*;

1992

(mk_eq_tables curState curStateTmp (getNumberOfStates ()))

1993

])*)

1994

"Buch_Arrays_Coherence";

1995

1996

1997

mk_global_comment "//* ";

1998

(*mk_global_comment "//* Acceptation States -- UNUSED AT THIS TIME !!!";

1999

mk_global_c_initialized_array acceptSt (getNumberOfStates()) acc_init;

2000

mk_global_invariant (mk_valid_range acceptSt (getNumberOfStates ())) "Buch_acc_Ranges_Validity";

2001

2002

mk_global_comment "//* ";

2003

mk_global_comment "//* Some constants";

2004

mk_global_c_enum_type listOp (List.map (fun e -> func_to_op_func e) (getFunctions_from_c()));

2005

mk_global_c_initialized_enum curOp listOp (func_to_init root);

2006

mk_global_c_enum_type listStatus (callStatus::[termStatus]);

2007

mk_global_c_initialized_enum curOpStatus listStatus (funcStatus_to_init Promelaast.Call);

2008

2009

2010

mk_global_comment "//* ";

2011

mk_global_comment "//* Loops management";

2012

mk_decl_loops_init ();

2013

2014

2015

mk_global_comment "//* ";

2016

mk_global_comment "//**************** ";

2017

mk_global_comment "//* Axiomatized transitions automata";

2018

2019

mk_decl_axiomatized_auotmata ();

2020

2021

mk_global_comment "//* ";

2022

mk_global_comment "//**************** ";

2023

mk_global_comment "//* Safety invariants";

2024

mk_global_comment "//* ";

2025

2026

mk_invariant_1 ();

2027

mk_invariant_2 ();

2028

mk_invariant_3 ();

2029

mk_invariant_4 ();

2030

mk_invariant_5 ();

2031

mk_invariant_6 ();

2032

2033

2034

mk_global_comment "//* ";

2035

mk_global_comment "//* END Primitives generated for LTL verification";

2036

mk_global_comment "//****************";

2037

2038

flush_globals()

2039

2040

2041

2042

2043

2044

2045

2046

2047

2048

2049

2050

(* ************************************************************************* *)

2051

(** {b Pre/post management} *)

2052

2053

2054

(** Function called by mk_asbstract_pre and mk_asbstract_post. *)

2055

let mk_abstract_pre_post (states_l,trans_l) func status =

2056

(* Intially, no state is a source for crossable transition and no transition is crossable*)

2057

let st_status = Array.make (List.length states_l) false in

2058

let tr_status = Array.make (List.length trans_l) false in

2059

2060

(* Conjunction of forbidden transitions and disjunction of crossable transitions are compute together.

2061

Moreover, authorized states are annotate in the same pass.

2062

2063

2064

List.iter

2065

(fun tr ->

2066

if isCrossable tr func status then

2067

begin

2068

Array.set st_status tr.stop.nums true;

2069

Array.set tr_status tr.numt true

2070

end

2071

)

2072

trans_l;

2073

2074

(st_status,tr_status)

2075

2076

(**{b Pre and post condition of C functions} In our point of view, the pre or

2077

the post condition of a C function are defined by the set of states

2078

authorized just before/after the call, as such as the set of crossable

2079

transitions. The following functions generates abstract pre and post-conditions

2080

by using only informations deduced from the buchi automata.

2081

2082

(** Given the buchi automata and the name of a function, it returns two arrays

2083

corresponding to the abstract pre-condition. *)

2084

let mk_asbstract_pre auto func =

2085

mk_abstract_pre_post auto func Promelaast.Call

2086

2087

2088

(** Given the buchi automata and the name of a function, it returns two arrays

2089

corresponding to the abstract post-condition. *)

2090

let mk_asbstract_post auto func =

2091

mk_abstract_pre_post auto func Promelaast.Return

2092

2093

2094

(** Generates a term representing the given pre or post condition.

2095

Transitions and states are rewrited into predicates in the same maner. The computation is then generalized

2096

Conjunction of forbidden and disjunction of authorized are compute together. *)

2097

let pre_post_to_term (st_status, tr_status) =

2098

let pp_to_term an_array array_term =

2099

let (authorized,forbidden,_) =

2100

Array.fold_left

2101

(fun (au_pred,fo_pred,i) b ->

2102

if b then

2103

begin

2104

(por(au_pred,prel(Rneq, zero_term(), (mk_offseted_array array_term i))),

2105

fo_pred,

2106

i+1

2107

)

2108

end

2109

else

2110

(au_pred,

2111

pand(fo_pred,prel(Req, zero_term(), (mk_offseted_array array_term i))),

2112

i+1

2113

)

2114

)

2115

(pfalse,ptrue,0)

2116

an_array

2117

2118

authorized::[forbidden]

2119

2120

2121

let tr = pp_to_term tr_status (host_trans_term ()) in

2122

let st = pp_to_term st_status (host_state_term ()) in

2123

st@tr

2124

2125

2126

2127

2128

2129

2130

2131

2132

2133

2134

2135

let force_condition_to_predicate global_inv restricted_inv =

2136

let pred_l = ref [] in

2137

let treat global restric array_term=

2138

Array.iteri

2139

(fun index value ->

2140

if (not value) && global.(index) then

2141

begin

2142

let n_pred = Prel(Req,(mk_offseted_array array_term index),zero_term())in

2143

pred_l:= n_pred::!pred_l

2144

end

2145

)

2146

restric

2147

2148

treat (fst global_inv) (fst restricted_inv) (host_state_term ());

2149

treat (snd global_inv) (snd restricted_inv) (host_trans_term ());

2150

if !pred_l<>[] then

2151

mk_conjunction (List.rev !pred_l)

2152

else

2153

Ptrue

2154

2155

2156

2157

2158

2159

2160

2161

2162

2163

2164

2165

2166

2167

Local Variables:

2168

compile-command: "LC_ALL=C make -C ../.."

2169

End:

2170

Older »