diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-08-31 22:46:44 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-31 22:46:44 +0100 |
commit | 03d33623bdb9e507525d7ea191fa5ba6eff9d6dd (patch) | |
tree | a6ba3c5b3736a0ffa9a8dc33eeeb3ff6c52cdcc3 /src/hls | |
parent | b431bdeb59e69df41cd98fadea49968d224493ee (diff) | |
download | vericert-kvx-03d33623bdb9e507525d7ea191fa5ba6eff9d6dd.tar.gz vericert-kvx-03d33623bdb9e507525d7ea191fa5ba6eff9d6dd.zip |
Fix bug for basic block construction in loops
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/Partition.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index 1c25cdc..e0cacd1 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -61,15 +61,19 @@ let translate_cfi = function let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in let trans_inst = (translate_inst i, translate_cfi i) in + printf "Current: %d\n" (P.to_int s); match trans_inst, succ with | (None, Some i'), _ -> + if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) } + else Errors.OK {bb_body = []; bb_exit = Some i'} | (Some i', None), (s', Some i_n)::[] -> if List.exists (fun x -> x = s) (fst e) then Errors.OK { bb_body = [i']; bb_exit = Some (RBgoto s') } - else if List.exists (fun x -> x = s) (snd e) && not is_start then begin + else if List.exists (fun x -> x = s) (snd e) && not is_start then Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) } - end else begin + else begin match next_bblock_from_RTL false e c s' i_n with | Errors.OK bb -> Errors.OK (prepend_instr i' bb) @@ -98,7 +102,7 @@ let rec translate_all edge c s c_bb = | Errors.OK {bb_exit = None; _} -> Errors.Error (Errors.msg (coqstring_of_camlstring "Error in translate all")) | Errors.OK {bb_body = bb; bb_exit = Some e} -> - let succ = successors_instr e in + let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in match traverseacc (translate_all edge c) succ c_bb with | Errors.Error msg -> Errors.Error msg | Errors.OK c' -> |